Re: [Caml-list] Comparing two things of any two types, in pure

[oleg@pobox.com]

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).