[CoFI] Re: question

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

------------------------------------------
[here comes Alexandres reply first  BKB]
from: "Alexandre Zamulin" <zam@iis.nsk.su>

Dear All,

I fully support Michel in his proposal. To my mind, the relations 
between compond sorts cannot be always deduced from the relations 
between the argument sorts. I believe that some kind of multi-level 
specifications is needed for this purpose, which is beyond the scope 
of CASL.

Best,

Alexandre.

------------------------------------------
From: "Peter D. Mosses" <pdm@daimi.aau.dk>

Till wrote:

> concerning Michel's proposal:

Alexandre's too, I guess.

> >My proposal would be to simplify CASL w.r.t. this issue, and just decide
> >that compound id do not interact w.r.t. subsorting relations (again,
> >***but*** for the special case of fitting morphism). Thus:
> >a) Nat < Int will not entail List[Nat] < List[Num], but the latter can
> >of course be explicitly specified by the user.
> >b) If in one generic spec we have Elem < List[Elem], and fit Elem to
> >Nat, then we have in the resulting spec Nat < List[Nat].
> >
> >I believe the above suggested modification is easily implementable both
> >in the summary and in the semantics.
> 
> From a design point of view, I agree with Michel and do not think
> that Bernd's proposal 
> 
> >As to you question: I think a better modelling would be to have a
> >supertype "Interval" or "Bounds" or so, of which "FromOneToTen" and
> >"FromOneToTwenty" would be subsorts, e.g. specified using a subsort
> >definition constraining the bounds. 
> 
> solves the problem, because you still have that
> ARRAY(FromOneToTen, Nat) is a subsort of ARRAY(Interval, Nat).

I too now support the proposal to modify the design.  What I hadn't
noticed before was that even though we don't have higher-order
function types in CASL, first-order types like ARRAY also exhibit
contravariance with respect to subtyping in their index argument,
i.e., ARRAY(S,T) corresponds closely to the function type S -> T.
Even though compound ids in CASL are not really proper type
constructors, they should at least behave consistently with them
regarding subtypes, to avoid surprises.

My recollection is that at the time we last discussed this issue
(Amsterdam in September?), we didn't see clear arguments either way,
and the decision reflected in v0.98/v0.99 was never regarded as a
particularly well-motivated one.  I personally favoured the assumption
of monotonicity (which also underlies my "unified algebras" framework). 
One can deal with types like ARRAY by letting them be dependent types
taking the lower and upper index values as numeric arguments:
ARRAY(1,10,Nat).  But this is admittedly a bit of a hack, and it
doesn't seem to be applicable in connection with compound ids.

Thanks to Alexandre for raising this issue again!

Cheers,

Peter Mosses (in the process of resurfacing...)

P.S. The Danish university net was down all weekend - sorry for any
problems with accessing the CoFI archives at brics.dk.  It should be
OK again now.