Maude-help mailing list

[pbrowne <Patrick.Browne AT comp.dit.ie>]

Paco/Michael
Thanks very much for your detailed responses. You have confirmed some of
my rather vague intuitions about Maude and Haskell.

As part of my research I am comparing Haskell type classes/instances
with the structuring features institution based languages (IBLs) such as
Maude, CafeoBJ, OBJ3 and CASL. At this stage, it seems the IBLs have a
lot to offer over Haskell type classes/instances (name-space control,
parameterised modules, views, multiple logics, non-constructive axioms
for specification, constructive axioms for data structures and
algorithms ..).

It seems that the only thing the IBLs don't have is the kind of type
level inference provided by Haskell's classes. Am I correct in assuming
the Maude *unify* command provides a Haskell-like type level reasoning?

Regards,
Pat


Michael Katelman wrote:
> On Sat, Jan 2, 2010 at 10:51 AM, Michael Katelman 
> <katelman AT uiuc.edu>
>  wrote:
>> On Fri, Jan 1, 2010 at 6:16 PM, Francisco Durán 
>> <duran AT lcc.uma.es>
>>  wrote:
>>> Hi Pat,
>>>
>>> I agree with you. I think Maude does not suffer from the expression 
>>> problem.
>>> Order-sortedness gives a very expressive power, and makes "classifying" 
>>> very
>>> precise.
>>>
>>> I don't think however that I would buy your solution. If I wanted to 
>>> define
>>> a new constructor for a sort S, I would import S in protecting mode, and
>>> define a supersort of it S'. Notice that in this way all functions on S
>>> still work, and I only need to worry about those I want to add. If I 
>>> wanted
>>> to "extend" some of the previously defined functions to my new sort S', 
>>> I'd
>>> just need to add the subsort overloaded declaration and cover the new 
>>> cases.
>>> Notice that in this way you get the advantages of "closed types" for
>>> defining total functions at the time you have facilities for extending
>>> available types.
>> Perhaps it's also worth mentioning, since the example cited was
>> OO-style inheritance, that if you extend a data type as above and add
>> new equations for constructors in the original definition, they will
> 
> I mean new equations for an equationally defined function where the
> argument is one of the original constructors, not equations directly
> on the constructors.
> 
>> not override the original ones like those of a child class in Java.
>> Essentially, Maude could choose to apply either one at its discretion.
>> The usual requirement to ensure that this operates correctly is
>> confluence.
>>
>> -Mike
>>
>>> Happy new year,
>>>
>>> Paco
>>>
>>> El 31/12/2009, a las 22:49, pbrowne escribió:
>>>
>>>> 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
>>>>
>>>>
>>>> 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.
>>>>
>>>> I *think* that a new constructor could be added to an existing sort by
>>>> importing in a using rather than protecting mode.
>>>> So I (perhaps incorrectly) conclude that Maude does not suffer from the
>>>> expression problem.
>>>>
>>>>
>>>> !!!!Happy new year to all on the Maude list!!!!
>>>> Pat
>>>>
>>>>
>>>>
>>>> Michael Katelman wrote:
>>>>> Pat,
>>>>>
>>>>> Could you clarify exactly what the "expression problem" is? I am
>>>>> having difficulty following the wikipedia entry.
>>>>>
>>>>> Since you mentioned type classes (a la Haskell), perhaps it's relevant
>>>>> to note that while ad-hoc overloading of functions is allowed in
>>>>> Maude, the situation is somewhat different from Haskell's type
>>>>> classes.  Haskell's type classes are used to support a sort of
>>>>> restricted polymorphism where the type signature quantifies over a
>>>>> subset of all types with the same overloaded operators, but the
>>>>> "type-system" of Maude is not polymorphic; in the sense that the
>>>>> signatures of functions cannot have universal quantifiers over
>>>>> "types", like in Haskell.
>>>>>
>>>>> At least that's my take on how the two are related.
>>>>>
>>>>> -Mike
>>>>>
>>>>> On Thu, Dec 31, 2009 at 5:44 AM, pbrowne 
>>>>> <Patrick.Browne AT comp.dit.ie>
>>>>> wrote:
>>>>>> hi,
>>>>>> I have a question concerning Wadler's expression problem[1] for
>>>>>> algebraic data types. In relation to Haskells type classes is easy to
>>>>>> add a new operations on existing data types, it requires only the
>>>>>> definition of a new function. All the old functions on those types
>>>>>> continue to work unchanged. On the other hand, it is difficult to add
>>>>>> new structure to an existing data type: it requires the addition of a
>>>>>> new constructor for the existing data type.
>>>>>>
>>>>>> Questions:
>>>>>> 1)Does expression problem exist in Maude?
>>>>>> 2)If it does not exist in Maude, is there an illustrative example
>>>>>> available?
>>>>>>
>>>>>>
>>>>>> Pat
>>>>>>
>>>>>> [1]http://en.wikipedia.org/wiki/Expression_Problem
>>>>>>
>>>>>> _______________________________________________
>>>>>> Maude-help mailing list
>>>>>> Maude-help AT cs.uiuc.edu
>>>>>> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help
>>>>>>
>>>>> _______________________________________________
>>>>> Maude-help mailing list
>>>>> Maude-help AT cs.uiuc.edu
>>>>> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help
>>>>
>>>> _______________________________________________
>>>> Maude-help mailing list
>>>> Maude-help AT cs.uiuc.edu
>>>> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help
>>>
> 
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help