killing a cat

killing a cat

[Warren Harris]

[-- 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 --]

Re: killing a cat

[Zheng Li]

Hi,

Warren Harris wrote:
> 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 think it's reasonable to use universal qualifier here.

> 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

It's hard to tell where a better option is without knowing your overall
design on types and data structures. On the other hand, I would usually
restrict universal qualifiers into a range as small as possible. In your
example, I would probably define as the follows:

<code>
type 'a handler = { handle: 'a -> (string * 'a) writer }
and  'a writer = { write: 'b. (unit -> 'a -> 'b) -> 'b }

let helper name wf = { handle = wf name }
let write_int_field s i = { write = fun k -> k () (s, i+1) }
let f = helper "f" write_int_field
</code>

which seems simpler to me. However this really depends on your overall
design.

HTH.

--
Zheng