Language.TEval.TInfLetI

Simply-typed Curry-style (nominal) lambda-calculus with integers and zero-comparison Let-polymorphism via inlining Type inference

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

Documentation

data Typ

Constructors

TInt

!Typ :> !Typ

TV TVarName

Instances

Eq Typ

Show Typ

type TVarName = Int

data Term

Constructors

V VarName

L VarName Term

A Term Term

I Int

Term :+ Term

IFZ Term Term Term

Fix Term

Let (VarName, Term) Term

Instances

Eq Term

Show Term

type VarName = String

type TEnv = [(VarName, TVEM Typ)]

Type Environment: associating *would-be* types with free term variables

env0 :: TEnv

lkup :: TEnv -> VarName -> TVEM Typ

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

data TVE

Type Variable Environment: associating types with free type variables

Constructors

TVE Int (IntMap Typ)

Instances

Show TVE

type TVEM = State TVE

TVE is the state of a monadic computation

newtv :: TVEM Typ

Allocate a fresh type variable (see the first component of TVE)

tve0 :: TVE

tvlkup :: TVE -> TVarName -> Maybe Typ

tvext :: TVE -> (TVarName, Typ) -> TVE

tvsub :: TVE -> Typ -> Typ

Type variables are logic variables: hypothetical reasoning

tvchase :: TVE -> Typ -> Typ

shallow substitution; check if tv is bound to anything substantial

unify :: Typ -> Typ -> TVE -> Either String TVE

The unification. If unification failed, return the reason

unify' :: Typ -> Typ -> TVE -> Either String TVE

If either t1 or t2 are type variables, they are definitely unbound

unifyv :: TVarName -> Typ -> TVE -> Either String TVE

Unify a free variable v1 with t2

occurs :: TVarName -> Typ -> TVE -> Bool

The occurs check: if v appears free in t

unifyM :: Typ -> Typ -> (String -> String) -> TVEM ()

Monadic version of unify

teval' :: TEnv -> Term -> TVEM Typ

Type reconstruction: abstract evaluation

teval :: TEnv -> Term -> Typ

Resolve all type variables, as far as possible

Exception: constant mismatch: TInt and TV 2 :> TV 2

Exception: occurs check: TV 5 in TV 5 :> TV 5