Maude-help mailing list

[Marc Boyer <Marc.Boyer AT onera.fr>]

Dear all,

I am not a all a maude expert, but since I am coding in maude for about
2 years, I have faced with some of the problems/questions presented
here.

So, my point of view could be different from others. And because I am
not sure that all concepts are understood the same way, I am going
to use code.

pbrowne a écrit :
> Michael,
> The expression problem can be described as the ability to add new
> variants (either constructors or methods) to a data type (or sort)
> without changing the existing code. The Haskell and OO language issues
> are well described at:
> http://stackoverflow.com/questions/870919/why-are-haskell-algebraic-data-types-closed

First, have a look on your expression problem, without subsorts.

It is well known from years (and this is the core of ADT) that
the ability of a code to evolve depends on the separation of the
implementation and the interface.

Let us define a "data type" Point, with a common constructor x/y
   sort Point .
   op cartPoint( _ , _ ) : Rat Rat -> Point [ctor] .
   op _ + _ : Point Point -> Point .

   vars x x' y y' : Rat .
   eq [cart-sum] :
      cartPoint( x , y ) + cartPoint( x' , y' ) = cartPoint( x + x' , y 
+ y' ) .

When adding a new polar representation.
   op polPoint( _ , _ ) : Rat Rat -> Point [ctor] .
then, the [cart-sum] equation no more matches...

Of course, the definition of the interface could be
  ops _.x _.y : Point -> Rat .
  eq ( cartPoint( x , y ) ).x = x .
  eq ( cartPoint( x , y ) ).y = y .
  vars rho theta : Rat .
  eq ( polarPoint( rho , theta ) ).x = rho * cos( theta ) .
  eq ( polarPoint( rho , theta ) ).y = rho * cos( theta ) .

and cart-sum could be re-written
  vars p p' : Point .
   eq [xy-sum] :
      p + p' = cartPoint( (p).x + (p').x , (p).y + (p').y ) .

Then, by defining clear public interface, we can have new constructors
and keep code of methods running (result of ADT studies).

We could also change the internal representation of a sort (adding a
attribute that was not identified at first analysis).

We could also define "better implementation", like
   vars rho' : Rat .
   eq [polar-rho-sum] :
      polarPoint( rho , theta ) + polarPoint( rho' , theta )
      =
      polarPoint( rho + rho' , theta ) .

The fact is there that it is no simple way to say to maude to use
polar-rho-sum instead of xy-sum when possible. We could of course add
an [owise] attribute to the xy-sum equation, but this is a one-shot
solution.


> With respect to Maude, here is my current *opinion*
> I *think* Maude supports subsort polymorphism that allows us to use
> elements of a subsort in the function’s rank (arity and co-arity).
> I *think* the Maude allows functions to be inherited and overridden in a
> subsort (a  bit like overriding and inheritance in object oriented
> languages methods).
> Therefore I *think* that a Maude sort can be extended by subsorting and
> adding a new method.

Now, let us turn to subsorts. Let us define a colored point, like in
common OO tutorial.

  sort ColoredPoint .
  subsort ColoredPoint < Point .

And we would like to have a function print, with different behaviours
for ColoredPoint and Point .

  My personal solution is the following.

  op coloredPoint( _ , _ , _ ) : Rat Rat Color -> ColoredPoint [ctor] .

  op Point( _ ) : ColoredPoint -> Point . *** Upcast, super
  ops _.x _.y : Point -> Rat .
  op _.color : Point -> Color .

  op print( _ ) : Point -> String .

  eq [upcast-cpt-pt] :
     Point( coloredPoint( x , y , c ) ) = cartPoint( x , y ) .
  var cpt : ColoredPoint .
  eq [cpt-x] ( cpt ).x = ( Point( cpt ) ).x .
  eq [cpt-y] ( cpt ).y = ( Point( cpt ) ).y .
  eq [cpt-color] ( coloredPoint( x , y , c ) ).color = c .

  eq [pt-print] :
     print( pt ) = "x=" + string( (pt).x , 10 ) +
                   " y=" + string( (pt).y , 10 ) .

  eq [cpt-print] :
     print( cpt ) = print( Point( cpt ) )
                   + " color= " + string( color ) .

But here, both pt-print and cpt-print could be used for a variable
a sort ColoredPoint (since is also have Point sort). We could solve
it by using matching with constructors, but is breaks the difference
internal representation / public interface.

My solution is to write what means late binding (also known as virtual
/ static in Java/C++).

Let us introduce one new sort SubPoint .
  sort SubPoint .
  subsort SubPoint < Point .
when defining ColoredPoint, it is defined as a SubPoint.
  subsort ColoredPoint < SubPoint .
and rewrite [pt-print] as [virtual-pt-print]
  ceq  [virtual-pt-print] :
     print( pt ) = "x=" + string( (pt).x , 10 ) +
                  " y=" + string( (pt).y , 10 )
     if not ( pt :: SubPoint ) .

And it is done.


Does these two patterns solve your "Walder expression problem"? I
don't know, but these are the two ones that I am currently using
in my maude code.

Best regards,
   Marc Boyer
--
Marc Boyer, Ingenieur de recherche                              ONERA
Tel: (33)  5.62.25.26.36                                         DTIM
Fax: (33)  5.62.25.26.52                          2, av Edouard Belin
http://www.onera.fr/staff/marc-boyer/          31055 TOULOUSE Cedex 4