The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Hi Greg,

I was thinking about your email – sorry fir the slow process.

From: <coq-club-request AT inria.fr> on behalf of Greg Morrisett <morrisett AT gmail.com>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Friday, 3 March 2017 at 13:25
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] injectivity of inductive type implies False

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.   

I am not convinced that this does the job. What if I give enough information so that you know the type I mean. E.g.

Parameter MyNat : Set

Parameter myZero : MyNat

Parameter mySucc : MyNat -> MyNat

Parameter myInduction : …

In HoTT I can even show that Nat = MyNat. It seems to me that this parametrisation trick only works for simple type system. 

I mean I may want to know that both Age and Salary are represented by natural numbers but I don’t want to mix them up. This may also be related to adding dimensions to your type system.

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

I didn’t claim I have a solution to all these issues. However, I view nominal typing as something I put on top of my core structural type system. And my intuition is that the names should be fresh and unique – however this is achieved.

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.  

Precisely!

Thorsten

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

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.