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

newtype StepT m α

A monad transformer for small step operational semantics.

Constructors

StepT

Fields

runStepT :: MaybeT m α

Instances

MonadVar Var m => MonadVar Var (StepT m)

(Monad m, Functor m) => Alternative (StepT m)

Monad m => Monad (StepT m)

Functor m => Functor (StepT m)

(Monad m, Functor m) => Applicative (StepT m)

stepsExhausted :: Applicative m => StepT m α

To indicate that a term is in normal form.

step :: Tm0 Lang -> StepT M (Tm0 Lang)

A single evaluation step.

star :: Monad m => (α -> StepT m α) -> α -> m α

The reflexive-transitive closure of a small-step operational semantics.

eval :: Tm0 Lang -> Tm0 Lang

Evaluate a term to normal form

identityTm :: M (Tm0 Lang)

λx.x

appTm :: M (Tm0 Lang)

(λx.x)(λx.x)

main :: IO ()

A demonstration of evaluating (and pretty-printing). Output:

ap[lam[@2.@2];lam[@3.@3]] ~>* lam[@2.@2]