Structure
-- indeterminacy
Top = \E %a.%a
\zline{the biggest type}
AnyPair = \E %a \E %b.%a \* %b
\zline{any pair}
$(3,4):\E %a.%a
{\em -- does not provide sufficient structure!}
$(3,4):\E %a.%a \* %a
Information hiding
\E %a.%a \* ( %a->Int )
\zline{object, operation}
x : \E %a. %a \* ( %a->Int )
\zline{ \( \leadsto \)
snd ( x )( fst( x ))
}
slide
:
Existential types -- examples
