[Caml-list] Memoize GADT

[Caml-list] Memoize GADT

[Christophe Papazian]

Hi,

this must be a very basic question for some of you, sorry for the inconvenience :

When I have function "f" of type (a -> b), I can easily add a layer to that function to memoize the result by using a (a,b) Hashtbl.t to store the results of the expensive to compute "f".

let mf = let e = Hashtbl.create 0 in ( fun x -> try Hashtbl.find e x with Not_found -> let res = f x in Hashtbl.add e x res; res )

But now, I have a function "g" 
	let g (type a) : a gadt -> a = ....

And If I apply the same method, type a becomes weak (_'a).

Is there something simple to memoize that function as easy as the previous example and keep its polymorphism ? I think not, but I hope to be wrong.

Thanks

	Christophe

Re: [Caml-list] Memoize GADT

[Alain Frisch]

We have encountered exactly the same problem recently.  A slightly more 
general version of your question is how to memoize a function of type

   'a t -> 'a s

for two type parametrized constructors t and s (and similarly with 
higher arities).  We want an hash table which can hold key/value 
bindings ('a t * 'a s) for any 'a.  The equality of keys must be such 
that when (key1 : 'a t) is equal to (key2 : 'b t), we can deduce that 'a 
and 'b are the same type (i.e. the value must hold enough information to 
deduce the type from the content), which guarantees that 'a s and 'b s 
are also the same type (and so the existing value associated to key1 can 
be returned for key2).  This assumption often holds when 'a t is a GADT 
representing "expressions which evaluate to values of type 'a".

Our solution (implemented by my colleague Sebastien, in Cc:) has been to 
create a functor with the following signature:

======================================================================
module type ParametricType = sig
   type 'a t
end

module ParametricEquality : sig
   type (_, _) t =
     | Eq: ('a, 'a) t
     | Ne: ('a, 'b) t
end

module type ParametricHashedType = sig
   type 'a t
   val equal: 'a t -> 'b t -> ('a, 'b) ParametricEquality.t
   val hash: 'a t -> int
end

module ParametricHashtbl : sig
   module type S = sig
     type 'a key
     type 'a value
     type binding = Binding: 'a key * 'a value -> binding
     type t
     val create: int -> t
     val clear: t -> unit
     val reset: t -> unit
     val copy: t -> t
     val add: t -> 'a key -> 'a value -> unit
     val remove: t -> 'a key -> unit
     val find: t -> 'a key -> 'a value
     val find_all: t -> 'a key -> 'a value list
     val replace: t -> 'a key -> 'a value -> unit
     val mem: t -> 'a key -> bool
     val length: t -> int
     val iter: (binding -> unit) -> t -> unit
     val fold: (binding -> 'a -> 'a) -> t -> 'a -> 'a
   end
   module Make(X:ParametricHashedType)(Y:ParametricType): S with type 'a 
key = 'a X.t and type 'a value = 'a Y.t
end
======================================================================

Note that the first input of the function (ParametricHashedTyped) looks 
like the standard argument to Hashtbl.Make, except that the equality 
function returns a dynamic witness of equality between 'a and 'b in case 
of equality between two values of types 'a t and 'b t.  This is 
implemented using a GADT.  We also use a GADT to introduce an 
existential on 'a for key/value pairs of type ('a t * 'a s) to be used 
for iterators (iter/fold).  Instead we could have defined those 
iterators as taking a polymorphic function as argument (through 
polymorphic methods or record fields, or with a first-class module), but 
they would have been more heavy to use on the call site (although this 
would avoid the allocation of the Binding constructor).

On the implementation side, there are three choices:

  - Create a type-safe implementation by instantiating Hashtbl, and 
store values which keep a copy of the key, with an existential both on 
keys and on values.  This requires extra comparisons and boxing. (Good 
exercise left to the reader!)

  - Copy and adapt the implementation of Hashtbl, which can avoid some 
of the extra comparisons. (Painful!)

  - The quicker way (and the one we have chosen for now) is to 
instantiate Hashtbl on type Obj.t for keys and values, and using unsafe 
operations (Obj.magic) to cast its result to the signature above.  I 
don't think it is good style to share here code using Obj.magic, so I 
will refrain from doing so :-)

We have done the same for Set, Map, association lists and Weak (for 
such, I believe, the unsafe implementation is the only choice, because 
if we wrap the values with freshly allocated existential constructors, 
they can immediately be garbage-collected).

It would probably make sense to provide such functors as part of the stdlib.



Alain







On 02/06/2013 09:19 AM, Christophe Papazian wrote:
> Hi,
>
> this must be a very basic question for some of you, sorry for the inconvenience :
>
> When I have function "f" of type (a -> b), I can easily add a layer to that function to memoize the result by using a (a,b) Hashtbl.t to store the results of the expensive to compute "f".
>
> let mf = let e = Hashtbl.create 0 in ( fun x -> try Hashtbl.find e x with Not_found -> let res = f x in Hashtbl.add e x res; res )
>
> But now, I have a function "g"
> 	let g (type a) : a gadt -> a = ....
>
> And If I apply the same method, type a becomes weak (_'a).
>
> Is there something simple to memoize that function as easy as the previous example and keep its polymorphism ? I think not, but I hope to be wrong.
>
> Thanks
>
> 	Christophe
>
>

Re: [Caml-list] Memoize GADT

[Gabriel Scherer]

On Wed, Feb 6, 2013 at 9:19 AM, Christophe Papazian
<christophe.papazian@gmail.com> wrote:
> this must be a very basic question for some of you, sorry for the inconvenience :

This is actually a rather advanced question (everything related to
GADTs is advanced for now, and when you add observationally pure
effects and value restriction into the mix, you're quite sure this is
not "very basic"), thank you for asking it. I think one important
difficulty is that you want to memoize a polymorphic function, with
possibly non-regular recursion: the "keys" of the memo table could
have different types, and arbitrarily many so -- this can happen with
polymorphic recursion, even without GADTs.

It would help to see a real code example of your GADT definition and
the function you're trying to memoize (for example, if it is
recursive, would it be ok to just memoize over the recursive calls of
a single top call, or do you also need to memoize over several
unrelated calls?).

I would try to do this using existential types: have an additional
GADT `a tyrepr` that represents (as runtime data) the types that can
be picked by the parameter `a`, then define an monomorphic existential
type `exists a . a tyrepr * a gadt` (... as a third GADT type), and do
your memoization on that. In the function you want to memoize you can
build the existential corresponding to the argument, look it up on the
table, and if you find something extract the attached value. You get a
result of the type (encoded as a GADT) `exists a . a tyrepr * a
result`, can check  that the two type representation are equal (`a
tyrepr -> b tyrepr -> (a, b) eq option`), and in this case extract
your result with static knowledge that it has the right type.

There have been some questions on that in the Haskell community as
well, see Conal Elliott's
  http://conal.net/blog/posts/memoizing-polymorphic-functions-part-one
and later posts (by him, Dan Piponi, and him again).

> When I have function "f" of type (a -> b), I can easily add a layer to that function to memoize the result by using a (a,b) Hashtbl.t to store the results of the expensive to compute "f".
>
> let mf = let e = Hashtbl.create 0 in ( fun x -> try Hashtbl.find e x with Not_found -> let res = f x in Hashtbl.add e x res; res )
>
> But now, I have a function "g"
>         let g (type a) : a gadt -> a = ....
>
> And If I apply the same method, type a becomes weak (_'a).
>
> Is there something simple to memoize that function as easy as the previous example and keep its polymorphism ? I think not, but I hope to be wrong.
>
> Thanks
>
>         Christophe
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs