Safe Haskell	None
Language	Haskell2010

Abt.Tutorial

Synopsis

Documentation

newtype M α Source

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 α -> α Source

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

data Lang ns where Source

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

Constructors

LAM :: Lang `[S Z]`
APP :: Lang `[Z, Z]`
PI :: Lang `[Z, S Z]`
UNIT :: Lang []
AX :: Lang []

Instances

HEq1 [Nat] Lang
Show1 [Nat] Lang

lam :: Tm Lang (S Z) -> Tm0 Lang Source

app :: Tm0 Lang -> Tm0 Lang -> Tm0 Lang Source

ax :: Tm0 Lang Source

unit :: Tm0 Lang Source

pi :: Tm0 Lang -> Tm Lang (S Z) -> Tm0 Lang Source

newtype StepT m α Source

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 α Source

To indicate that a term is in normal form.

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

A single evaluation step.

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

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

eval :: Tm0 Lang -> Tm0 Lang Source

Evaluate a term to normal form

newtype JudgeT m α Source

Constructors

JudgeT
Fields runJudgeT :: ExceptT String m α

Instances

MonadVar Var m => MonadVar Var (JudgeT m)
(Monad m, Functor m) => Alternative (JudgeT m)
Monad m => Monad (JudgeT m)
Functor m => Functor (JudgeT m)
(Monad m, Functor m) => Applicative (JudgeT m)

type Ctx = [(Var, Tm0 Lang)] Source

raise :: Monad m => String -> JudgeT m α Source

checkTy :: Ctx -> Tm0 Lang -> Tm0 Lang -> JudgeT M () Source

inferTy :: Ctx -> Tm0 Lang -> JudgeT M (Tm0 Lang) Source

identityTm :: M (Tm0 Lang) Source

λx.x

appTm :: M (Tm0 Lang) Source

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

main :: IO () Source

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

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