From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <oleg@okmij.org>
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 nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78])
	by yquem.inria.fr (Postfix) with ESMTP id E711FBB83
	for <caml-list@yquem.inria.fr>; Sat,  9 Sep 2006 08:37:08 +0200 (CEST)
Received: from selenite.metnet.navy.mil (selenite.metnet.navy.mil [192.16.167.32])
	by nez-perce.inria.fr (8.13.6/8.13.6) with ESMTP id k896b6V6026690
	(version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL)
	for <caml-list@inria.fr>; Sat, 9 Sep 2006 08:37:08 +0200
Received: (qmail 3897 invoked by uid 107); 9 Sep 2006 06:36:53 -0000
Received: from unknown (HELO Adric.metnet.fnmoc.navy.mil) (10.100.105.102)
  by selenite.metnet.navy.mil with SMTP; 9 Sep 2006 06:36:53 -0000
Received: by Adric.metnet.fnmoc.navy.mil (Postfix, from userid 760)
	id 04B8AAC00; Fri,  8 Sep 2006 20:11:39 -0700 (PDT)
To: caml-list@inria.fr
Cc: Diego.FERNANDEZ_PONS@etu.upmc.fr
Subject: Comparing two things of any two types, in pure OCaml
Reply-To: oleg@pobox.com
Errors-To: oleg@okmij.org
From: oleg@pobox.com
Message-Id: <20060909031139.04B8AAC00@Adric.metnet.fnmoc.navy.mil>
Date: Fri,  8 Sep 2006 20:11:39 -0700 (PDT)
X-Miltered: at nez-perce with ID 45026112.001 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 variants:01 booleans:01 int-:01 int-:01 val:01 associative:01 val:01 


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.

It seems however that open polymorphic variants are ideal for the
task. We start with

let myeq (x : [>]) (y : [>]) = false;;

and add one clause, comparing two booleans

let myeq x y = match (x,y) with
	(`T'bool x, `T'bool y) -> x = y
	| _ -> myeq x y;;

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's generate some test data

let v1 = true
let v2 x = not x
let v3 f = f 2
let v4 x = x = 1;;

and we are ready for the first test:

let t1 = [
	myeq (`T'bool v1) (`T'bool v1);
	myeq (`T'int2bool v4) (`T'int2bool v4);
	myeq (`T'bool v1) (`T'int2bool v4)
	];;

 which gives
	val t1 : bool list = [true; true; false]

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;;


We can now write the table associating with each function a
documentation string. We use an associative list of sorts:
	
let docs = [(myeq (`T'bool v1), "bool value");
	    (myeq (`T'int2bool v4), "v4");
	    (myeq (`T'int2bool'2bool v3), "v3");
	];;

let lookup x docs =
	  let rec loop = function [] -> None 
		| ((c,d)::t) -> if c x then Some d else loop t
	in loop docs
;;

Another test:

let t2 = 
	[lookup (`T'int2bool'2bool v3) docs;
	 lookup (`T'bool v1) docs;
	 lookup (`T'int2bool v4) docs
	];;

which evaluates to
 val t2 : string option list = [Some "v3"; Some "bool value"; Some "v4"]

We realize that we forgot about the function v2, which is of the type
bool->bool. So, we extend myeq once again

let myeq x y = match (x,y) with
	(`T'bool2bool (x : bool->bool), 
	 `T'bool2bool y) -> x == y
	| _ -> myeq x y;;

and extend our documentation

let docs = (myeq (`T'bool2bool v2), "negation")
	   :: docs;;
	
let t3 = 
	[lookup (`T'int2bool'2bool v3) docs;
	 lookup (`T'bool2bool v2) docs;
	 lookup (`T'bool v1) docs;
	 lookup (`T'int2bool v4) docs
	];;

which evaluates to
  val t3 : string option list =
  [Some "v3"; Some "negation"; Some "bool value"; Some "v4"]