From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 6E272BC88 for ; Mon, 7 Feb 2005 05:33:18 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j174XHvE013816 for ; Mon, 7 Feb 2005 05:33:17 +0100 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 FAA20585 for ; Mon, 7 Feb 2005 05:33:17 +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.13.0/8.13.0) with ESMTP id j174XFq2003966 for ; Mon, 7 Feb 2005 05:33:16 +0100 Received: from localhost (suiren [130.54.16.25]) by kurims.kurims.kyoto-u.ac.jp (8.13.1/8.13.1) with ESMTP id j174XDbV016675; Mon, 7 Feb 2005 13:33:13 +0900 (JST) Date: Mon, 07 Feb 2005 13:32:48 +0900 (JST) Message-Id: <20050207.133248.51779961.garrigue@math.nagoya-u.ac.jp> To: keiko@kaba.or.jp Cc: caml-list@inria.fr Subject: Re: [Caml-list] polymorphic recursion with type constraint? From: Jacques Garrigue In-Reply-To: <20050207.121707.74656685.keiko@kaba.or.jp> References: <20050207.121707.74656685.keiko@kaba.or.jp> X-Mailer: Mew version 4.1.53 on Emacs 21.3 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 4206EF8D.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 4206EF8B.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 recursion:01 kaba:01 rec:01 subst:01 subst:01 well-typed:01 recursion:01 rec:01 typable:01 compiler:01 polymorphic:01 polymorphic:01 typing:01 typing:01 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: From: nakata keiko > > Can I make the following function 'subst' well-behave, > so that it can be used in the contexts where: > 1) 'p' (the first argument) is assumed of type 'path', and > 'env' (the first argument)is assumed of type '(string * tau) list; > and > 2)'p' is assumed of type 'tau', and > 'env' is assumed of type '(string * tau) list; > > > type tau = [`Root | `Apply of path * tau |`Var of string] > and path = [`Root | `Apply of path * tau] > > let rec subst p env = > match p with > `Root -> `Root > | `Apply (p1, p2) -> `Apply(subst p1 env , subst p2 env) > | `Var s -> List.assoc s env > > Yet 'subst' is well-typed, > > let sub (p : path) (env : (string * tau)) = subst p env > > fails. To make the problem setting more explicit, you want to use the above function as both tau -> (string * tau) list -> tau and path -> (string * tau) list -> path Independently of recursion problems, this is impossible because usual variant typing assumes that all branches in a pattern matching will be used, so that the typing will at least be path -> (string * tau) list -> tau due to the `Var case. Maximal sharing of code is obtained by the following program: let rec subst_path env = function `Root -> `Root | `Apply (p1, p2) -> `Apply (subst_path env p1, subst_tau env p2) and subst_tau env = function #path as p -> (subst_path env p :> tau) | `Var s -> List.assoc s env Your first program would be typable assuming both "conditional typing of branches" and polymorphic recursion. The second is available inderectly, but the first was only implemented in an experimental version of the compiler. Jacques Garrigue