Pi02B

23 universal types

Variants of polymorphism

parametric Polymorphismen with type variables, as elaborated in systemF
ad-hoc polymorphism: different behaviour on different types, e.g. overloading
multi-method displatch is a generalization, e.g.CLOS iallows that methods can be specialized upon any or all of their required arguments, not only the receiver
intensional polymorphism or even more general with patterns...

systemF lamda calculus extended with Type Variables etc.

λX.t # type abstraction
t[T] # type application
λX.t # value type abstraction
X # term type variable
∀X.T # universal type
Γ,X # context type variable binding
{`(Gamma,X\ |--\ t: T)/(Gamma |--\ lambda X. t: AA X.T)`} # typing: Type abstraction
{`(Gamma,X\ |--\ t: AA X.T)/(Gamma |--\ t[U]: [X |-> U] T)`} # typing: Type application
type erasure as above.Wells 1994. given a closed untyped term, it is undeciable to decide whether there is a well type term in System F wich erases to it

existential types are similar to module systems, with packing/unpacking types from a module.

parametric polymorphism cannot handle a situation like: modify an argument and return it: we need to say that it returns the type of the argument but must be a subtype to allow the operation
thus, extend systemFl with subtype relation and refine universal types with subtyping constraints

(i) kernel F_<:

λX<:T.t # term type abstraction is always bounded, unbounded quantification is derived as λX<:Top.t
∀X<:T.T # universal type
... # all rules are adapted similarly
{`(Gamma, X <: U |-- S <: T) / (Gamma |-- AAX <: U.S <: AAX <: U . T)`} # subtyping ∀ - kernel rule
scoping is not obvious from the rules, but crucial. e.g. X<:a:Nat, b:X}
- FboundedQuantification: defines a recursive type, or more generally could allow mutual recursive types
- is illegal (for system F_<: discussed here)

(ii) Full F_<:

kernel compares quantified types only if bounds are equal, this is lifted here by
{`(Gamma |-- T_1 <: S_1\ \ Gamma, X <: T_1 |-- S_2 <: T_2) / (Gamma |-- AAX <: S_1.S_2 <: AAX <: T_1 . T_2)`} # subtyping ∀ - full rule: contravariant on left-side, covariant on right-side

Theorems Safety: Preservation (if Γ ⊢ t :T and t → t' then Γ ⊢ t' : T) and Progress (if t closed, well.typed then either t is a value or ∃t → t')

kinds "type of types"

* # kind of proper types
* ⇒ * # type operations i.e. function from proper types to proper types
* ⇒ * ⇒ * # kind of functions from proper type to type operators i.e. 2-argument operators
(* ⇒ *) ⇒ * # kind of function from type operators to proper types

we extend systemF by giving a type to each TypeVariable X :: K

X :: K . T # Type typeOperator abstraction
T T # Type typeOperator application
Γ , X::K # context type variable binding
* #kind of proper types
* ⇒ * #kind of operators
{`(X::K in Gamma) /(Gamme |-- X :: K)`} # Kinding rule for Variable, analoguous for abstraction, application and arrow
{`(S_1 -= S_2\ \ T_1 -= T_2) / (S_1 -> S_2\ -=\ T_1 -> T_2))`} # typeEquivalence arrow analoguous equivalence, abstraction ....
these are 3 additions to simpy typed lambdaCalculus
1. rules of kinding: how to combine type expression
2. whenever a type appears, we must check, it is well formed i.e. has kind *
3. rules for definition equivalence

System F_ω similar additions to systemF with universal types ∀X::K.T
Theorems: Preservation, Progress, is decidable
Hierarchy F_i with kinds K_i
- K₁ = {*} (?)
- K_i = {*} ∪ { J ⇒ K | J ∈ K_i-1 and K ∈ K'_i-1_ ' } (?)
- K_ω = ⋃K_i
F₁ only kind *, no quantification or abstraction over types => simply type lambda calculus
F₂ only kind *, quantification only over proper types => systemF

till now we have

missing is family by types index by terms! dependentTypes. e.g. allow to restrict a list to a list with n elements

<: gets even more complicated in F'_omega_?, than it was in systemF