search

lambdageek / unbound-generics

Specify variable binding in syntax trees using GHC.Generics (reimplementation of Unbound)
https://hackage.haskell.org/package/unbound-generics/
BSD 3-Clause "New" or "Revised" License
56 stars 18 forks source link

What does Embed really do? #22

Closed mrkgnao closed 6 years ago

mrkgnao commented 6 years ago

Hi, new user here: is there a functional difference between the following two representations of a type-annotated lambda?

data Exp  = ... | Lam  Ty (Bind (Name Exp)            Exp)
data Exp' = ... | Lam'    (Bind (Name Exp', Embed Ty) Exp')

Other than the fact that unbind and so on return different things, that is: are there differences in substitution, instantiation, and so on?

mrkgnao commented 6 years ago

From this paper, I gather that there is no real difference in this case:

http://www.seas.upenn.edu/~sweirich/papers/icfp11.pdf

but that Embed allows you to keep, e.g. (Name e, Type t) pairs together for things like lets that bind multiple names at once.

lambdageek commented 6 years ago

Sorry I missed this. Yes, that's exactly right: it becomes more useful when you're using combinators like Rebind or Rec:

-- model mutual recursion:
--   letrec x1 = e1 and ... and xN = eN in body
data Expr = ...
  | Letrec (Bind (Rec [(Var, Embed Expr)]) Expr)
type Var = Name Expr

I think the original paper also had some comment about Lambda (Bind (Var, Embed Type) Expr) being more readable because it's in the same order as a concrete syntax lambda x:t. e, but in practice I find that awkward to work with because you have to unbind just to look at the type which is unnecessary. So in simple cases I (now) tend to prefer Lambda Type (Bind Var Expr).