killing a cat

[Warren Harris <warren@metaweb.com>]

[-- Attachment #1: Type: text/plain, Size: 3094 bytes --]

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

In its simplest form, I have a writer type and a dispatching handler  
like this:

type ('a, 'b) writer = ((unit -> 'a) -> 'b)
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:

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

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

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

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 }

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

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 }

This works:

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

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

Warren Harris
Metaweb Technologies




[-- Attachment #2: smime.p7s --]
[-- Type: application/pkcs7-signature, Size: 3739 bytes --]