Re: [Caml-list] Explicit Arity with Polymorphic Variants

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2015/01/26 04:57, Jordo wrote:
> 
> You've listed some good examples of why this would be difficult to implement and some examples of how this would be confusing to developers. But I am having a hard time seeing how you have demonstrated why polymorphic variants cannot assume two forms - each incompatible with the other, with any particular form being completely inferred. I am not claiming that a distinction between the two forms is not needed at the type level - the two forms would be incompatible with each other at the type level just as they are incompatible for standard variants. My question was why does a distinction at the type level require a type *definition* (which was your original claim). For the sake of experimentation, assume you can create any syntax you need that would unambiguously express which of the two forms is being reasoned about in all situations.


Indeed, there is no theoretical difficulty in introducing multi-argument polymorphic variants, and they were considered at some point.
However, for this to work this should imperatively be supported at the type level too: multi-argument polymorphic variant should have a type incompatible with single-argument ones.
So this means making the type algebra more complex, adding extra syntax both at the value/pattern and type level, and extending the unification and type inference algorithms, for something that doesn't seem that useful (if you need performance, you're better served by normal variants anyway).
Of course you're free to try to add them to the compiler :-)

	Jacques