liboleg-0.2: A collection of Oleg Kiselyov's Haskell modules (2009-2008)

Language.TEval.TInfLetP

Description

Simply-typed Curry-style (nominal) lambda-calculus with integers and zero-comparison Let-polymorphism via type schemes Type inference

Synopsis

# Documentation

data Typ Source

Constructors

 TInt !Typ :> !Typ TV TVarName

Instances

 Eq Typ Show Typ

data TypS Source

Constructors

 TypS [TVarName] Typ

Instances

 Show TypS

data Term Source

Constructors

 V VarName L VarName Term A Term Term I Int Term :+ Term IFZ Term Term Term Fix Term Let (VarName, Term) Term

Instances

 Eq Term Show Term

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

Constructors

 TVE Int (IntMap Typ)

Instances

 Show TVE

type TVEM = State TVESource

TVE is the state of a monadic computation

Allocate a fresh type variable (see the first component of TVE)

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

The unification. If unification failed, return the reason

If either t1 or t2 are type variables, they are definitely unbound

Unify a free variable v1 with t2

occurs :: TVarName -> Typ -> TVE -> BoolSource

The occurs check: if v appears free in t

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

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.

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)

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)