• The library provides convenient combinators for working with "locally-nameless" terms.
• With generalized de Bruijn term
  • you can lift whole trees instead of just applying succ to individual variables.
  • higher rank types isn't necessary by using a monad transformer.
• Useful for writing a AST of binders like forall or lambda.

the De Bruijn index is a notation for representing terms in the λ calculus with the purpose of eliminating the names of the variable from the notation.

λz. (λy. y (λx. x)) (λx. z x) is

• ekmett/bound · GitHub
• HackageDB: bound-0.7
• Richard Bird and Ross Patterson's de Bruijn notation as a nested data type
• Conor McBride and James McKinna's I am not a number: I am a free variable
• runarorama/scala-bound · GitHub

• A Scala port by runarorama.
• Implement Var using Either.
• There is no polymorphic recursion issue.