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




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.



data Typ Source


!Typ :> !Typ 
TV TVarName 


type TEnv = [(VarName, Typ)]Source

Type Environment: associating types with free term variables

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

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

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

data TVE Source

Type Variable Environment: associating types with free type variables


TVE Int (IntMap Typ) 


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

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

Type reconstruction: abstract evaluation

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

Resolve all type variables, as far as possible

Exception: Branches of IFZ have different types.

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