A (Silly?) Question About Universal Type Quantification

A (Silly?) Question About Universal Type Quantification

[Will M Farr]

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

Hello,

I recently encountered a situation where I had (effectively) the  
following polymorphic type:

type 'a record = { id : int; data : 'a }

and the following compare function

let compare {id = id1} {id = id2} = Pervasives.compare id1 id2

and wanted to put such records into a set.  However, I could not  
figure out how to make the polymorphic 'a in the type definition  
"disappear" in the module argument to the Set.Make functor.  For  
example, the obvious

Set.Make(struct
   type t = 'a record
   let compare = compare
end)

fails because the 'a in the type definition for t is unbound.  Is  
there no way to do this?  I'm thinking of some sort of "forall"  
designation, which universally quantifies the type parameter, like

Set.Make(struct
   type t = forall 'a : 'a record
   let compare = compare
end)

(I'm sure that there is better terminology for this---please pardon my  
ignorance about types and type theory.)

I ended up solving my problem by placing the record type into a  
functor, whose argument specified the concrete type for data, but I'm  
curious if other solutions exist.

Thanks,
Will

[-- Attachment #2: This is a digitally signed message part --]
[-- Type: application/pgp-signature, Size: 203 bytes --]

Re: [Caml-list] A (Silly?) Question About Universal Type Quantification

[Martin Jambon]

Will M Farr wrote:
> Hello,
> 
> I recently encountered a situation where I had (effectively) the
> following polymorphic type:
> 
> type 'a record = { id : int; data : 'a }

You could do this:

type record = { id : int; data : 'a . 'a }

The only minor problem is that you can't create values of such type :-)


> and the following compare function
> 
> let compare {id = id1} {id = id2} = Pervasives.compare id1 id2
> 
> and wanted to put such records into a set.  However, I could not figure
> out how to make the polymorphic 'a in the type definition "disappear" in
> the module argument to the Set.Make functor.  For example, the obvious
> 
> Set.Make(struct
>   type t = 'a record
>   let compare = compare
> end)
> 
> fails because the 'a in the type definition for t is unbound.  Is there
> no way to do this?  I'm thinking of some sort of "forall" designation,
> which universally quantifies the type parameter, like
> 
> Set.Make(struct
>   type t = forall 'a : 'a record
>   let compare = compare
> end)
> 
> (I'm sure that there is better terminology for this---please pardon my
> ignorance about types and type theory.)
> 
> I ended up solving my problem by placing the record type into a functor,
> whose argument specified the concrete type for data, but I'm curious if
> other solutions exist.

Looks like the right approach.

You could also used a defunctorized version of Set, at the cost of losing the
static guarantee that you won't mix sets using inconsistent comparison functions.


Martin

-- 
http://mjambon.com/

Re: [Caml-list] A (Silly?) Question About Universal Type Quantification

[Alan Schmitt]

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

On Thu, Sep 10, 2009 at 5:00 PM, Will M Farr <farr@mit.edu> wrote:

> Hello,
>
> I recently encountered a situation where I had (effectively) the following
> polymorphic type:
>
> type 'a record = { id : int; data : 'a }
>
> and the following compare function
>
> let compare {id = id1} {id = id2} = Pervasives.compare id1 id2
>
> and wanted to put such records into a set.  However, I could not figure out
> how to make the polymorphic 'a in the type definition "disappear" in the
> module argument to the Set.Make functor.


Interestingly, I had the same problem recently where I wanted to create a
list of "tests" that could access some extra information  when run (and
would also return a list of tests to run later). I found that using a class
type worked well:

class type test =
  object
    method name : string
    method run : (test * float) list
  end

To define a test, I simply do:

let test_download : Timed_events.test =
  object (self)
    val mutable cache = 0 (* anything I want *)
    method name = "Download"
    method run =
      (* From here I can access the cache and plan to run the test again in
10 seconds *)
      [self, 10.0]
    end

Alan

[-- Attachment #2: Type: text/html, Size: 1731 bytes --]