Re: [Caml-list] Memoize GADT

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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