Data.Bind
Binders, the two nameless coordinate systems, and the canonical rendering that makes alpha-equivalent terms identical.
Names are for working, indices are for identity. A checker, an interpreter and an error message all want the name the programmer wrote; only a hash and a wire format want the name gone. This module keeps both and puts the boundary between them in one place.
The two coordinate systems are branded so they cannot be mixed up. An Index is the outward distance from a use site to its binder, so it survives adding binders at the root and it is what a nameless rendering emits. A Level is the inward distance from the root to a binder, so it survives going deeper and it is what an environment addresses. bind_index_at and bind_level_at are the only conversions between them, and at a fixed depth each is the other’s inverse. Nothing here accepts a bare Int where one of the two is meant. Opt-in: not in Base.
Types
Index
type Index = MkIndex(Int) deriving (Eq, Ord, Show)
The outward distance from a use site to the binder it refers to: bind_index(0) is the nearest enclosing binder.
The constructor is spelled MkIndex rather than Index on purpose: constructors share one flat namespace with every module in the program, so a constructor named for its type would rebind any other Index in scope and the failure would surface far from the declaration.
Level
type Level = MkLevel(Int) deriving (Eq, Ord, Show)
The inward distance from the root to a binder: bind_level(0) is the outermost binder in scope. Constructor named MkLevel for the same reason Index uses MkIndex.
BindEnv
type BindEnv(a) = BindEnv { slots: List((String, a)) }
The binders in scope, innermost first, each with a name and a payload.
Shadowing is by position, not by rewriting: pushing a name that is already in scope hides the older slot from bind_index_of while leaving it reachable by its own index, which is what an interpreter walking a closure environment needs.
Nameless
type Nameless
= NTok(String)
| NLit(String)
| NRef(String)
| NScope(List(String), Nameless)
| NSeq(List(Nameless))
deriving (Eq, Show)
A rendering skeleton that knows where the binders are.
The fold over it is the whole point: a term’s own traversal decides which tokens to emit and which names it binds, and this decides how a reference is spelled. Because a bound reference is spelled by outward distance, two terms that differ only in the names of their binders render to the same bytes.
Functions and Values
bind_index
bind_index : (Int) -> Data.Bind.Index
Brand a raw outward distance as an Index. One of the two ways in.
bind_index_int(bind_index(2))
2
bind_level
bind_level : (Int) -> Data.Bind.Level
Brand a raw inward distance as a Level. One of the two ways in.
bind_level_int(bind_level(2))
2
bind_index_int
bind_index_int : (Data.Bind.Index) -> Int
The raw distance carried by an Index. One of the two ways out.
bind_level_int
bind_level_int : (Data.Bind.Level) -> Int
The raw distance carried by a Level. One of the two ways out.
bind_index_at
bind_index_at : (Int, Data.Bind.Level) -> Data.Bind.Index
The index a use site under depth binders must write to reach level l.
This and bind_level_at are the module’s only conversions, and they are the same reflection, so at a fixed depth each undoes the other. Both are undefined outside 0 <= distance < depth; a caller that might be out of scope should ask the environment instead.
bind_index_int(bind_index_at(3, bind_level(0)))
2
bind_level_at
bind_level_at : (Int, Data.Bind.Index) -> Data.Bind.Level
The level that a use site under depth binders reaches by writing index i.
bind_level_int(bind_level_at(3, bind_index_at(3, bind_level(2))))
2
bind_empty
bind_empty : forall a. Data.Bind.BindEnv(a)
No binders in scope.
bind_push
bind_push : forall a. (Data.Bind.BindEnv(a), String, a) -> Data.Bind.BindEnv(a)
Push one binder, which becomes index 0. Pushing a shadowing name keeps the older slot addressable at its previous index.
let env = bind_push(bind_push(bind_empty, "x", 1), "x", 2)
(bind_at(env, bind_index(0)), bind_at(env, bind_index(1)))
(Some(2), Some(1))
bind_push_all
bind_push_all : forall a. (Data.Bind.BindEnv(a), List((String, a))) -> Data.Bind.BindEnv(a)
Push several binders at once, leftmost outermost, the way a multi-parameter binder brings its parameters into scope.
bind_name_at(bind_push_all(bind_empty, [("x", 1), ("y", 2)]), bind_index(1))
Some(x)
bind_push_names
bind_push_names : (Data.Bind.BindEnv(String), List(String)) -> Data.Bind.BindEnv(String)
Push binders that carry no payload beyond their own name.
bind_names(bind_push_names(bind_empty, ["x", "y"]))
[y, x]
bind_depth
bind_depth : forall a. (Data.Bind.BindEnv(a)) -> Int
How many binders are in scope. A use site here writes indices below this and levels below this.
bind_names
bind_names : forall a. (Data.Bind.BindEnv(a)) -> List(String)
Every name in scope, innermost first, with shadowed names still listed at their own index.
bind_drop
bind_drop : forall a. (Data.Bind.BindEnv(a), Int) -> Data.Bind.BindEnv(a)
Drop the n innermost binders, leaving what was in scope before them.
bind_names(bind_drop(bind_push_names(bind_empty, ["x", "y", "z"]), 2))
[x]
bind_index_of
bind_index_of : forall a. (Data.Bind.BindEnv(a), String) -> Option(Data.Bind.Index)
The index of the innermost binder named name, or None when the name is free here.
match bind_index_of(bind_push_names(bind_empty, ["x", "y"]), "y") of
None => -1
Some(i) => bind_index_int(i)
0
bind_level_of
bind_level_of : forall a. (Data.Bind.BindEnv(a), String) -> Option(Data.Bind.Level)
The level of the innermost binder named name, or None when the name is free here.
bind_slot_at
bind_slot_at : forall a. (Data.Bind.BindEnv(a), Data.Bind.Index) -> Option((String, a))
The binder an index points at, name and payload, or None when the index escapes the environment.
bind_at
bind_at : forall a. (Data.Bind.BindEnv(a), Data.Bind.Index) -> Option(a)
The payload an index points at.
bind_name_at
bind_name_at : forall a. (Data.Bind.BindEnv(a), Data.Bind.Index) -> Option(String)
The name an index points at, which is what an error message wants back.
bind_at_level
bind_at_level : forall a. (Data.Bind.BindEnv(a), Data.Bind.Level) -> Option(a)
The payload a level points at.
bind_at_level(bind_push_all(bind_empty, [("x", 10), ("y", 20)]), bind_level(0))
Some(10)
bind_name_at_level
bind_name_at_level : forall a. (Data.Bind.BindEnv(a), Data.Bind.Level) -> Option(String)
The name a level points at.
bind_token
bind_token : (String) -> String
A token committed with its byte length, so no token can be confused with the concatenation of its neighbours.
bind_token("add")
3:add
bind_num_end
bind_num_end : String
The character closing every run of digits a rendering writes.
Skeletons concatenate with no separator, so a digit run sitting beside a neighbour that also opens with a digit reads as one number and the boundary between them is lost. A binder index therefore closes with this character, and a caller emitting its own numeric tags through NLit closes them the same way to keep the whole rendering uniquely decodable.
bind_nameless
bind_nameless : ((String) -> String, Data.Bind.Nameless) -> String
Render a skeleton with binder references as outward distance and free names spelled by free.
A bound reference becomes b, its index, and bind_num_end. A free name is handed to free, which is where a caller substitutes whatever identity it has for a name it does not own: a content hash, a slot in the recursive group being hashed, or the name itself.
bind_nameless(\(x) -> x, NScope(["a"], NSeq([NTok("lam"), NRef("a")])))
3:lamb0;
bind_nameless_show
bind_nameless_show : (Data.Bind.Nameless) -> String
Render with free names spelled as length-prefixed tokens under an f tag.
This is the rendering to compare two terms with when nothing outside them matters, which is exactly alpha-equivalence.
bind_nameless_show(NSeq([NRef("free"), NScope(["x"], NRef("x"))]))
f4:freeb0;
bind_alpha_eq
bind_alpha_eq : (Data.Bind.Nameless, Data.Bind.Nameless) -> Bool
True when two skeletons differ only in the names of their bound variables.
bind_alpha_eq(
NScope(["a"], NRef("a")),
NScope(["b"], NRef("b")),
)
true