18
$\begingroup$

This page asserts that

many languages do not use implicit subtyping (structural equivalence), prefering explicit/declared subtyping (declaration equivalence)

I've mostly used programming languages which uses explicit subtyping. What are the advantages of implicit subtyping, as described in the notes above.

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ From the FAQ, on the scope of this exchange: "Work in this field is often distinguished by its emphasis on mathematical technique and rigor." I'm downvoting because I don't see any scope for rigor in the answers to this question. $\endgroup$
    – David Eppstein
    Commented Dec 28, 2010 at 3:59
  • 6
    $\begingroup$ Sadly, there is vastly more scope for rigor in answering this question than you might initially hope for. A lot of very eminent people burned a lot of the 90s wrestling with apparently trivial questions about subtyping. It's an area with a very poor effort-to-reward ratio, unfortunately. $\endgroup$
    – Neel Krishnaswami
    Commented Dec 28, 2010 at 9:55
  • 6
    $\begingroup$ yes, there is a lot of room for mathematics and rigor in answering this question, or at least to explain mathematically what implicit subtyping is. I am not sure about the effort-to-reward ratio. $\endgroup$
    – Noam Zeilberger
    Commented Dec 28, 2010 at 13:41
  • 1
    $\begingroup$ I probably should have just said it was "very hard", since upon reflection I realize I am very interested in the answers. $\endgroup$
    – Neel Krishnaswami
    Commented Dec 28, 2010 at 19:26
  • 1
    $\begingroup$ Ok, I'm convinced. I'd remove my downvote but the system won't let me. $\endgroup$
    – David Eppstein
    Commented Dec 28, 2010 at 19:48

2 Answers 2

Reset to default
19
$\begingroup$

The short answer is "to verify additional properties of existing code". Longer answer follows.

I am not sure "implicit" vs "explicit" is good terminology. This distinction is sometimes called "structural" vs "nominal" subtyping. Then there is also a second distinction in the possible interpretations of structural subtyping (described shortly). Note that all three interpretations of subtyping really are orthogonal, and so it doesn't really make sense to compare them against each other, rather than understanding the uses of each.

The main operational distinction in interpreting a structural subtyping relation A <: B is whether it is witnessed by a real coercion with (runtime/compiletime) computational content, or whether it can be witnessed by the identity coercion. If the former, the important theoretical property that has to hold is "coherence", i.e., if there are multiple ways to show that A is a substructural subtype of B, each of the accompanying coercions have to have the same computational content.

The link you gave seems to have the second interpretation of structural subtyping in mind, where A <: B can be witnessed by the identity coercion. This is sometimes called a "subset interpretation" of subtyping, taking the naive view that a type represents a set of values, and so A <: B just in case every value of type A is also a value of type B. It is also sometimes called "refinement typing", and a good paper to read for the original motivation is Freeman & Pfenning's Refinement types for ML. For a more recent incarnation in F#, you can read Bengston et al, Refinement types for secure implementations. The basic idea is to take an existing programming language that may (or may not) already have types but in which types do not guarantee all that much (e.g., only memory safety), and consider a second layer of types selecting subsets of programs with additional, more precise properties.

(Now, I would argue that the mathematical theory behind this interpretation of subtyping is still not as well understood as it should be, and perhaps that is because its uses are not as widely appreciated as they should be. One problem is that the "set of values" interpretation of types is too naive, and so sometimes it is abandoned rather than refined. For another argument that this interpretation of subtyping deserves more mathematical attention, read the introduction to Paul Taylor's Subspaces in Abstract Stone Duality.)

Improve this answer
$\endgroup$
7
  • $\begingroup$ Hi Noam, nice answer! I will add that nominal subtyping a la OO is fundamentally a way of defining a class of non-identity coercions which are nevertheless realized by no-ops. That is, the width subtyping of objects induced by inheritance formally involves a non-identity coercion (eg, a coercion $A \times B \times C <: A \times B$ means you throw away the $C$), but by laying out records sequentially in memory you can use the same binary code to project out $A$ and $B$ components for both types. $\endgroup$
    – Neel Krishnaswami
    Commented Dec 28, 2010 at 15:24
  • 1
    $\begingroup$ It is the job of the optimizer to figure out the optimal memory layout, so coercions which are identities should really be the result of optimization. $\endgroup$
    – Andrej Bauer
    Commented Dec 28, 2010 at 19:19
  • 2
    $\begingroup$ so just to clarify Andrej's comment with respect to my answer, in a refinement typing interpretation, subtyping relationships are always witnessed by the identity coercion by definition, because the refinement types carry no extra computational content. In other words, if A and B are two refinements ("subsets"/"properties") of a type of values X, A <: B asserts that for every value x in X, if x:A then also x:B. Such a statement can be verified or falsified, but it has no effect at runtime, since the proofs that x:A and x:B do not exist at runtime. $\endgroup$
    – Noam Zeilberger
    Commented Dec 29, 2010 at 11:00
  • 1
    $\begingroup$ @Noam: I agree, but only when we're talking about the metatheory of a single language, and not if we're talking about compilation. Identity coercions can be realized by procedures which do a lot of work, and non-identity coercions can be realized by procedures which don't do anything. Concretely, suppose that we have a type $\mathbb{N}$, and a refinement $\{x:N\;\;|\;\;x < 2^{32}\}$. Then we could implement elements of the refinement with a single unboxed word, even though the full type requires memory allocation to represent. The identity coercions here must be realized by real computation. $\endgroup$
    – Neel Krishnaswami
    Commented Dec 29, 2010 at 14:54
  • 3
    $\begingroup$ @Neel: I would divide it into two steps, 1. apply the computation--free identity coercion from $N$ to its refinement $\{x:N | x < 2^{32}\}$, then 2., apply the partially-defined coercion from $N$ to the (completely separate) type of single unboxed words, which is totally-defined on the refinement $\{x:N | x < 2^{32}\}$. Maybe that's splitting hairs...but in any case this goes to show what I said "that the mathematical theory behind this interpretation of subtyping is still not as well understood as it should be" :) $\endgroup$
    – Noam Zeilberger
    Commented Dec 29, 2010 at 15:36
4
$\begingroup$

This answer is a sort of minimal supplement to Noam's excellent answer. One data point of interest is the fate of C++ concepts, which foundered on an attempt to unify nominal and structural notions of type.

There's an excellent writeup here, with links to much of the relevant discussion: http://bartoszmilewski.wordpress.com/2010/06/24/c-concepts-a-postmortem/

However, the above writeup doesn't discuss the nominal vs. structural issue in any depth. There's another writeup here, which does: http://nerdland.net/2009/07/alas-concepts-we-hardly-knew-ye/

The key paper both point to is Bjarne Stroustrup's “Simplifying the Use of Concepts”: http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2009/n2906.pdf, which goes into the practical issues encountered in some depth.

As a whole, the discussion is more pragmatic than rigorous. However, it gives a good insight into the sorts of tradeoffs involved in these issues, especially in the context of a large existing language.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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