Re: [CoFI] Revised proposal for CASL Views, Imports

[Didier Bert <Didier.Bert@imag.fr>]

   Dear friends,

>COMMENTS ARE SOLICITED - ESPECIALLY FROM ANYONE WHO OBJECTS TO THE
>ELIMINATION OF IMPLICIT FITTING VIEWS!
>

-------------------------------------------------------------------------
GENERAL COMMENTS:

- I agree with the permutation of "imports" and "params". This makes the
meaning and understanding easier.
- I agree also with the elimination of implicit views, in the sense that
I consider that an instantiation relies (basicly) upon two specification
morphisms and the notation with only specifications (as LIST[NAT]) can
induce a confusion or a misunderstanding. (See also, obviously, the
technical arguments of the discussion).

Nevertheless: we have to experiment the notation to see if it is not
too constraining for the user. I wonder whether operations like
"morphism
composition" should not be interesting to declare new views
(to be provided in the CASL-extensions, probably!).

-------------------------------------------------------------------------
DETAILED COMMENTS:

A- On the modification of the CASL summary (part: PROPOSED CHANGES
TO THE CASL SUMMARY):

A.1- The sentence just before 6.3:
        The instantiation is also undefined whenever the result is
        not a push-out.
Have we a characterization which avoid to refer to the "push-out"
notion?
I am afraid that the reader is discouraged to write and use any generic
specification if such conditions are required.

A.2- Since the point 6.3.2 is removed, then the number 6.3.1 is no more
useful.

-----
B- On the informal explaination (First part and their consequences in
the
rest of the document):

About the example of generic views:

  view LISTasELEM [ELEM]: ELEM to LIST[ELEM] = Elem |-> List end

It should be clear if the source specification (ELEM) is in the scope of
the parameter. We can interpret the instantiation:

  view LISTasELEM[view NATasELEM]

either as a view: NAT to LIST[view NATasELEM] = Nat |-> List
or:               ELEM to LIST[view NATasELEM] = Elem |-> List

I guess that it is the second one which is the right interpretation.
With the same example, the specification expression:

        LIST[view LISTasELEM[view NATasELEM]]

contains two instances of the sort "List", which are not distinguished.
Can we combine view instantiation and renaming? Must we use compound
identifiers?

-----
C- About the discussion (Last part). This comment can be skipped because
it is not developed in the (pure) CASL framework. However, it
illustrates
similarities and differencies between the "named specification"
approach and the unnamed (CASL) one.

Unique view expression vs. unique signature morphism.

In the framework where named morphisms are defined between named
specifications, the second mecanism (Till's one) is easily implementable
because source and target specification names are part of the named
specification morphism. And we can deal with specification morphisms,
not
simply signature morphisms. Semantic checking are confined at some
particular places. So, in the Andrzej's example, V, V0 and V1 have
distinct "dependent types", namely:
        view V : ELEM to NAT
        view V0: SOME0 to NAT
        view V1: SOME1 to NAT
even if they have same source signature and same mapping.

Moreover, this example is typically a case where we could have the
following
possibilities (that occur very often in writing specifications):

view S0 : ELEM to SOME0 end     -- implicit identity mapping
view S1 : SOME0 to SOME1 end

Then:
view V1 : SOME1 to NAT = ... (as it is)...
view V0 : SOME0 to NAT = S1;V1 end      -- morphism composition. No need
view V  : ELEM to NAT = S0;V0 end       -- of semantic checking
                                        -- if target(S1)= source(V1).
Now,
view VL [SOME0] : SOME0 -> LIST[SOME0] = ...
needs always a view from SOME0 to something to be correctly
instantiated.
So, clearly:
        view VL[view V]  is not okay,
        view VL[view V0] is okay,
        view VL[view V1] is not okay (excepted if we introduce again,
the
                         implicit view S1 at the right place!).

Best regards
Didier

-- 
----------------------------------------------------------------------------
Dr. Didier Bert                   
http://www-lsr.imag.fr/users/Didier.Bert/
CNRS, Laboratoire LSR-IMAG         Tel: 04 76 82 72 16      +33 476 82
72 16
681, rue de la Passerelle          Fax: 04 76 82 72 87      +33 476 82
72 87
BP 72 
38402 Saint-Martin-d'Heres CEDEX, France
----------------------------------------------------------------------------