• 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.

De Bruijn Index

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


Scala Bound

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

Go to the Edward Kmett's slides

<Thank You!>