From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id KAA24444; Tue, 12 Nov 2002 10:09:43 +0100 (MET) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id KAA24439 for ; Tue, 12 Nov 2002 10:09:43 +0100 (MET) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id gAC99fX15070 for ; Tue, 12 Nov 2002 10:09:41 +0100 (MET) Received: from localhost (suiren.kurims.kyoto-u.ac.jp [130.54.16.25]) by kurims.kurims.kyoto-u.ac.jp (8.9.3/3.7W) with ESMTP id SAA25644; Mon, 11 Nov 2002 18:26:15 +0900 (JST) To: frisch@clipper.ens.fr Cc: caml-list@inria.fr Subject: Re: [Caml-list] dynamic runtime cast in Ocaml In-Reply-To: References: <20021107162220A.garrigue@kurims.kyoto-u.ac.jp> X-Mailer: Mew version 1.94.2 on Emacs 21.2 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-Id: <20021111182614T.garrigue@kurims.kyoto-u.ac.jp> Date: Mon, 11 Nov 2002 18:26:14 +0900 From: Jacques Garrigue X-Dispatcher: imput version 20000228(IM140) Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk From: Alain Frisch > > 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 JG ------------------- 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