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 80F7DBC8C for ; Tue, 25 Jan 2005 18:24:37 +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 j0PHOaVH004715 for ; Tue, 25 Jan 2005 18:24:37 +0100 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id SAA28527 for ; Tue, 25 Jan 2005 18:24:36 +0100 (MET) Received: from smtp1.adl2.internode.on.net (smtp1.adl2.internode.on.net [203.16.214.181]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j0PHOYvD004706 for ; Tue, 25 Jan 2005 18:24:35 +0100 Received: from [192.168.1.200] (ppp205-248.lns1.syd3.internode.on.net [203.122.205.248]) by smtp1.adl2.internode.on.net (8.12.9/8.12.9) with ESMTP id j0PHOP88093342; Wed, 26 Jan 2005 03:54:27 +1030 (CST) Subject: Re: [Caml-list] Type indexed types? From: skaller Reply-To: skaller@users.sourceforge.net To: Jim Farrand Cc: caml-list In-Reply-To: <1106672472.28636.20.camel@pelican.wigram> References: <20050125122849.GB15086@draco.xyxyx.org> <1106672472.28636.20.camel@pelican.wigram> Content-Type: text/plain Message-Id: <1106673863.28636.42.camel@pelican.wigram> Mime-Version: 1.0 X-Mailer: Ximian Evolution 1.2.2 (1.2.2-4) Date: 26 Jan 2005 04:24:25 +1100 Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 41F680D5.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 41F680D2.002 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 sourceforge:01 wrote:01 wrote:01 unification:01 unification:01 rhs:01 glebe:01 061:98 arbitrary:01 nsw:01 partial:01 algorithm:01 algorithm:01 argument:01 X-Spam-Checker-Version: SpamAssassin 3.0.0 (2004-09-13) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.0 X-Spam-Level: On Wed, 2005-01-26 at 04:01, skaller wrote: > On Tue, 2005-01-25 at 23:28, Jim Farrand wrote: > > Note that I already have a function which can compute if type a is a > > specialisation of type b. The algorithm I have requires a comparison with 4 possible results: less, greater, equal or incomparable. You can derive that from just less-equal: match a <= b, b <= a with | true, true -> Equal | true, false -> Less | false, true -> Greater | false, false -> Incomparable Unfortunately this requires two unification steps. To use you own comment "There must be a better way" but I don't know what it is. BTW: I obtain this result by adding a constraint to the unification algorithm that it only permits equations of the form: 'a = t in the MGU, where 'a is a variable taken from the LHS of the input equation (there is only a single equation when you're measuring 'less') This is essential matching an function argument against a function signature (we want to reduce the signature to make it equal to the argument). However, when we're trying to order all the match candidates, it would be nicer to get one of the above four results in one unification step. However it just won't work for an arbitrary MGU, which might have the LHS variables coming from either side of the equation. This can happen if you get matching type variables. Unfortunately, you can't just pick the LHS one every time, since after substitution, an RHS variable can end uo on the LHS .. :( So I'd like to know if there is a better way to calculate the four value partial ordering relation between two types than two comparisons for less.. any hints? -- John Skaller, mailto:skaller@users.sf.net voice: 061-2-9660-0850, snail: PO BOX 401 Glebe NSW 2037 Australia Checkout the Felix programming language http://felix.sf.net