Re: [Caml-list] What about polymorphic union types in functors?

[Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>]

From: Alex Baretta <alex@baretta.com>

> I need the ocaml compiler to typecheck the use of variant tags to ensure 
> that no tag is used in a context where it is not meaningful. The absence 
> of such static typechecking would force me to throw an exception at 
> runtime if a tag is used where it is not meaningful. Such typechecking 
> is possible, and I actually rely heavily on it. What I need is a _union_ 
> morphism between a pair of similar modules and a third module similar to 
> the first two. From an algebraic stadpoint, this operator is well 
> defined. However, ocaml is unable to compile such code because pattern 
> matching on polymorphic variants requires all variants to be known 
> statically. However, I suspect that this limitation is due to the 
> implementation rather than the underlying model. If the compiler knew 
> that F1.t and F2.t were polymorphic variant types, then it could 
> dispatch be executing sequentially the pattern matching code for F1.t 
> defined by the F1 module and the pattern matching code for F2.t defined 
> in the F2 module. This can be done because at the time when F1 and F2 
> are compiled all polymorphic variants are actually known. There might be 
> some corner cases to be worked out, but the general principle ought to work.

You are mostly right for the execution part, but this would also
require extending the type system: currently, when you write
  type t = [t1 | t2]
the type checker just extracts the tag definitions from t1 and t2 and
builds a new variant type. The fact the tags came from t1 and t2 is
completely forgotten.
This means that there is now way to represent [t1 | t2] without
knowing the tags of t1 and t2.

Supposing this refinement is possible, the next problem is that it
would require some form of runtime information passing.
When you put a type definition in a caml functor, no information at
all is passed at runtime. So if a variant type is abstract, there is
no way we can pattern-match on it.
We would need something like stream parsers, but typing specially:
again more typing problems.
By the way, the code for pattern matching t1 is not defined when you
define t1, but only when you pattern-match on it. This way we can
generate optimal code, considering all the cases in the
pattern-matching.

Even if we were to do all that, the performance of the resulting code
would not be as good as the one obtained through code generation.

Is this a serious limiting factor for your programming?
In particular, does it impact expressiveness, or just conciseness?

Cheers,

Jacques Garrigue

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners