Re: Semantics of free datatype in presence of subsorting

["Peter D. Mosses" <pdm@daimi.aau.dk>]

> [Dear Semanticists,
>
> It seems that the problem with overloading caused by free data types
> in the context of order-sorted signatures found some solution,
> accepted at least by the people directly involved in the work on this
> topic. Here is the remaining correspondence, following the earlier
> messages indicating the problem. Please note that towards the end,
> Till's proposal in fact contains a small adjustment to the language
> design. Any further comments welcome, also perhaps to the language
> design list.

As nothing about this has appeared yet on the cofi-language mailing
list, I'm submitting this reaction only to cofi-semantics for now (and
omitting most of the original message).  I'm in the process of trying
to list the changes to be implemented in v1.0 of the CASL Summary, and
I'd like to be quite sure that we aren't missing any opportunities for
simplification before proposing language design changes.

> Below:  AH = Anne Haxthausen (in consultation with Maura Cerioli, I understand)
> 	TM = Till Mossakowski
> 
> AT]
> ...
AH> >>1 Overloaded constructors
AH> >>
AH> >>  free datatype s = f(s1)|f(s2)
AH> >>
AH> >>  where s1 and s2 have a common subsort s0
AH> >This is clearly ruled out as ill-formed by the condition about
AH> >no common subsorts, so I do not see a problem here.
AH> 
AH> The language summary only says "all the sorts that are embedded in
AH> the declared sort by the alternatives must have no common
AH> subsorts". It does not say that the domains of overloaded
AH> constructors must not have no common subsorts.
AH> So this case is not ruled out as far as we can see.

TM> Oh yes, you are right.
TM> So this example has to be ruled out as well (and indeed it is ruled
TM> out by my suggestion).

Have you considered imposing the following condition instead?

  The alternatives of a free datatype must have no terms in common
  (with variables ranging over any sorts that are used but not declared
  by the datatype declaration).

I think that this subsumes not only 1 above, but also 2 below:

AH> >>2 Interaction between embedding
AH> >>
AH> >>   free datatype s = s1 | s2
AH> >>
AH> >>   where s1 and s2 have no common subsort, but for which a term t
AH> >>   exists with both sorts. The simplest (and most useless) case
AH> >>   is if a constant k exists for both sorts (but in general it applies
AH> >>   to functions f:w --> s1, f: w' --> s2 with a common w0<w and w0<w')
...

Regarding the following:

TM> "A free datatype must not contribute in any way to the
TM> overloading relation. In particular, this means that all the 
TM> constructors of the free datatype must neither be
TM> in the overloading relation with each other nor with functions
TM> in the local environment. Further, the introduction of new
TM> subsort relationships through the free datatype must not
TM> lead to the addition of profiles from the local environment 
TM> to the overloading relation."

AH> I like the suggestion by Till.  

I'm afraid that the above would seem overly complicated in the CASL
Summary...  Wouldn't it be enough to extend my proposal above with
something like:

  For each sort, the terms must also be distinct from those
  expressible using operations from the local environment (with
  variables ranging over the sorts declared in the latter). 

The motivation for these formulations is that most users may prefer to
regard the values of free datatypes as terms, and it may be helpful to
formulate conditions on this basis.  In fact it might be even gentler
to say first:

  The alternatives of a free datatype must have no ground terms in
  common with each other, nor with the local environment.
  
and then add:

  When the datatype declaration uses sorts from the local environment,
  the terms considered allow also variables over these sorts.

Sorry for my tardiness in reacting - also if I've overlooked some
obvious or previously-considered drawback to my proposals above.

Best regards

Peter