liboleg-2010.1.10.0: An evolving collection of Oleg Kiselyov's Haskell modules




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



data Typ Source


!Typ :> !Typ 
TV TVarName 


type TEnv = [(VarName, TVEM Typ)]Source

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

data TVE Source

Type Variable Environment: associating types with free type variables


TVE Int (IntMap Typ) 


type TVEM = State TVESource

TVE is the state of a monadic computation

newtv :: TVEM TypSource

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

tvsub :: TVE -> Typ -> TypSource

Type variables are logic variables: hypothetical reasoning

tvchase :: TVE -> Typ -> TypSource

shallow substitution; check if tv is bound to anything substantial

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

The unification. If unification failed, return the reason

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

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

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

Unify a free variable v1 with t2

occurs :: TVarName -> Typ -> TVE -> BoolSource

The occurs check: if v appears free in t

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

Monadic version of unify

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

Type reconstruction: abstract evaluation

teval :: TEnv -> Term -> TypSource

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