Language.TEval.TInfTEnv

Simply-typed Curry-style (nominal) lambda-calculus with integers and zero-comparison Type inference, of the type and of the environment, aka conditional typechecking This code does not in general infer polymorphic bindings as this is akin to higher-order unification.

The benefit of the approach: we can handle _open_ terms. Some of them we type check, and some of them we reject. The rejection means the term cannot be typed in _any_ type environment.

One often hears a complaint against typing: one can evaluate terms we can't even type check. This code shows that we can type check terms we can't even evaluate.

We cannot evaluate open terms at all, but we can type check them, inferring both the type as well as the _requirement_ on the environments in which the term must be used.

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

Instances

Eq Term

Show Term

type VarName = String

type TEnv = [(VarName, Typ)]

Type Environment: associating types with free term variables

env0 :: TEnv

lkup :: TEnv -> VarName -> Typ

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

unext :: TEnv -> VarName -> TEnv

env_map :: (Typ -> Typ) -> TEnv -> TEnv

env_fold_merge :: TEnv -> TEnv -> (Typ -> Typ -> seed -> Either err seed) -> seed -> Either err (TEnv, seed)

Merge two environment, using the given function to resolve the conflicts, if any

data TVE

Type Variable Environment: associating types with free type variables

Constructors

TVE Int (IntMap Typ)

Instances

Show TVE

newtv :: TVE -> (Typ, TVE)

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

merge_env :: TEnv -> TEnv -> TVE -> (TEnv, TVE)

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

Type reconstruction: abstract evaluation

teval :: Term -> (Typ, TEnv)

Resolve all type variables, as far as possible

Exception: Branches of IFZ have different types.

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