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.
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
.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With