Re: [Caml-list] dynamic runtime cast in Ocaml

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

From: Alain Frisch <frisch@clipper.ens.fr>
> > By the way, for the expressivity addict (Curry-style), there is now a
> > multimatch branch in CVS with support for a specific form of
> > dependent types. 
> 
> Nice !  Do you have specific cases of application in mind ?
> It's amazing to see how Caml succeed in escaping ML jail (rows, HO
> polymorphism, etc...).

I don't know. Actually I was quite dubious about the usefulness of
such a feature until a member of the Coq team told me that he
sometimes wished he could write programs that way. I suppose you need
some exposure to higher-order type systems before you can imagine
applications.
By the way, there was a nice example of encoding set types in variants
in TIP'02 in Dagstuhl, and this encoding would work (partially) with
this extension.

> Any long-term plan for inclusion in OCaml ?

None. This feature is fun, but it's still unclear whether it is really
useful. Not that i'm not convinced that dependent types are useful,
but dependent types are much more than this simple hack.

Another problem is that while type inference works nicely,
interface inclusion is hard to check (Francois Pottier told me it was
NP-complete). I'm still looking for a reasonable algorithm:
exponential in the number of constructors is a bit too much.

> I guess that backtracking unification could benefit to OCaml in other
> places (e.g.:undoing the effect of typing an ill-typed expression in the
> toplevel).

Always looking in the corners, you are.
This is unrelated to the rest of the patch, and I actually plan to move
backtracking to the main trunk in the future.

> Do you have any paper/doc describing multimatch typing ?

All the theory (and why it was so easy) is in my FOOL9 paper.
  http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/

For the implementation, it's just two new keywords, multifun and
multimatch, that trigger different typing rules.  Also there is clever
typing for as-patterns, which can help you get more readable types:

# let f x = multimatch x with `A -> 1
            | `B -> multimatch x with `A -> 'a' | `B -> true;;
val f : [< `A & 'a = int & 'b = char | `B & 'a = 'b & 'b = bool] -> 'a
# let f' = multifun `A|`B as x -> f x;;
val f' : [< `A & 'a = int | `B & 'a = bool] -> 'a

---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>
-------------------
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