Types and programming languages, Benjamin Pierce
Posted: 2016-07-31 , Modified: 2016-07-31
Tags: none
Posted: 2016-07-31 , Modified: 2016-07-31
Tags: none
\(\mu\) is a recursion operator for types. A definition \(T = \mu X. Y\) means: let \(T\) be the infinite type satisfying \(X=Y\).
Hungry = \mu A. Nat -> A
Stream = \mu A. Unit -> {Nat, A}
Process = \mu A. Nat -> {Nat, A}
Counter = \mu C. {get: Nat, inc: Unit -> C}Note: you can’t define Hungry in Haskell because (Then how does printf work? Something with type classes?)
Recursive types well-types the fixed-point combinator. \[ fix_T = \la f:T\to T.(\la x:(\mu A. A\to T). f (x x)) (\la x:(\mu A. A\to T). f (x x)) \]
Every type is inhabited (\(\la\_:(). fix_T (\la x:T.x)\)), so systems with recursive types are useless as logics.
[Embed untyped lambda calculus]
There are 2 basic approaches to recursive types. What is the relationship between the type and its one-step unfolding?
unfold and fold going both ways. (Ex. Haskell)Note equi-recursive places more demands on the typechecker.
Theorem (Knaster-Tarski): Let \(X\) be a poset, \(f:X\to X\) be order-preserving. Then there exists a fixed point, \(\sup\set{x\in X}{x\le f(x)}\).
Let \(\cal U\) be the universal set. Consider \((\cal P(\cal U), \subeq)\). Say \(X\) is \(F\)-closed/consistent if \(F(X)\subeq/\supeq X\).
Corollary. The intersection/union of all \(F\)-closed/consistent is the least/greatest fixed point of \(F\), denoted by \(\mu F, \nu F\).
(Principle of induction/coinduction) If \(X\) is \(F\)-closed, \(\mu F\subeq X\); if \(X\) is \(F\)-consistent, \(X\subeq \nu F\).
Finite tree types are given by
T = Top | (T, T) | T -> T Infinite tree types are like this but the tree can be infinite.
Say \(T<:Top\), \(S_1<:T_1, S_2<:T_2 \implies (S_1\times S_2)<:(T_1,T_2)\) and similarly for \(\to\). Take the transitive closure to get the subtyping relation.
A tree type is regular if subtrees(T) is finite.
T = X
| Top
| T x T
| T -> T
| \mu X. T“Keep substituting” \(\mu X. T\) to get the tree type corresponding to the \(\mu\)-type, treeof\(([X\mapsto \mu X. T]T)(\pi)\).
2 questions:
Constraint typing: \(\Ga \vdash t:T|_{\cal X} C\) means “term \(t\) has type \(T\) under assumptions \(\Ga\) whenever constraints \(C\) are satisfied.” \(\cal X\) tracks type variables introduced in each subderivation.
(This is a hybrid between the normal deductive system, and the bottom-up constraint generation system.)
Not allowed: doubleFun:\(\forall a . (\forall f : a\to a) \to a \to a\) defined by
let doubleFun = \f x -> f (f x)Reason: a polytype cannot appear inside ->.
T-LetPoly: \[ \frac{\Ga \vdash [x\mapsto t_1]t_2:T_2 \quad \Ga \vdash t_1:T_1}{\Ga \vdash \text{let }x=t_1\text{ in }t_2:T_2}. \] Instead of calculating a type for \(t_1\), it substitutes \(t_1\) in the body. I.e., perform a step of evaluation before calculating types.
Problem: If the body contains many occurrences, we have to check once for each occurrence. This can take exponential time. See p. 333-4 for solution. Worst-case is still exponential, but in practice it is essentially linear.
We need to abstract out a type from a term and instantiate the abstract term with concrete type annotations.
Equivalent to polymorphic lambda-calculus a.k.a. 2nd-order lambda calculus because it corresponds to 2nd-order intuitionistic logic, which allows quantification over predicates (types) not just terms.
New terms are
Impredicative: definition involves thing being defined. \(T=\forall X.X\to X\) ranges over all types, including \(T\) itself.
Predicative/stratified: range is restricted to monotypes.