The post Elegant memoization with functional memo tries showed a simple type of search tries and their use for functional memoization of functions. This post provides some composition tools for memo tries, whose definitions are inevitable, in that they are determined by the principle presented in Simplifying semantics with type class morphisms.
Compositional semantics and type class morphisms
The discipline of denotational semantics defines meaning functions compositionally, i.e., the meaning of a construct must be some function of the meanings of its components.
Type class morphisms make the denotational discipline even more specific:
The meaning of each method corresponds to the same method for the meaning.
meaning (a `mappend` b) == meaning a `mappend` meaning b
Memo tries, semantics, and morphisms
The semantic function for a memo trie is
untrie, which converts a trie (back) to a function:
untrie :: (a :->: b) -> (a -> b)
Let’s look at the consequences of requiring that
untrie be a morphism over
untrie mempty == mempty untrie (s `mappend` t) == untrie s `mappend` untrie t untrie (fmap f t) == fmap f (untrie t) untrie (pure a) == pure a untrie (tf <*> tx) == untrie tf <*> untrie tx untrie (return a) == return a untrie (u >>= k) == untrie u >>= untrie . k untrie id == id untrie (s . t) == untrie s . untrie t untrie (arr f) == arr f untrie (first t) == first (untrie t)
These morphism properties imply that all of the expected laws hold, assuming that we interpret equality semantically (or observationally). For instance,
untrie (mempty `mappend` a) == untrie mempty `mappend` untrie a == mempty `mappend` untrie a == untrie a untrie (fmap f (fmap g a)) == fmap f (untrie (fmap g a)) == fmap f (fmap g (untrie a)) == fmap (f.g) (untrie a) == untrie (fmap (f.g) a)
The implementation instances follow from applying
trie to both sides of each of these morphism laws, using the property
trie . untrie == id.
instance (HasTrie a, Monoid b) => Monoid (a :->: b) where mempty = trie mempty s `mappend` t = trie (untrie s `mappend` untrie t) instance HasTrie a => Functor ((:->:) a) where fmap f t = trie (fmap f (untrie t)) instance HasTrie a => Applicative ((:->:) a) where pure b = trie (pure b) tf <*> tx = trie (untrie tf <*> untrie tx) instance HasTrie a => Monad ((:->:) a) where return a = trie (return a) u >>= k = trie (untrie u >>= untrie . k) instance Category (:->:) where id = trie id s . t = trie (untrie s . untrie t) instance Arrow (:->:) where arr f = trie (arr f) first t = trie (first (untrie t))
Correctness of these instances follows by applying
untrie to each side of each definition and using the property
untrie . trie == id.
Arrow instances don’t quite work, however, because of necessary but disallowed
HasTrie constraints on the domain type.
John Hughes pointed out a similar problem near the end of Generalising Monads to Arrows, saying “I consider this to be a defect of the Haskell type system, which hopefully can be corrected in a future version of the language.”