Simply-typed Curry-style (nominal) lambda-calculus with integers and zero-comparison Let-polymorphism via type schemes Type inference
- data Typ
- type TVarName = Int
- data TypS = TypS [TVarName] Typ
- data Term
- type VarName = String
- type TEnv = [(VarName, TypS)]
- env0 :: TEnv
- lkup :: TEnv -> VarName -> TypS
- ext :: TEnv -> (VarName, TypS) -> TEnv
- data TVE = TVE Int (IntMap Typ)
- type TVEM = State TVE
- newtv :: TVEM Typ
- tve0 :: TVE
- tvlkup :: TVE -> TVarName -> Maybe Typ
- tvext :: TVE -> (TVarName, Typ) -> TVE
- tvdomainp :: TVE -> TVarName -> Bool
- tvfree :: TVE -> [TVarName]
- tvsub :: TVE -> Typ -> Typ
- tvchase :: TVE -> Typ -> Typ
- unify :: Typ -> Typ -> TVE -> Either String TVE
- unify' :: Typ -> Typ -> TVE -> Either String TVE
- unifyv :: TVarName -> Typ -> TVE -> Either String TVE
- occurs :: TVarName -> Typ -> TVE -> Bool
- tvdependentset :: TVE -> TVE -> TVarName -> Bool
- unifyM :: Typ -> Typ -> (String -> String) -> TVEM ()
- instantiate :: TypS -> TVEM Typ
- generalize :: TVEM Typ -> TVEM TypS
- freevars :: Typ -> [TVarName]
- teval' :: TEnv -> Term -> TVEM Typ
- teval :: TEnv -> Term -> TypS
- tevalng :: TEnv -> Term -> Typ
Documentation
type TEnv = [(VarName, TypS)]Source
Type Environment: associating *would-be* types with free
term variables
Type Variable Environment: associating types with free
type variables
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
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
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))
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 -> 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.