Conal Elliott

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.

For instance,

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 Monoid, Functor, Applicative, Monad, Category, and Arrow, i.e.,

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)

Deriving instances

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.

The Category and 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.”

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...