Implement and represent polyadic operations

Question

I'm not sure I even know how to ask this question .. In implementing a compiler I would like to allow the client to specify, say, folds on tuples. I have provided a way to curry and uncurry a function, but only because I wrote a binary operator in Ocaml and folded it over the term and type representations. The user could not write this function.

In the macro processor, the user can write this function because tuples are lists.

For curried functions, the user can easily write transformers, because the term is binary in both the target language and the Ocaml representation of the term and the typing.

But they can't do this for tuples. Here's another example: the user easily defines serial functional composition operator. But the user cannot define parallel composition: the binary version:

 f1: D1 -> C1, f2: D2-> C2 --> f1 * f2: D1 * D2 -> C1 * C2

is easily written, but cannot be extended to 3 terms: here a fold would compute

 f1 * (f2 * f3)

instead of

f1 * f2 * f3

[isomorphic but not equal]

The generalisation of this question is "How do I implement a polyadic programming language" which is a bit too much to ask here. What I tried to do was provide a builtin transformer:

curry: T1 * T2 * T3 ... --> T1 -> T2 -> ... uncurry: T1 -> T2 -> .. T1 * T2 * T3

so then the user could just do folds with a binary operator:

uncurry (fold user_op (uncurry term))

but this is neither general enough nor works so well.. :)

I guess an equivalent question for Haskell would be: since Haskell has no n-ary products, the n-ary tuple constructors is simulated in the library with n functions, where each one has to be written out by hand. This clearly sucks. How would this be fixed?

[I mean, it is trivial to write a Python script to generate those n functions up to some limit n, so why is it so hard to do this in a well typed way inside the language?]

Answer 1

There are two components that collaborate to cause this issue:

• Tuples are not auto-flattened - the parentheses in type expressions do more than group, they create distinct types that are joined by further tuples. This leads to your observation that a * (b * c) is isomorphic but not equivalent to a * b * c.
• The type system does not provide a means to express algebra on tuple types. By this I mean that the type system does not have a cons operator or any equivalent for tuples; there is no way to express that a type has more or fewer tupled elements than another type.

The result is that there is no way to express the type of a function that operates on tuples of arbitrary length.

So, the short summary is that the OCaml type system lacks mechanisms to express the type of the function you are trying to write, and therefore you cannot write the function (setting aside nasty games with Obj; you could write the function, but you could not express its type to use it in a type-safe fashion).