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 <[EMAIL PROTECTED]> 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 <[EMAIL PROTECTED]> Please avoid sending me Word or PowerPoint attachments. See http://www.gnu.org/philosophy/no-word-attachments.html
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe