2
$\begingroup$

In the introduction of the book by B.Jacobs, "Categorical Logic and Type Theory" (it's online here), he classifies type systems into three general flavours: Simply typed ones, depended typed (term depended types) and polymorphic types (type depended types). He says also there are also mix types.

Now if you start out with a dependently types theory and introduce transitive universes, hence forcing types on the level of terms, are you automatically speaking of a polymorphic type system then?

$\endgroup$
3
$\begingroup$

These three “flavors” are usually presented as the lambda cube. They aren't really flavors but properties that can be combined independently, so there are not $3$ but $2^3 = 8$ flavors. In fact you could go as high as $4$ properties yielding $16$ flavors:

  • terms depending on terms, i.e. functional languages (e.g. $f : x \mapsto x+2$);
  • terms depending on types, i.e. polymorphism (e.g. $\mathrm{head} : [X] \rightarrow X$);
  • types depending on types, i.e. type operators (e.g. $\mathrm{list} : X \mapsto [X]$);
  • types depending on terms, i.e. dependent types (e.g. $\mathrm{array(int)} : n \mapsto \mathrm{int}^n$).

Theories without lambda abstraction tend to be less interesting and do a bad job of encoding most programming languages, so they're generally left out.

If you introduce transitive universes, then having types depending on terms automatically gives you types depending on higher-order terms, i.e. types. The Barendregt cube tends to collapse when terms and types are collapsed. However this doesn't necessarily give you all the polymorphism you want. The Barendregt cube is a classification; it doesn't reflect all the properties of the language. In particular, polymorphism can be more or less explicit, requiring you to thread type arguments down to every function, or not.

I think the right way to put it is that you're automatically speaking of a type system that can encode a polymorphic type system, but not necessarily give it to you the way you want.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.