2
$\begingroup$

Modern type theories (e.g. Calculus of Constructions) seem to effect an extensional conflation of dependent and polymorphic types. E.g., in Coq, after declaring

Variable n: forall (x:Prop), x.

n, a polymorphic (function) term, has both a dependent (depending on x) and a polymorphic (over Prop) type. So the dependent/polymorphic distinction becomes merely intensional in these theories1, reducing to that of a perspective. Is this analysis correct or am I missing something? Also, can one pull off dependent types w/out polymorphism in Coq? Vice versa it's possible, as we can get (subtype) polymorphism w/out dependent types:

Parameter natT:> nat -> Type.
Check 1: nat. Check 1: Type.  


1 On the other hand, due to the Curry-Howard isomorphism, first-order logic corresponds to dependent and second-order logic to polymorphic types. However, my understanding is that the (second-order) polymorphic terms still have dependent types -- just not dependent on terms but on types. (Is this correct?)

$\endgroup$
4
  • $\begingroup$ What makes $\mathsf{Prop}$ a "polymorphic type" here? It's perfectly possible to have a useful language in which $\mathsf{Prop}$ is just an ordinary type. $\endgroup$ Jan 20, 2018 at 11:10
  • $\begingroup$ (Intuitionistic) Second-order propositional logic corresponds to the polymorphic lambda calculus. Second-order propositional logic is usually not what people mean by "second-order logic". Indeed, classical second-order propositional logic is trivially reducible to classical propositional logic. The distinction between having and not having dependent types roughly corresponds to the distinction between predicate logic and propositional logic. Most popular dependently typed systems correspond to (at least partially) higher-order (predicate) logics. $\endgroup$ Jan 21, 2018 at 22:21
  • $\begingroup$ @MaliceVidrine: You've misunderstood: forall (x:Prop), x is the polymorphic type (as I wrote, polymorphic over Prop) $\endgroup$
    – jaam
    Jan 22, 2018 at 11:54
  • $\begingroup$ @jaam - Ah, I see, that makes it clearer. $\endgroup$ Jan 22, 2018 at 16:49

1 Answer 1

3
$\begingroup$

Much of your question is unclear. I'm going to attempt an end run around it.

The lambda cube is a collection of related type theories that are individually important and serve as archetypical systems. (That said, I sometimes get the impression that people put too much significance on the lambda cube. It is nowhere near comprehensive.)

The simplest system in the lambda cube is $\lambda\!\!\to$, the simply typed lambda calculus. From $\lambda\!\!\to$ there are three directions (axes) we can go. We can add the ability for terms to depend on types producing $\lambda2$, the polymorphic lambda calculus. We can add the ability for types to depend on types producing $\lambda\underline\omega$, the simply typed lambda calculus with operators. Finally, we can add the ability for types to depend on terms producing $\lambda P$, the dependent lambda calculus. "Dependently typed" always refers to types depending on terms. Other possible dependencies (potentially between sorts not mentioned) are not referred to as "dependent types". This is just what "dependent types" means, types that depend on terms. (Note, in $\lambda\!\!\to$, terms can depend on terms. That's what lambda abstraction does.) There is no (trivial, at least) embedding of any of these three extensions into the others.

In particular, a type like $\forall \alpha.\alpha\to\alpha$ in $\lambda2$ has no counterpart in $\lambda P$, i.e. $\lambda P$ cannot express a polymorphic identity function. Conversely, a type like $\Pi n:\mathbb N.n+n > n$ in $\lambda P$ has no analogue in $\lambda2$. So you can have dependently typed lambda calculi without (parametric) polymorphism and polymorphic lambda calculi without dependent types.

I don't know why you bring up subtyping at all, but most lambda calculi with subtyping in the literature are usually variations of the polymorphic lambda calculus ($\lambda2$) also known as System F. In particular, one of the most notable such systems is System F${}_{<:}$. If you wanted to talk about pre-generics Java (i.e. Java before Java 1.5), you potentially wouldn't even need parametric polymorphism, e.g. you could work within a simply typed lambda calculus extended with subtyping. Nothing stops you from combining subtyping and dependent typing, though. Subtyping is a different feature altogether and adding it takes you off the lambda cube entirely (which, as I mentioned before, is perfectly okay).

The Calculus of Constructions is equivalent to the system produced by adding all three extensions simultaneously. For the purposes of polymorphism, and not thinking in terms of the lambda cube, the key addition over $\lambda P$ is a universe, i.e. a "type of types". Let's use $\mathcal U$ to notate it. (It is often called $\mathsf{Type}$ or $\mathsf{Set}$.) With $\mathcal U$ added to $\lambda P$, call the system $\lambda P+\mathcal U$ we can easily embed $\lambda2$ by turning quantifications over types into abstractions over terms of type $\mathcal U$, e.g. $\forall \alpha.\alpha\to\alpha$ becomes $\Pi \alpha:\mathcal U.\alpha\to\alpha$. That said, within $\lambda P + \mathcal U$, we'd want $\forall \alpha.\alpha\to\alpha$ to mean something more, and, in particular, we would expect that you could instantiate a term of that type to $\mathcal U$. We can't apply a term of type $\Pi \alpha:\mathcal U.\alpha\to\alpha$ to $\mathcal U$ though since it is not the case that $\mathcal U : \mathcal U$. This can be added as an axiom, but it is inconsistent. Another question is whether $(\Pi \alpha:\mathcal U.\alpha\to\alpha):\mathcal U$. If it is, then $\mathcal U$ is called impredicative, otherwise it is predicative. In Coq, $\mathsf{Prop}$ is impredicative but $\mathsf{Set}$ is not. This is one of the major distinctions between $\mathsf{Prop}$ and $\mathsf{Set}$. In the (impredicative) Calculus of Constructions as described on Wikipedia, what it writes as $\forall x:\mathsf{P}.e$ would correspond to $\Pi x:\mathsf{Prop}.e$, while what it writes as $\forall x:\mathsf{T}.e$ would correspond to $\forall x.e$.

$\endgroup$
4
  • $\begingroup$ OK, so the notion of "dependent type" has the precise technical meaning of "a type depending on a term", and consequently (on the lambda cube) only $\lambda P$, $\lambda P2$, $\lambda P\underline{\omega}$ and $\lambda P\omega$ have dependent types? But since "polymorphic type" has the meaning of a type whose operations are applicable to values of more than one type, all theories on lambda cube except $\lambda\!\!\rightarrow$ and $\lambda P$ have polymorphic types? $\endgroup$
    – jaam
    Jan 25, 2018 at 13:27
  • 1
    $\begingroup$ In the context of lambda calculi, "polymorphic" virtually always means "parametric polymorphism". This would be the systems $\lambda2$, $\lambda\omega$, $\lambda P2$, and $\lambda P\omega$ in the lambda cube. $\lambda\underline\omega$ just means you have type expressions like $(\lambda x.x)\mathbb N$ or maybe $F(\lambda x,y.x)$. Even by that vague and informal definition of "polymorphism", $\lambda\underline\omega$ isn't "polymorphic". Cardelli's "definition" is trying to capture all the various things that have been called "polymorphism", and I think that is a mistake. $\endgroup$ Jan 25, 2018 at 21:24
  • $\begingroup$ So polymorphism is signaled by terms depending on a type (w/ types like $\forall x:Set.x$, etc.)? $\endgroup$
    – jaam
    Jan 26, 2018 at 12:27
  • $\begingroup$ Yes. A term (in normal form) of e.g. $\forall \alpha.\alpha\to\alpha$ looks like $\Lambda \alpha.\lambda x:\alpha.x$ in the polymorphic lambda calculus, $\lambda 2$. You can see that the subterm $\lambda x:\alpha.x$ has a free type variable ($\alpha$) which is then bound by the $\Lambda$. $\endgroup$ Jan 26, 2018 at 21:17

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .