Language.TEval.TEvalNR

Simply-typed Church-style (nominal) lambda-calculus with integers and zero-comparison Type reconstruction, for all subterms

http://okmij.org/ftp/Computation/Computation.html#teval

Documentation

data Typ

Constructors

TInt

!Typ :> !Typ

Instances

Eq Typ

Show Typ

data Term

Constructors

V VarName

L VarName Typ Term

A Term Term

I Int

Term :+ Term

IFZ Term Term Term

Fix Term

Instances

Eq Term

Show Term

type VarName = String

type TEnv = [(VarName, Typ)]

Type Environment: associating types with free variables

env0 :: TEnv

lkup :: TEnv -> VarName -> Typ

ext :: TEnv -> (VarName, Typ) -> TEnv

type TermIndex = [Int]

A virtual typed AST: associating a type to each subterm

type Typs = Map TermIndex Typ

topterm :: Typ -> Typs

toptyp :: Typs -> Typ

shift :: Int -> Typs -> Typs

teval :: TEnv -> Term -> Typs

Type reconstruction: abstract evaluation