Language.TEval.EvalN
Description
Untyped (nominal) lambda-calculus with integers and the conditional
http://okmij.org/ftp/Computation/Computation.html#teval
- 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]