Abt.Tutorial

Documentation

newtype M α

We'll start off with a monad in which to manipulate ABTs; we'll need some state for fresh variable generation.

Constructors

M

Fields

_M :: State Int α

Instances

Monad M

Functor M

Applicative M

MonadVar Var M

Check out the source to see fresh variable generation.

runM :: M α -> α

We'll run an ABT computation by starting the variable counter at 0.

data Lang ns where

Next, we'll define the operators for a tiny lambda calculus as a datatype indexed by arities.

Constructors

Lam :: Lang `[S Z]`

Ap :: Lang `[Z, Z]`

Instances

HEq1 [Nat] Lang

Show1 [Nat] Lang

example :: M [Var]

Check out the source to see this example term: note that number of arguments and presence of abstractions is guaranteed by the types. The representation is not scope-safe (i.e. free variables are permitted), but that's how we want it.