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 Let-polymorphism via type schemes Type inference



data Typ Source


!Typ :> !Typ 
TV TVarName 


data TypS Source


TypS [TVarName] Typ 


type TEnv = [(VarName, TypS)]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)

tvdomainp :: TVE -> TVarName -> BoolSource

TVE domain predicate: check to see if a TVarName is in the domain of TVE

tvfree :: TVE -> [TVarName]Source

Give the list of all type variables that are allocated in TVE but not bound there

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

tvdependentset :: TVE -> TVE -> TVarName -> BoolSource

Compute (quite unoptimally) the characteristic function of the set forall tvb in fv(tve_before). Union fv(tvsub(tve_after,tvb))

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

Monadic version of unify

instantiate :: TypS -> TVEM TypSource

Given a type scheme, that is, the type t and the list of type variables tvs, for every tvs, replace all of its occurrences in t with a fresh type variable. We do that by creating a substitution tve and applying it to t.

generalize :: TVEM Typ -> TVEM TypSSource

Given a typechecking action ta yielding the type t, return the type scheme quantifying over _truly free_ type variables in t with respect to TVE that existed before the typechecking action began. Let tve_before is TVE before the type checking action is executed, and tve_after is TVE after the action. A type variable tv is truly free if it is free in tve_after and remains free if the typechecking action were executed in any tve extending tve_before with arbitrary binding to type variables free in tve_before. To be more precise, a type variable tv is truly free with respect to tve_before if: tv notin domain(tve_after) forall tvb in fv(tve_before). tv notin fv(tvsub(tve_after,tvb)) In other words, tv is truly free if it is free and independent of tve_before.

Our goal is to reproduce the behavior in TInfLetI.hs: generalize/instantiate should mimic multiple executions of the typechecking action. That means we should quantify over all type variables created by ta that are independent of the type environment in which the action may be executed.

freevars :: Typ -> [TVarName]Source

Return the list of type variables in t (possibly with duplicates)

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

Type reconstruction: abstract evaluation

teval :: TEnv -> Term -> TypSSource

Resolve all type variables, as far as possible, and generalize We assume teval will be used for top-level expressions where generalization is appropriate.

tevalng :: TEnv -> Term -> TypSource

non-generalizing teval (as before)

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

Exception: occurs check: TV 1 in TV 1 :> TV 1