How do Let expressions work in AST?

Question

Consider:

data Expr a
  = V a
  | Lit Integer
  | Let (Expr a) (Expr (Maybe a))
    deriving (Eq,Show)

The Let constructor enables me to bind an expression (first arg) in order to reference it in the second (V Nothing refers to it).

If I do something like

Let (Lit 3) $ Let (Lit 1) $ Var Nothing

which Lit does the Var Nothing refer to? Furthermore, I’d like to generalize that to multiple bindings at once, and I have no idea how to do that. I followed some examples from the excellent Edward Kmett bound package, but now I’m both confused and lost.

Jat

Answer 1

I'm guessing slightly because I haven't seen this style of binding before, but I think the Maybe type is effectively being used to encode de Bruijn indices.

The basic idea there is that references to bound variables are stored as a number specifying the number of surrounding binders to go through to reach the relevant binder. So for example 0 would refer to the closest surrounding binder, 1 to the next closest, and so on.

I think what's happening here is that Maybe is being used to count the binders instead. So Nothing is equivalent to 0 and refers to the closest binder, and Just Nothing is equivalent to 1 and refers to the next closest, and so on.

So in your example, the V Nothing would refer to Lit 1, whereas V (Just Nothing) would refer to Lit 3.

Balsa

Ok, but the V (Just Nothing) doesn’t type check, does it? – Jat

It should do, because the type parameter inside two Lets will be Maybe (Maybe a). – Balsa

This is almost certainly it. Reminds me a lot of how bound works. – Genoese