Combining Universal and Existential Quantification

• Combination
  • Universal quantification: generic types.
  • Existential quantification: abstract data types.
  • Combination: parametric data abstractions.

nil: forall a. List[a]
cons: forall a. (a x List[a]) $->$ List[a]
hd: forall a. List[a] $->$ a
tl: forall a. List[a] $->$ List[a]
Null: forall a. List[a] $->$ Bool

array: forall a. Int $->$ Array[a]
index: forall a. (Array[a] x Int) $->$ a
update: forall a. (Array[a] x Int x a) $->$ Unit