24
$\begingroup$

Types and Programming Languages 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?

$\endgroup$
22
$\begingroup$

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.

$\endgroup$
  • 3
    $\begingroup$ 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? $\endgroup$ – John Salvatier May 10 '11 at 17:39
  • 3
    $\begingroup$ 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. $\endgroup$ – Dave Clarke May 10 '11 at 18:00
  • 2
    $\begingroup$ 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. $\endgroup$ – sclv May 10 '11 at 18:01
  • $\begingroup$ (changed from a comment to an answer) $\endgroup$ – Neel Krishnaswami May 10 '11 at 18:34
  • $\begingroup$ 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. $\endgroup$ – Charles Stewart May 12 '11 at 8:23
22
$\begingroup$

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's thesis for an example of adding subtyping to a dependent type theory (in this case, Twelf).

$\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.