Maude-help mailing list

[Matthias Radestock <matthias AT sorted.org>]

I have been experimenting with dependent types in Maude. In one of my
examples I want to define a 'zip' operation that is only defined for
lists of equal length. I start off with

    op _zip_ : List{X} List{Y} ~> List{Tuple{X,Y}} .

    eq LX zip LY = LX zipHelper LY if size(LX) = size(LY) .

'zip' is declared as a partial operation and I can indeed restrict it to
work only on lists of equal length.

I can push the check to the sort level by defining a sort for pairs of
lists with equal length and changing the equation for zip:

    sort BalancedListPair{X,Y} .
    subsort BalancedListPair{X,Y} < Tuple{List{X},List{Y}} .

    cmb < LX # LY > : BalancedListPair{X,Y} if size(LX) = size(LY) .

    var BXY : BalancedListPair{X,Y} .
    eq LX zip LY = zipHelper BXY if BXY := < LX # LY > .

The problem with the above approaches is that the signature of zip
remains unchanged - it gives no clue to the fact that zip only operates
on lists of equal length. I could change the zip declaration to

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

but that changes the arity of zip and forces callers to bundle the
arguments with the Tuple constructor.


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.


Am I missing a trick somewhere? Is there a way to do what I want in
current Maude?


Regards,

Matthias