<p>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.</p>

<p>There's an excellent writeup here, with links to much of the relevant discussion: <a href="http://bartoszmilewski.wordpress.com/2010/06/24/c-concepts-a-postmortem/" rel="nofollow">http://bartoszmilewski.wordpress.com/2010/06/24/c-concepts-a-postmortem/</a></p>

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

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

<p>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.</p>

CC BY-SA 2.5
2011-01-04T16:39:59.820Z
2011-01-04T16:39:59.820Z
sclv
<p>The short answer is "to verify additional properties of existing code".  Longer answer follows.</p>

<p>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.</p>

<p>The main operational distinction in interpreting a structural subtyping relation A &lt;: 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.</p>

<p>The link you gave seems to have the second interpretation of structural subtyping in mind, where A &lt;: 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 &lt;: 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 &amp; Pfenning's <a href="http://www.cs.cmu.edu/~fp/papers/pldi91.pdf">Refinement types for ML</a>.  For a more recent incarnation in F#, you can read Bengston et al, <a href="http://research.microsoft.com/en-us/projects/f7/seven-csf08-paper.pdf">Refinement types for secure implementations</a>.  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.</p>

<p>(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 <a href="http://www.paultaylor.eu/ASD/subasd.pdf">Subspaces in Abstract Stone Duality</a>.)</p>

CC BY-SA 2.5
2010-12-28T15:24:02.810Z
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.
Neel Krishnaswami
CC BY-SA 2.5
2010-12-28T15:33:27.510Z
This kind of trick makes the hair on my neck stand up, because the interplay between contextual equivalence and realizability you need to show this works is really intricate. While doing the  proofs in any given case isn't that hard, I have no good sense of how they fit into the mathematical universe, since the general metatheorems about these techniques are (a) either not known or (b) call for more category theory than I currently possess.
Neel Krishnaswami
CC BY-SA 2.5
2010-12-28T19:19:42.977Z
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.
Andrej Bauer
CC BY-SA 2.5
2010-12-29T11:00:47.850Z
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.
Noam Zeilberger
CC BY-SA 2.5
2010-12-29T12:03:31.533Z
What about the following relationship between structural and nominal subtyping, in the form of translating a structural system into a nominal one: Our hierarchy of nominal types will be all possible record structures with subtyping between compatible structures. Then we translate a type A with the structure B to a subtype A <: B. Is that right? It's not terribly exciting, though.
Ohad Kammar
CC BY-SA 2.5
2010-12-29T14:54:49.760Z
@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.
Neel Krishnaswami
CC BY-SA 2.5
2010-12-29T15:36:32.660Z
@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" :)
Noam Zeilberger
CC BY-SA 2.5
2010-12-28T15:07:22.597Z
2010-12-28T16:41:27.047Z
2010-12-28T16:41:27.047Z
Noam Zeilberger
<p>This <a href="http://rigaux.org/language-study/types.txt">page</a> asserts that </p>

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

<p>I've mostly used programming languages which uses explicit <a href="http://en.wikipedia.org/wiki/Subtypes">subtyping</a>. What are the advantages of implicit subtyping, as described in the notes above.</p>

CC BY-SA 2.5
2010-12-28T03:59:22.413Z
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.
David Eppstein
CC BY-SA 2.5
2010-12-28T09:55:53.377Z
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.
Neel Krishnaswami
CC BY-SA 2.5
2010-12-28T13:41:06.717Z
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.
Noam Zeilberger
CC BY-SA 2.5
2010-12-28T19:26:39.730Z
I probably should have just said it was "very hard", since upon reflection I realize I am very interested in the answers.
Neel Krishnaswami
CC BY-SA 2.5
2010-12-28T19:48:19.157Z
Ok, I'm convinced. I'd remove my downvote but the system won't let me.
David Eppstein
<pl.programming-languages><type-theory>
Implicit vs explicit subtyping
Frankie Ribery
# Implicit vs explicit subtyping

(Asked by: username_0 on 2010-12-28)

This [page](http://rigaux.org/language-study/types.txt) 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](http://en.wikipedia.org/wiki/Subtypes). What are the advantages of implicit subtyping, as described in the notes above.

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

> **Comments:**
> **username_1**: 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.  
> **username_2**: 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.  
> **username_3**: 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.  
> **username_2**: I probably should have just said it was "very hard", since upon reflection I realize I am very interested in the answers.  
> **username_1**: Ok, I'm convinced. I'd remove my downvote but the system won't let me.  

---

## 2 answers

### Answer by username_3 on 2010-12-28. Score: 19 | Accepted answer

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](http://www.cs.cmu.edu/~fp/papers/pldi91.pdf). For a more recent incarnation in F#, you can read Bengston et al, [Refinement types for secure implementations](http://research.microsoft.com/en-us/projects/f7/seven-csf08-paper.pdf). 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](http://www.paultaylor.eu/ASD/subasd.pdf).)

> **Comments:**
> **username_2**: 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.  
> **username_2**: This kind of trick makes the hair on my neck stand up, because the interplay between contextual equivalence and realizability you need to show this works is really intricate. While doing the  proofs in any given case isn't that hard, I have no good sense of how they fit into the mathematical universe, since the general metatheorems about these techniques are (a) either not known or (b) call for more category theory than I currently possess.  
> **username_5**: 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.  
> **username_3**: 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.  
> **username_6**: What about the following relationship between structural and nominal subtyping, in the form of translating a structural system into a nominal one: Our hierarchy of nominal types will be all possible record structures with subtyping between compatible structures. Then we translate a type A with the structure B to a subtype A <: B. Is that right? It's not terribly exciting, though.  
> **username_2**: @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.  
> **username_3**: @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" :)  

---

### Answer by username_4 on 2011-01-04. Score: 4

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.


---

