Maude-help mailing list

[Michael Katelman <katelman AT uiuc.edu>]

On Sat, Jan 2, 2010 at 2:13 PM, pbrowne 
<Patrick.Browne AT comp.dit.ie>
 wrote:
> 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?

I can't speak to your question in particular detail, and such
comparisons always seem difficult anyway, but one major difference
that cannot be ignored is polymorphism. I'm not advocating for one
language over another, and I certainly can't speak to IBLs in general,
but Maude simply does not support polymorphism as usually connoted. In
Haskell, when you write

id x = x

the proper type of this function is "forall a :: a -> a". The
quantification is what makes it polymorphic. You cannot do this
directly in Maude, for which the equivalent would be a function whose
type applies to any "kind", using Maude terminology (note that's
completely different from Haskell's use of "kind"). Another difference
is higher-orderedness in the type-system.

-Mike

>
> 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
>
>