* Re: [Caml-list] Memoize GADT
2013-02-06 8:19 [Caml-list] Memoize GADT Christophe Papazian
@ 2013-02-06 9:50 ` Alain Frisch
2013-02-06 9:55 ` Gabriel Scherer
1 sibling, 0 replies; 3+ messages in thread
From: Alain Frisch @ 2013-02-06 9:50 UTC (permalink / raw)
To: Christophe Papazian; +Cc: Caml List, Sebastien Briais
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
>
>
^ permalink raw reply [flat|nested] 3+ messages in thread* Re: [Caml-list] Memoize GADT
2013-02-06 8:19 [Caml-list] Memoize GADT Christophe Papazian
2013-02-06 9:50 ` Alain Frisch
@ 2013-02-06 9:55 ` Gabriel Scherer
1 sibling, 0 replies; 3+ messages in thread
From: Gabriel Scherer @ 2013-02-06 9:55 UTC (permalink / raw)
To: Christophe Papazian; +Cc: Caml List
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
^ permalink raw reply [flat|nested] 3+ messages in thread