RE: [Caml-list] Recursive subtyping issue

["David Allsopp" <dra-news@metastack.com>]

Guillaume Yziquel wrote:
> Stéphane Glondu a écrit :
> > Guillaume Yziquel a écrit :
> >>> # type untyped;;
> >>> type untyped
> >>> # type 'a typed = private untyped;;
> >>> type 'a typed = private untyped
> >>> # type -'typing tau = private obj
> >>>   and 'a t = 'a typed tau
> >>>   and obj = private untyped tau;;
> >>> type 'a tau = private obj
> >>> and 'a t = 'a typed tau
> >>> and obj = private untyped tau
> >>> # let f : 'a t -> obj = fun x -> (x : 'a t :> obj);; val f : 'a t ->
> >>> obj = <fun> # let g : obj -> 'a t = fun x -> (x : obj :> 'a t);; val
> >>> g : obj -> 'a t = <fun> #
> >
> > Why don't you just declare 'a t to be synonym for obj in the
> > implementation of your module, declare them as abstract in its
> > interface, and export the specially typed identities f and g?
> 
> Because subtyping seems more efficient than applying a noop function.

I wholeheartedly agree that doing this in the type system is much cleaner than using noop/coercion functions but I don't think that there's any difference in terms of efficiency. If the noop/coercion functions are correctly coded then they will be of the form:

external foo_of_bar : bar -> foo = "%identity"

in *both* the .ml and .mli file for the module in question. I'm virtually certain that ocamlopt eliminates calls to the %identity primitive.

> And this code might run really often, so I do not like very much the
> idea of having noop functions running really often.

See previous; I don't think it makes a difference (to runtime performance, anyway).

> Moreover, having conversion functions is not really handy, from a
> syntactic point of view: It's quite convenient to write something like
> 
> let f : string -> obj :> string -> float t = blah blah blah...
> 
> than doing the explicit, runtime, casting in the definition of f.

Agreed - this is where your approach is really neat!

<snip>

> I then tried to go the whole way, and get rid of conversion functions
> altogether.

Being pedantic, what you mean is getting rid of *coercion* functions; *conversion* functions could never eliminated because by their nature they are "doing" something (for example, int_of_string constructs a new integer value based on the string value given to it - you could never just trick the type system into using the same value for both in a meaningful way).

This is tremendously clean - as long as the types are clearly documented! The problem is that ocamldoc doesn't let you "document" coercions (by which I mean that having a conversion function provides means for the documentation of that particular usage).


David