Bound variable indexing - kvverti/rusty-lavender GitHub Wiki

Type unification is interested in unifying the following

for a b. a -> b
for a b. b -> a

and in calculating the order of parameters for

'a -> 'b

Current Plan

• Do an ordered traversal of the parse tree
• Save the order of bound variable encounters
  • Current plan is via a trie structure - this would make it easier to query symbols as well
• Transform expressions with implicit bound variables into lambdas, and replace bound variable references with modified De Bruijn indices.