Subsorts and compound identifiers

[pdmosses@brics.dk]

The following change to the Summary was introduced in v0.96,
reflecting an apparent agreement at the meetings in Paris and Lille:

Sect 6.2, pp. 21-22: 

  In general, subsort embeddings between component sorts do not induce
  subsort embeddings between compound sorts. For instance, consider a
  specification with Nat declared as a subsort of Int. When putting
  together two extensions of it with sorts (compound-id List Nat),
  respectively (compound-id List Int), one does not get 
  (compound-id List Nat) declared automatically as a subsort of 
  (compound-id List Int)--this has to be specified explicitly, if
  required.  

I cannot find the motivation for this change.  If I may quote from a
message from Andrzej to some of us (Tue, 29 Apr), in answer to my query:

> > Perhaps you might also remind me of the arguments against *always*
> > extending subsorting to compound sort identifiers when forming or
> > amalgamating signatures - these arguments are not in S-2, as far as I
> > can see.  The language summary will have to warn readers about the
> > lack of monotonicity.  (I recall now that Michel was worried about
> > this in Paris, but I missed the point then...)  [...]
>
> In S-2 we did not address this issue at all, leaving it for
> the subsorting group. If I recall right, the input from them was
> ambiguous: basically, we would like to get that subsorting does carry
> through compound identifiers usually, but there were some anomalies
> Till pointed out.

Till, would you please describe those anomalies?  Especially since
your comment on this point in (the annotated-discharged language
summary) S-1 v1.3 suggests resolving the question to confirm the v0.95
wording, whereas the dischargement contradicts your recommendation!

**********************************************************************
PROPOSAL:  Require subsorting between compound sort identifiers to be
compatible with subsorting between their components.
**********************************************************************

Sect 6.2, pp. 21-22: 

  Subsort embeddings between component sorts induce subsort embeddings
  between the compound sorts (but not vice versa). For example, when
  Nat is declared as a subsort of Int, we get automatically
  (compound-id Seq Nat) embedded as a subsort of (compound-id Seq Int)
  in signatures containing all these sorts.

  If there are two compound sorts with multiple components, and the
  number of components are the same, and each pair of corresponding
  components either consist of two identical IDs or of two sorts in the
  subsort relationship, then there also is a subsort embedding between
  the compound sorts.

  Instantiation also behaves as expected here: if in a generic
  specification we have Elem declared as a subsort of 
  (compound-id Seq Elem), where Elem is a parameter sort, then in the
  result of instantiation of Elem by Nat, one does get Nat automatically
  declared as a subsort of (compound-id Seq Nat).

Peter

[It's unfortunate that Peter didn't raise this issue on cofi-langauge
 earlier... Let's hope it can be resolved by Monday!  --PDM]