From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <garrigue@math.nagoya-u.ac.jp>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: 
X-Spam-Status: No, score=0.4 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE 
	autolearn=disabled version=3.1.3
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39])
	by yquem.inria.fr (Postfix) with ESMTP id 2E7DDBB83
	for <caml-list@yquem.inria.fr>; Sat,  9 Sep 2006 09:14:26 +0200 (CEST)
Received: from rabbit.math.nagoya-u.ac.jp (rabbit.math.nagoya-u.ac.jp [133.6.130.5])
	by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id k897EOoD002854
	for <caml-list@inria.fr>; Sat, 9 Sep 2006 09:14:25 +0200
Received: from localhost (moose-172 [172.16.254.3])
	by rabbit.math.nagoya-u.ac.jp (8.12.11/3.7W) with ESMTP id k897DvpN011727;
	Sat, 9 Sep 2006 16:13:57 +0900 (JST)
Date: Sat, 09 Sep 2006 16:13:49 +0900 (JST)
Message-Id: <20060909.161349.09849160.garrigue@math.nagoya-u.ac.jp>
To: oleg@pobox.com
Cc: caml-list@inria.fr, Diego.FERNANDEZ_PONS@etu.upmc.fr
Subject: Re: [Caml-list] Comparing two things of any two types, in pure
 OCaml
From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
In-Reply-To: <20060909031139.04B8AAC00@Adric.metnet.fnmoc.navy.mil>
References: <20060909031139.04B8AAC00@Adric.metnet.fnmoc.navy.mil>
X-Mailer: Mew version 4.2 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 concorde with ID 450269D0.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)!
X-Spam: no; 0.00; ocaml:01 oleg:01 bool:01 pons:01 hashtable:01 hash:01 hashtable:01 bool:01 annotation:01 datatypes:01 annotations:01 variants:01 variants:01 modular:01 constructors:01 

Hi Oleg,

> This message shows an example of an open, extensible comparison function
> 'a -> 'b -> bool.
> 
> Diego Olivier Fernandez Pons wrote about a help system associating (by
> means of a hashtable) a documentation string to a function. Alas, the
> hash function is not perfect and collisions are possible. Therefore,
> we need to validate each hashtable hit by physically (==) comparing
> the function (whose documentation we need to lookup) against the
> target function. The functions to document have generally different
> types. This raises two questions: how to store functions of different
> types in the same data structure, and how to compare a candidate
> function against these functions of different types. The physical
> comparison function (==) cannot be used as it is: we need a comparison
> function [cmp : 'a -> 'b -> bool] that can take arguments of any two
> types, returning false if the argument types are different.
> 
> Jacques Garrigue suggested using Obj.repr. He also wrote ``Type
> theoretician answer: What you would need to do that transparently
> inside the type system is generic functions with dynamics.'' and
> mentioned GADT.

Small comment: By transparently I meant "without any type
annotation". Then I gave a solution using normal datatypes for
annotations, and polymorphic methods, and just mentioned that GADTs
were not useful in this case. Note that my solution cannot directly
use polymorphic variants, as it uses non-regular types, and
polymorphic variants have to be regular. But an interesting question
is whether that solution could be made more modular, to enable
extension with new type constructors.

> 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:
     let type_handled x = myeq x x
   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 instance, you cannot define an hashtable in a
   module, and add new cases no included in the original type in
   another module. For this reason, exceptions may be better for
   extension across modules.

This said, I love polymorphic variants anyway...

Jacques Garrigue