by Tom Ellis on 9th September 2012
ApplicativesJasper Van der Jeugt recently posted an article on his blog (also discussed on Haskell Reddit) about defining an Applicative instance in a manner reminiscent of Operational’s Free Monad implementation. The datatype is Table
data Table t f where
-- Applicative interface:
-- <$>, pure and <*>
Map :: (a -> b) -> Table t a -> Table t b
Pure :: a -> Table t a
App :: Table t (a -> b) -> Table t a -> Table t b
-- Primitives
Column :: Field a => FieldInfo t a -> Table t aand it is given Functor and Applicative instances
instance Functor (Table t) where
fmap = Map
instance Applicative (Table t) where
pure = Pure
(<*>) = AppThese instances make me uncomfortable, as they do not satisfy the required Functor laws and Applicative laws up to equality of the GADT terms. For example in the Functor instance, fmap id (Pure ()) is Map id (Pure ()) instead of Pure (). In the Applicative instance pure id <*> pure () is App (Pure id) (Pure ()) instead of Pure ().
Operational’s response to this issue is to not export the constructors of ProgramT, its Free Monad-constructing datatype. Thus you cannot observe the violation of the laws, but nonetheless I feel uneasy about these kinds of constructions.
ApplicativesIs it possible to define general Free Applicatives in such a way that the laws are satisfied up to term equality for the datatype? The answer is “almost” or “yes, with a caveat”. I’m not sure which, for reasons outlined at the end.
> {-# LANGUAGE ExistentialQuantification #-}
>
> import Control.Applicative The main data structure is a ChainA f a b where f :: * -> *, a :: *, b :: *. ChainA f a b contains a non-empty “list” of elements of type f (domain -> range) where domain and range can vary throughout the list, subject to the restriction that the domain of one element matches the range of the next element. These chains represent function composition under an Applicative. The “list” structure is required here for normalisation. A “tree” structure of compositions would not be normalised.
> data ChainA f a b = Single (f (a -> b)) | forall c. Many (f (c -> b)) (ChainA f a c)
>
> instance Functor f => Functor (ChainA f a) where
> fmap f (Single t) = Single (fmap (f .) t)
> fmap f (Many g v) = Many (fmap (f .) g) v A ChainA f b c can be composed with a ChainA f a b to give a ChainA f a c. This is analogous to list concatenation.
> chain :: ChainA f b c -> ChainA f a b -> ChainA f a c
> chain (Single t) v = Many t v
> chain (Many t ts) v = Many t (chain ts v) The Free Applicative on a Functor f is then given by FreeA f, where
> data FreeA f a = Pure a | ChainA (ChainA f () a) By keeping the Pure constructor out of ChainA we prevent the potential denormalisation of chaining Pure with Pure.
Functor and Applicative instances for this are very straightforward, with the possible exception of ChainA f <*> ChainA g. For this we have to use pullUnit to change a ChainA f () (b -> c) into a ChainA f b c. This is a very natural operation on Applicatives.
> instance Functor f => Functor (FreeA f) where
> fmap f (Pure a) = Pure (f a)
> fmap f (ChainA a) = ChainA (fmap f a)
>
> instance Functor f => Applicative (FreeA f) where
> pure = Pure
> Pure f <*> g = fmap f g
> f <*> Pure g = fmap ($ g) f
> ChainA f <*> ChainA g = ChainA $ chain (pullUnit f) g pullUnit is defined in terms of some messy-looking functions, but their meaning is completely apparent from their type signatures. It feels that they must be the only possible functions with these type signatures, though I do not know how to prove this.
The ability to perform these transformations seems to be essential to what it means to be an Applicative. I am tempted to formulate a conjecture (along the lines of a similar characterisation of monads) that an Applicative is exactly a Category that possesses some of these transformations satisfying certain properties.
> pullUnit :: Functor f => ChainA f () (b -> c) -> ChainA f b c
> pullUnit = removeUnit . pull
>
> pass :: Functor f => ChainA f a b -> ChainA f (a,c) (b,c)
> pass (Single t) = Single (fmap (\f -> \(a,c) -> (f a, c)) t)
> pass (Many t ts) = Many (fmap (\f -> \(a,c) -> (f a, c)) t) (pass ts)
>
> pull :: Functor f => ChainA f a (b -> c) -> ChainA f (a,b) c
> pull (Single t) = Single (fmap uncurry t)
> pull (Many t ts) = Many (fmap uncurry t) (pass ts)
>
> removeUnit :: Functor f => ChainA f ((), a) b -> ChainA f a b
> removeUnit (Single t) = Single (fmap (\f -> \a -> f ((),a)) t)
> removeUnit (Many t ts) = Many t (removeUnit ts) Three of the Applicative laws are trivial:
pure id <*> v = vpure f <*> pure x = pure (f x)u <*> pure y = pure ($ y) <*> uand one is tricky:
pure (.) <*> u <*> v <*> w = u <*> (v <*> w)i.e. first and second are required to be equal, where
> first :: Applicative f => f (b -> c) -> f (a -> b) -> f a -> f c
> first u v w = pure (.) <*> u <*> v <*> w
>
> second :: Applicative f => f (b -> c) -> f (a -> b) -> f a -> f c
> second u v w = u <*> (v <*> w) If you follow through the definitions for <*> you will find that second leads to a ChainA f () c sequence where the elements have types f b c, f a b, f () a. On the other hand, first leads to a composition chain of the types f (a -> b, a) c, f a (a -> b, a), f () a. On the face of it the two cannot be equal since their elements have different types. However, given the existential quantification in the definition of Many it is not clear to me that there is any Haskell function that can tell them apart. If anyone knows the answer please tell me! It would be great to have a Free Applicative implementation that genuinely satisfies the Applicative laws. I would also welcome hearing about any other approaches to Free Applicatives.