From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.6 required=5.0 tests=AWL,NO_REAL_NAME,SPF_FAIL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 4D98CBB83 for ; Wed, 13 Sep 2006 11:18:07 +0200 (CEST) Received: from selenite.metnet.navy.mil (selenite.metnet.navy.mil [192.16.167.32]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id k8D9I0cT026666 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Wed, 13 Sep 2006 11:18:06 +0200 Received: (qmail 20869 invoked by uid 107); 13 Sep 2006 09:17:57 -0000 Received: from unknown (HELO Adric.metnet.fnmoc.navy.mil) (10.100.105.102) by selenite.metnet.navy.mil with SMTP; 13 Sep 2006 09:17:57 -0000 Received: by Adric.metnet.fnmoc.navy.mil (Postfix, from userid 760) id 537F4AC04; Wed, 13 Sep 2006 02:14:35 -0700 (PDT) To: garrigue@math.nagoya-u.ac.jp Cc: caml-list@inria.fr In-reply-to: <20060909.161349.09849160.garrigue@math.nagoya-u.ac.jp> Subject: Re: [Caml-list] Comparing two things of any two types, in pure Reply-To: oleg@pobox.com Errors-To: oleg@okmij.org From: oleg@pobox.com Message-Id: <20060913091435.537F4AC04@Adric.metnet.fnmoc.navy.mil> Date: Wed, 13 Sep 2006 02:14:35 -0700 (PDT) X-Miltered: at discorde with ID 4507CCC8.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; oleg:01 variants:01 int-:01 bool:01 bool:01 int-:01 variants:01 run-time:01 run-time:01 notation:01 compiler:01 metaocaml:01 polymorphic:01 polymorphic:01 typing:01 Hello! > > It seems however that open polymorphic variants are ideal for the > > task. We start with > > > > let myeq (x : [>]) (y : [>]) = false;; > [...] > > We can add another clause, for int->bool functions: > > let myeq x y = match (x,y) with > > (`T'int2bool (x : int->bool), `T'int2bool y) -> x == y > > | _ -> myeq x y;; > [...] > > Let us extend myeq once again: > > let myeq x y = match (x,y) with > > (`T'int2bool'2bool (x : (int->bool)->bool), > > `T'int2bool'2bool y) -> x == y > > | _ -> myeq x y;; > While such a solution is appealing, there are drawbacks. > 1) You have to add a new case for each new function type, rather than > each type constructor. > 2) In the open case, there is no static protection against mistyping a > variant constructor. But you can check it dynamically... > This will return true only if x's type is handled by myeq. > 2) Polymorphic variant typing does not always play well with > modularity. ... For this reason, exceptions may be better for > extension across modules. The drawback #1 is a feature! The intent was to play around the similarity between such polymorphic variants and dependent sums. The tag like `T'int2bool almost certainly has a run-time representation -- that's what makes (run-time) matching possible. Let's call the type of these run-time values typeRep. Therefore, the value `T'int2bool (x : int->bool) might be thought of as let tag = (repr `T'int2bool) : typerep in (tag, x : reflect(tag)) or, in a more familiar notation, Sigma (tag: typeRep) x : reflect(tag) where reflect is a function from terms to types. It should be a function: identical tags correspond to identical types. Then the myeq function might be thought of as let myeq x y = open x with (tag1,xv : reflect(tag1)) in open y with (tag2,yv : reflect(tag2)) in tag1 = tag2 && (==) [reflect(tag1)] xv yv where [t] is a type application. Then one may dream of the ways to generate these tags a bit more systematically (actually, there is: the compiler has the way to represent types, and in MetaOCaml, these types can be reified to run-time values).