mlabs-haskell / lambda-buffers

LambdaBuffers toolkit for sharing types and their semantics between different languages
https://mlabs-haskell.github.io/lambda-buffers/
Apache License 2.0
29 stars 0 forks source link

Generalizing `PrintRead` to allow type information to change the generated builtin. #155

Closed jaredponn closed 7 months ago

jaredponn commented 7 months ago

This PR changes

newtype PrintRead qvn = MkPrintRead { builtins :: Map ValueName qvn }

to

newtype PrintRead qvn = MkPrintRead { builtins :: Ref -> Maybe qvn }

s.t. the generated qvn may be influenced by the types it is instantiated with.

This is important because in languages without type classes, we need to explicitly say which instance should be used. For example if we have type

prod Dog = Dog Int Char

when we generate the Eq instance, writing something like

eq (Dog a0 b0)  (Dog a1 b1) = a0 `eq` a1 && b0 `eq` b1

won't suffice, as we must provide the type information of Int and Char to a0 `eq` a1 and b0 `eq` b1 respectively. We would need to write something like

eq (Dog a0 b0)  (Dog a1 b1) = a0 `eqInt` a1 && b0 `eqChar` b1

Admittedly, I see this as a temporary fix since the builtins really should provide the types they may be instantiated with e.g. we shouldn't just have eq as a builtin -- we should have eq instantiated with typesInt, Char, blah blah blah, are all builtins

bladyjoker commented 7 months ago

I think this is fairly uncontroversial change and @szg251's work in Rust codegen will not suffer for it. I'll go ahead an merge this.