<blockquote>
  <p>However, I am more interested in type theory as a foundation for mathematics than as a basis for programming languages, should I pay much attention to subtyping? </p>
</blockquote>

<p>One extra thing subtyping gives you is that subsumption implies that lots of coherence properties hold. A dependent type theory also needs a notion of proof irrelevance to model everything you can do with subtypes. For example, in dependent type theory you can approximate forming a subset with a dependent record: </p>

<p>$$
\{x \in S \;|; P(x)\} \mbox{ vs. } \Sigma x:S.\;P(x)
$$</p>

<p>However, note that the cardinality of the subset will be smaller than $S$, whereas the dependent record can have a bigger cardinality (since there can be many possible proofs of $P(x)$ for each $x:$). </p>

<p>To faithfully represent subtyping (which says that if $X &lt;: Y$, and $x:X$ then $x:Y$), you need $P(x)$ to be <em>proof-irrelevant</em> -- that is, for there to be at most one inhabitant of the type $P(x)$. </p>

<p>Once you have that, you can systematically elaborate subtyping into dependent type theory. See <a href="http://cs.cmu.edu/~wlovas">William Lovas</a>'s thesis for an example of adding subtyping to a dependent type theory (in this case, Twelf).  </p>

CC BY-SA 3.0
2011-05-10T18:38:42.050Z
2011-05-10T18:38:42.050Z
Neel Krishnaswami
<p>Subtyping and dependent types are orthogonal concepts. </p>

<p>Subtyping is typically equipped with a notion of subsumption, whereby an expression of one type can appear in place where a supertype is expected.</p>

<p>Subtyping is more likely to be decidable and is more simply to manage in implementation.</p>

<p>Dependent typing is vastly more expressive. But if you ever want to consider a group to also be a monoid, then you need a notion of subsumption to forget the extra structure. Often, such as when using Coq, a trivial proof obligation is generated to deal with this kind of coercion, so in practice subtyping may not add anything. What's more important is having ways of packaging together various theories to make them reusable, such as reusing the theory of monoids when talking about groups. Type classes in Coq are a recent innovation for doing such things. Modules are an older approach.</p>

<p>If you do a quick google of "subtyping dependent types" you find a bunch of work adding subtyping to dependent types, mostly from around the year 2000. I imagine that the meta-theory is really challenging, so no subtyping of dependent types appears in proof assistants.</p>

CC BY-SA 3.0
2011-05-10T17:39:54.770Z
Thank you, this is exactly what I was looking for. I have asked a couple of noob questions now that seem to have been somewhat well received even though cstheory.SE isn't the Right Place for such questions. On a scale of -5 to +5 would you encourage or discourage similar questions in the future? 

As a side note, as I understand it (from reading Robert Harper), type classes are a subcategory of modules, is that right?
John Salvatier
CC BY-SA 3.0
2011-05-10T18:00:24.147Z
This question is on the just right side of the border of what is suitable for cstheory.SE. Type classes are not really a subcategory of modules. It's more like type classes are modules+type inference+free_plumbing.
Dave Clarke
CC BY-SA 3.0
2011-05-10T18:01:15.597Z
I'd imagine that you can always model/simulate subtying with dependent types fairly easily. In Haskell, HList (which is just built on decidable type equality) gives you subtyping, for example (c.f. "Haskell's Overlooked Object System"). The only hard part about subtying is type inference, and once you're working with dependent types you've tossed 90% of that out anyway.
sclv
CC BY-SA 3.0
2011-05-10T18:34:28.213Z
(changed from a comment to an answer)
Neel Krishnaswami
CC BY-SA 3.0
2011-05-12T08:23:17.367Z
The subset theory of Martin-Loef's type theory is basically what you need to model structure forgetting, and that dates back to the 1980s.  I think this is sort of what @Neel is getting at in his answer.
Charles Stewart
CC BY-SA 3.0
2011-05-10T16:51:33.173Z
2011-05-10T17:03:29.967Z
2011-05-10T17:03:29.967Z
Dave Clarke
<p><a href="http://rads.stackoverflow.com/amzn/click/0262162091">Types and Programming Languages</a> focuses quite a bit on subtyping, but as far as I can tell, subtyping doesn't seem especially fundamental. Does subtyping give you anything more than dependent types do? Working with dependent types is bound to be more work, so I can understand why subtypes might be useful in practice. However, I am more interested in type theory as a foundation for mathematics than as a basis for programming languages, should I pay much attention to subtyping? </p>

<lo.logic><pl.programming-languages><type-theory>
Do dependent types give you everything subtyping does?
John Salvatier
# Do dependent types give you everything subtyping does?

(Asked by: username_0 on 2011-05-10)

[Types and Programming Languages](http://rads.stackoverflow.com/amzn/click/0262162091) focuses quite a bit on subtyping, but as far as I can tell, subtyping doesn't seem especially fundamental. Does subtyping give you anything more than dependent types do? Working with dependent types is bound to be more work, so I can understand why subtypes might be useful in practice. However, I am more interested in type theory as a foundation for mathematics than as a basis for programming languages, should I pay much attention to subtyping?

**Tags:** lo.logic, pl.programming-languages, type-theory

---

## 2 answers

### Answer by username_2 on 2011-05-10. Score: 24 | Accepted answer

Subtyping and dependent types are orthogonal concepts.

Subtyping is typically equipped with a notion of subsumption, whereby an expression of one type can appear in place where a supertype is expected.

Subtyping is more likely to be decidable and is more simply to manage in implementation.

Dependent typing is vastly more expressive. But if you ever want to consider a group to also be a monoid, then you need a notion of subsumption to forget the extra structure. Often, such as when using Coq, a trivial proof obligation is generated to deal with this kind of coercion, so in practice subtyping may not add anything. What's more important is having ways of packaging together various theories to make them reusable, such as reusing the theory of monoids when talking about groups. Type classes in Coq are a recent innovation for doing such things. Modules are an older approach.

If you do a quick google of "subtyping dependent types" you find a bunch of work adding subtyping to dependent types, mostly from around the year 2000. I imagine that the meta-theory is really challenging, so no subtyping of dependent types appears in proof assistants.

> **Comments:**
> **username_0**: Thank you, this is exactly what I was looking for. I have asked a couple of noob questions now that seem to have been somewhat well received even though cstheory.SE isn't the Right Place for such questions. On a scale of -5 to +5 would you encourage or discourage similar questions in the future?   As a side note, as I understand it (from reading Robert Harper), type classes are a subcategory of modules, is that right?  
> **username_2**: This question is on the just right side of the border of what is suitable for cstheory.SE. Type classes are not really a subcategory of modules. It's more like type classes are modules+type inference+free_plumbing.  
> **username_3**: I'd imagine that you can always model/simulate subtying with dependent types fairly easily. In Haskell, HList (which is just built on decidable type equality) gives you subtyping, for example (c.f. "Haskell's Overlooked Object System"). The only hard part about subtying is type inference, and once you're working with dependent types you've tossed 90% of that out anyway.  
> **username_1**: (changed from a comment to an answer)  
> **username_4**: The subset theory of Martin-Loef's type theory is basically what you need to model structure forgetting, and that dates back to the 1980s.  I think this is sort of what @Neel is getting at in his answer.  

---

### Answer by username_1 on 2011-05-10. Score: 24

> However, I am more interested in type theory as a foundation for mathematics than as a basis for programming languages, should I pay much attention to subtyping?

One extra thing subtyping gives you is that subsumption implies that lots of coherence properties hold. A dependent type theory also needs a notion of proof irrelevance to model everything you can do with subtypes. For example, in dependent type theory you can approximate forming a subset with a dependent record:

$$
\{x \in S \;|; P(x)\} \mbox{ vs. } \Sigma x:S.\;P(x)
$$

However, note that the cardinality of the subset will be smaller than $S$, whereas the dependent record can have a bigger cardinality (since there can be many possible proofs of $P(x)$ for each $x:$).

To faithfully represent subtyping (which says that if $X <: Y$, and $x:X$ then $x:Y$), you need $P(x)$ to be *proof-irrelevant* -- that is, for there to be at most one inhabitant of the type $P(x)$.

Once you have that, you can systematically elaborate subtyping into dependent type theory. See [William Lovas](http://cs.cmu.edu/~wlovas)'s thesis for an example of adding subtyping to a dependent type theory (in this case, Twelf).


---

