The Coq mailing list

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

I exchanged some more emails with morrisett, focusing on nomina types
vs structural types in the context of records.
By reading this new message, I think I can make my example also with
simple type constructors:

If library A defines

type aT =
    | Name1 of int
    | Name2 of int * int;;

and library B independently defines

type bT =
    | Name1 of int
    | Name2 of int * int;;
where by pure coincidence name Name1 and Name2 are the same
If we have a type system able to recognize that aT==bT, then the user
of A and B can use those
interchangeably.
Then, if Library B want to alpha-rename its Name1 into Name1Bis, there
is no way to transmogrify this
rename on the code that uses A and B.
I think this is quite of a big problem, and it means that
"conceptually" the meaning of Name1 is set in stone as a global
concept that all humanity should agree upon when any library using
Name1 is first released.
What are your views on this issue?
(yes, module abstraction would hide those names, but then we loose the
possibility of doing case analysis, that can be recover if the module
offers specific functions, but it seams very indirect)


type binary_tree = Leaf of int | Tree of binary_tree * binary_tree
On 17 March 2017 at 18:31, Thorsten Altenkirch
<Thorsten.Altenkirch AT nottingham.ac.uk>
 wrote:
> nominal types require the meta-theory to support some notion of freshness or
> gensyming which makes the