The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

> The tension between structural and nominal typing is an old one. I would
> nominal typing as an extension [..] a nominal type is a type
> with a name (or a stamp) and that there is an implicit coercion between
> nominal types and types.

While many seams to fancy this encoding of nominal type, this approach
is failing to capture their most important feature: allowing proper
development using libraries (or just different teams).
This is hard in structural typing since it logically assumes that any
method/field name to have a global meaning.
In practice, this prevents from any semantic preserving "method
rename" refactor to be applied. The names of fields/methods are like
global variables that can not be alpha-renamed, and that seams to go
against the most fundamental principles of functional programming.

Note how putting fancy contracts on methods does not help here, since
the empty contract would still be a subtype of the chosen one, still
preventing alpha renaming (in a library setting)

Nominal(sub) typing in its purest form allows for each method to be
introduced in exactly one point (and possibly overridden/implemented
somewhere else)
In this way, that method name is properly logically scoped under such
(for example) interface declaration.

(Yes, Java and other "nominal" languages have some issues here and
there still preventing proper alpha renaming... :-( )