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

Language.TEval.TInfTM

Description

Simply-typed Curry-style (nominal) lambda-calculus with integers and zero-comparison Type inference. Hiding the single-threaded state via simple algebraic transformations (beta-expansions).

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

Synopsis

Documentation

data Typ Source

Constructors

TInt 
!Typ :> !Typ 
TV TVarName 

Instances

type TEnv = [(VarName, Typ)]Source

Type Environment: associating types with free term variables

data TVE Source

Type Variable Environment: associating types with free type variables

Constructors

TVE Int (IntMap Typ) 

Instances

newtv :: TVE -> (Typ, TVE)Source

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

type TVEM a = TVE -> (a, TVE)Source

Introducing the combinators to hide single-threaded state tve in one case of teval' (the A case). The other cases stay as they are, to illustrate that our transformation is fully compatible with the earlier code.

(>>=) :: TVEM a -> (a -> TVEM b) -> TVEM bSource

return :: a -> TVEM aSource

teval' :: TEnv -> Term -> TVE -> (Typ, TVE)Source

The expression abstracted from the last-but-one re-writing of the A-clause below

Type reconstruction: abstract evaluation