[Haskell-cafe] Re: Memoization

[Peter Berry]

Sorry for digging up such an old thread, but my undergraduate
dissertation is on this topic so I couldn't resist. :)

(Some credit in the following goes to my supervisor, Ulrich Berger.)

> Mark Engelberg wrote:
> > I'd like to write a memoization utility.  Ideally, it would look
> > something like this:
> >
> > memoize :: (a->b) -> (a->b)

The type you actually want is more like:

memoFix :: ((a -> b) -> a -> b) -> a -> b

which is like the normal fixpoint function (defined only over
functions) except that it adds the memoization magic. The reason being
that you can then memoize recursive calls as well (without having to
figure out how to dive into the function definition and replace
recursive calls with calls to the memoized version).

On 27/05/07, apfelmus <apfelmus at quantentunnel.de> wrote:
> Note that due to parametricity, any function of this type is necessarily
> either id or _|_. In other words, there are only two functions of type
>
>   ∀a∀b. (a->b) -> (a->b)

Of course, this only talks about the value of id, not its behaviour.
fix :: ((a -> b) -> a -> b) -> a -> b = memoFix in the sense that the
values they compute are the same, but practically speaking they are
different since the latter does memoization.

> That's because the functions has to work for all types a and b in the
> same way, i.e. it may not even inspect how the given types a or b look
> like. You need type classes to get a reasonable type for the function
> you want
>
>   memoize :: Memoizable a => (a->b) -> (a->b)
>
>
> Now, how to implement something like this? Of course, one needs a finite
> map that stores values b for keys of type a. It turns out that such a
> map can be constructed recursively based on the structure of a:
>
>   Map ()            b  := b
>   Map (Either a a') b  := (Map a b, Map a' b)
>   Map (a,a')        b  := Map a (Map a' b)
>
> Here,  Map a b  is the type of a finite map from keys a to values b. Its
> construction is based on the following laws for functions
>
>         () -> b  =~=  b
>   (a + a') -> b  =~=  (a -> b) x (a' -> b) -- = case analysis
>   (a x a') -> b  =~=  a -> (a' -> b)       -- = currying

class Memoizable a f | a -> f where
    memIso :: (a -> b) :~= f b

where a :~= b represents an isomorphism between two types, and f is
the generalized trie functor indexed on the type a and storing values
of its parameter type (here b). Note that this only works if a is
algebraic (i.e. can be represented as a generalized trie using the
isomorphisms above and a couple more to deal with recursive and higher
kinded types[1]). And it almost goes without saying that you can only
memoize pure functions.

Then memoFix actually has a constrained type, namely:

memoFix :: Memoizable a f => ((a -> b) -> a -> b) -> a -> b

You can then take a recursive function like:

f :: A -> B
f x = ... f y ...

and transform it so it takes its own fixpoint as an argument:

f' :: (A -> B) -> A -> B
f' f x = ... f y ...

and then, if you have an instance

instance Memoizable A F where
    memIso = ...

after defining F, you can create the memo function with

fM : A -> B
fM = memoFix f'

You could generate F and the Memoizable instance using TH or DrIFT or
the like (allowing derivation would be really nice :). Actually F
could be considered a dependent type, so you could define a pretty
much universal instance using TH with that mechanism.

> For further and detailed explanations, see

[1]
>   R. Hinze. Memo functions, polytypically!
>   http://www.informatik.uni-bonn.de/~ralf/publications.html#P11
>
> and
>
>   R. Hinze. Generalizing generalized tries.
>   http://www.informatik.uni-bonn.de/~ralf/publications.html#J4

also:
T. Altenkirch. Representations of first order function types as
terminal coalgebras.
http://www.cs.nott.ac.uk/~txa/publ/tlca01a.pdf

which unfortunately you probably won't understand unless you know
about category/domain theory (I haven't figured it all out myself).

-- 
Peter Berry <pwberry at gmail.com>
Please avoid sending me Word or PowerPoint attachments.
See http://www.gnu.org/philosophy/no-word-attachments.html