Maude-help mailing list

[Matthias Radestock <matthias AT sorted.org>]

Francisco,

Francisco Duran 
<duran AT lcc.uma.es>
 writes:

> Matthias Radestock 
> <matthias AT sorted.org>
>  writes:
>
>> Here's what I would like to write:
>>     sort BalancedListPair{X,Y} .
>>     subsort BalancedListPair{X,Y} < (List{X},List{Y}) .
>>     cmb (LX,LY) : BalancedListPair{X,Y} if size(LX) = size(LY) .
>>     op _zip_ : BalancedListPair{X,Y} -> List{(X,Y)} .
>> In other words, I want product types and tupling such that any n-ary
>> operator is equivalent to a unary operator on n-tuples.
>
> Maude doesn't support such facilities, and actually we haven't
> consider so far including them.

I should have provided a bit more context. Apologies. The motivation for
the above is to provide better support for dependent typing. This places
two requirements on the solution:

1) The operator arity must remain unchanged - otherwise we have to
modify the callers

2) The dependency constraints must be captured in the operator signature
- otherwise it is not part of the type

The two solutions you suggested, namely

>     op zip : BalancedListPair{X, Y} -> List{Tuple{X, Y}} .

and

>     op _zip_ : List{X} List{Y} -> [List{Tuple{X, Y}}] .

fail the first and second requirement respectively.

The first one, which is also what I came up with, is actually not far
off the mark since it can be made to fit the requirements by following a
coding discipline of declaring all operators as unary and using explicit
tupling to encode n-ary operators. That is really inconvenient
though. It rules out infix operators and also results in a lot of tuple
con/de-structing clutter.

I hope this helps to explain the direction I was heading in. Of course
it may well turn out that what I was proposing runs contrary to some
basic principles of Maude's design and use. If not then perhaps it
merits consideration for some future version.


Matthias