The Coq mailing list

[Greg Morrisett <morrisett AT gmail.com>]

While I don't completely disagree with what you're saying, I think you're confusing abstraction and nominal typing.  Abstraction supports the kind of refactoring and parallel development to which you're referring --- I can give a single point of definition that supports easy change.  e.g.,

  Definition complex : Set  := (Q * Q).

  Definition add (c1 c2:complex) := (* e.g., cartesian addition *)

  ... development using complex and add ...

or better yet:

  Section Complex.

     Parameter complex : Set.

     Parameter add : complex -> complex -> complex.

      ... development using complex and add

  End Complex.

since this prevents me from using the definitional equality for the complex type and add operation.  A third option would be to abstract over a type-class, a module, etc.  No nominal types needed.   

And, since abstraction is (typically) scoped, it doesn't have to be "global" in the sense you suggested.  In the Section example above, there's no conflict with the names I've chosen outside the scope of the Section.  If anything, it's the *nominal* stuff that's problematic from a scoping standpoint since it doesn't alpha-vary the way that abstracted variables do. 

Finally, nominal types require the meta-theory to support some notion of freshness or gensyming which makes the meta-theory imperative --- something that I find ironic in the context of type-theory.  This, in turn, makes it difficult to support internalizing the meta-theory, and to support abstraction, requires us to add linguistic features such as sharing constraints (i.e., path aliases) in order to support certain naturally occurring patterns (e.g., the diamond pattern for module abstraction.)  

And, when we want to write polytypic definitions (e.g., the deriving clauses for a Haskell data type, or the decidable_equality for a Coq inductive), we can't just write the definition once and for all based on structure. 

I'll agree that some judicious use of nominal/generative types is useful in practice, but languages such as Java go overboard and fail to provide the structural definitions that are just as, if not more important.  Personally, I wish that Coq, ML, Haskell, etc. would give me the option when declaring an inductive/datatype as to whether or not I want it to be generative.  That is, I'd prefer to have a separation between an abstraction and a stamped, generative definition.  

-Greg

On Fri, Mar 3, 2017 at 7:47 AM, Marco Servetto <marco.servetto AT gmail.com> wrote:

> 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... :-( )