archives

Existential Types == Guarded Types

In the GHC Users' Guide:
Notice that GADTs generalise existential types.

And Martin Sulzmann gives us A Systematic Translation of Guarded Recursive Data Types to Existential Types

GADTs + Extensible Kinds = Dependent Programming

Tim Sheard claims that usual functional programming methods (plus two new features found in his new programming language Ωmega) take care of some of the needs dependent types are often thrown at.