[Caml-list] killing a cat

[Warren Harris]

I've encountered a complicated issue that I'm wondering if anyone can shed some light on here. It relates to polymorphic types what I like to call Schrödinger types (sorry, I don't know the real name for these, but they're the dreaded polymorphic variables with underscores that, like Schrödinger's cat, are undefined until you use them for the first time). I'll try to distill it down to its simplest form here, but the issue arises from desiring to implement something based on "type-indexed values" such as described here: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.1977

type ('a, 'b) writer = ((unit -> 'a) -> 'b)




let f = { handle = fun a k -> write_int_field "f" a k }



let helper name wf = { handle = fun a k -> wf name a k }
let f = helper "f" write_int_field







However, this doesn't allow me to define the helper function as before:

  let helper name wf = { handle = fun a k -> wf name a k };;
                                  ^^^^^^^^^^^^^^^^^^^^^^
This field value has type 'a -> (string -> 'a -> 'b, 'b) writer
which is less general than 'c. 'd -> (string -> 'd -> 'c, 'c) writer





This works:

let helper name wf = { handle = fun a k -> wf.write_field name a k }
let f = helper "f" write_int_field



Warren Harris
Metaweb Technologies

In its simplest form, I have a writer type and a dispatching handler like this: type ('a, 'b) handler = { handle : 'a -> (string -> 'a -> 'b, 'b) writer } Then I wish to define a family of handlers that ultimately call the writer's continuation. In the very simplest form, a handler might be expressed as: which would have type "(int, 'a) handler" as desired. (In the real implementation, there will be more than one handler, hence the need for the record.) However, I wish to define a family of handlers that all share common implementation, so I define a helper function (again, vastly simplified): However, here the type of "f" is now "('int, '_a) handler" and fails to unify with the desired type expressed in the interface. Now, I could get around this by making "f" be a function that when evaluated returns the result of the helper. However, I'm trying to avoid that because in the real implementation, the work of the helper is somewhat expensive and should only be performed once. An alternate solution can be achieved by pushing the universal qualifier for the result type down into the handler: type 'a handler = { handle : 'b . 'a -> (string -> 'a -> 'b, 'b) writer } I am forced into reworking the helper parameter function, wf, to also become a record in order for it to be universally qualified: type 'a field_handler = { write_field : 'b . string -> 'a -> (unit -> string -> 'a -> 'b) -> 'b } Here "f" has type "int handler" as desired, although this solution seems somewhat round-about, and was difficult to arrive at. Can anyone suggest another approach that prevents the dreaded underscores? (Note that using objects instead of records exhibits the exact same behavior.)

smime.p7s
Description: S/MIME cryptographic signature

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs