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



Untyped (nominal) lambda-calculus with integers and the conditional

The Abstract of the lecture notes
We expound a view of type checking as evaluation with `abstract values'. Whereas dynamic semantics, evaluation, deals with (dynamic) values like 0, 1, etc., static semantics, type checking, deals with approximations like int. A type system is sound if it correctly approximates the dynamic behavior and predicts its outcome: if the static semantics predicts that a term has the type int, the dynamic evaluation of the term, if it terminates, will yield an integer.

As object language, we use simply-typed and let-polymorphic lambda calculi with integers and integer operations as constants. We use Haskell as a metalanguage in which to write evaluators, type checkers, type reconstructors and inferencers for the object language.

We explore the deep relation between parametric polymorphism and inlining. Polymorphic type checking then is an optimization allowing us to type check a polymorphic term at the place of its definition rather than at the places of its use.

Joint work with Chung-chieh Shan.

Version The current version is 1.1, July 2008. References lecture.pdf [199K]



data Term Source


type Env = [(VarName, Value)]Source

Environment: associating values with free variables

data Value Source


VI Int 
VC (Value -> Value) 


eval :: Env -> Term -> ValueSource

Denotational semantics. Why? How to make it operational?