While explaining to someone what a type class X is I struggle to find good examples of data structures which are exactly X.
So, I request examples for:
- A type constructor which is not a Functor.
- A type constructor which is a Functor, but not Applicative.
- A type constructor which is an Applicative, but is not a Monad.
- A type constructor which is a Monad.
I think there are plenty examples of Monad everywhere, but a good example of Monad with some relation to previous examples could complete the picture.
I look for examples which would be similar to each other, differing only in aspects important for belonging to the particular type class.
If one could manage to sneak up an example of Arrow somewhere in this hierarchy (is it between Applicative and Monad?), that would be great too!
I believe the other answers missed some simple and common examples:
A type constructor which is a Functor but not an Applicative. A simple example is a pair:
But there is no way how to define its
Applicative
instance without imposing additional restrictions onr
. In particular, there is no way how to definepure :: a -> (r, a)
for an arbitraryr
.A type constructor which is an Applicative, but is not a Monad. A well-known example is ZipList. (It's a
newtype
that wraps lists and provides differentApplicative
instance for them.)fmap
is defined in the usual way. Butpure
and<*>
are defined asso
pure
creates an infinite list by repeating the given value, and<*>
zips a list of functions with a list of values - applies i-th function to i-th element. (The standard<*>
on[]
produces all possible combinations of applying i-th function to j-th element.) But there is no sensible way how to define a monad (see this post).How arrows fit into the functor/applicative/monad hierarchy? See Idioms are oblivious, arrows are meticulous, monads are promiscuous by Sam Lindley, Philip Wadler, Jeremy Yallop. MSFP 2008. (They call applicative functors idioms.) The abstract:
A good example for a type constructor which is not a functor is
Set
: You can't implementfmap :: (a -> b) -> f a -> f b
, because without an additional constraintOrd b
you can't constructf b
.My style may be cramped by my phone, but here goes.
cannot be a Functor. If it were, we'd have
and the Moon would be made of green cheese.
Meanwhile
is a functor
but cannot be applicative, or we'd have
and Green would be made of Moon cheese (which can actually happen, but only later in the evening).
(Extra note:
Void
, as inData.Void
is an empty datatype. If you try to useundefined
to prove it's a Monoid, I'll useunsafeCoerce
to prove that it isn't.)Joyously,
is applicative in many ways, e.g., as Dijkstra would have it,
but it cannot be a Monad. To see why not, observe that return must be constantly
Boo True
orBoo False
, and hence thatcannot possibly hold.
Oh yeah, I nearly forgot
is a Monad. Roll your own.
Plane to catch...
A type constructor which is not a Functor:
You can make a contravariant functor out of it, but not a (covariant) functor. Try writing
fmap
and you'll fail. Note that the contravariant functor version is reversed:A type constructor which is a functor, but not Applicative:
I don't have a good example. There is
Const
, but ideally I'd like a concrete non-Monoid and I can't think of any. All types are basically numeric, enumerations, products, sums, or functions when you get down to it. You can see below pigworker and I disagreeing about whetherData.Void
is aMonoid
;Since
_|_
is a legal value in Haskell, and in fact the only legal value ofData.Void
, this meets the Monoid rules. I am unsure whatunsafeCoerce
has to do with it, because your program is no longer guaranteed not to violate Haskell semantics as soon as you use anyunsafe
function.See the Haskell Wiki for an article on bottom (link) or unsafe functions (link).
I wonder if it is possible to create such a type constructor using a richer type system, such as Agda or Haskell with various extensions.
A type constructor which is an Applicative, but not a Monad:
You can make an Applicative out of it, with something like:
But if you make it a monad, you could get a dimension mismatch. I suspect that examples like this are rare in practice.
A type constructor which is a Monad:
About Arrows:
Asking where an Arrow lies on this hierarchy is like asking what kind of shape "red" is. Note the kind mismatch:
but,
I'd like to propose a more systematic approach to answering this question, and also to show examples that do not use any special tricks like the "bottom" values or infinite data types or anything like that.
When do type constructors fail to have type class instances?
In general, there are two reasons why a type constructor could fail to have an instance of a certain type class:
Examples of the first kind are easier than those of the second kind because for the first kind, we just need to check whether one can implement a function with a given type signature, while for the second kind, we are required to prove that no implementation could possibly satisfy the laws.
Specific examples
data F a = F (a -> Int)
This is a contrafunctor, not a functor, because it uses the type parameter
a
in a contravariant position. It is impossible to implement a function with type signature(a -> b) -> F a -> F b
.fmap
can be implemented:data Q a = Q(a -> Int, a) fmap :: (a -> b) -> Q a -> Q b fmap f (Q(g, x)) = Q(\_ -> g x, f x) -- this fails the functor laws!
The curious aspect of this example is that we can implement
fmap
of the correct type even thoughF
cannot possibly be a functor because it usesa
in a contravariant position. So this implementation offmap
shown above is misleading - even though it has the correct type signature (I believe this is the only possible implementation of that type signature), the functor laws are not satisfied (this requires some simple computations to check).In fact,
F
is only a profunctor, - it is neither a functor nor a contrafunctor.A lawful functor that is not applicative because the type signature of
pure
cannot be implemented: take the Writer monad(a, w)
and remove the constraint thatw
should be a monoid. It is then impossible to construct a value of type(a, w)
out ofa
.A functor that is not applicative because the type signature of
<*>
cannot be implemented:data F a = Either (Int -> a) (String -> a)
.A functor that is not lawful applicative even though the type class methods can be implemented:
data P a = P ((a -> Int) -> Maybe a)
The type constructor
P
is a functor because it usesa
only in covariant positions.The only possible implementation of the type signature of
<*>
is a function that always returnsNothing
:But this implementation does not satisfy the identity law for applicative functors.
Applicative
but not aMonad
because the type signature ofbind
cannot be implemented.I do not know any such examples!
Applicative
but not aMonad
because laws cannot be satisfied even though the type signature ofbind
can be implemented.This example has generated quite a bit of discussion, so it is safe to say that proving this example correct is not easy. But several people have verified this independently by different methods. See Is `data PoE a = Empty | Pair a a` a monad? for additional discussion.
It is somewhat cumbersome to prove that there is no lawful
Monad
instance. The reason for the non-monadic behavior is that there is no natural way of implementingbind
when a functionf :: a -> B b
could returnNothing
orJust
for different values ofa
.It is perhaps clearer to consider
Maybe (a, a, a)
, which is also not a monad, and to try implementingjoin
for that. One will find that there is no intuitively reasonable way of implementingjoin
.In the cases indicated by
???
, it seems clear that we cannot produceJust (z1, z2, z3)
in any reasonable and symmetric manner out of six different values of typea
. We could certainly choose some arbitrary subset of these six values, -- for instance, always take the first nonemptyMaybe
- but this would not satisfy the laws of the monad. ReturningNothing
will also not satisfy the laws.bind
- but fails the identity laws.The usual tree-like monad (or "a tree with functor-shaped branches") is defined as
This is a free monad over the functor
f
. The shape of the data is a tree where each branch point is a "functor-ful" of subtrees. The standard binary tree would be obtained withtype f a = (a, a)
.If we modify this data structure by making also the leaves in the shape of the functor
f
, we obtain what I call a "semimonad" - it hasbind
that satisfies the naturality and the associativity laws, but itspure
method fails one of the identity laws. "Semimonads are semigroups in the category of endofunctors, what's the problem?" This is the type classBind
.For simplicity, I define the
join
method instead ofbind
:The branch grafting is standard, but the leaf grafting is non-standard and produces a
Branch
. This is not a problem for the associativity law but breaks one of the identity laws.When do polynomial types have monad instances?
Neither of the functors
Maybe (a, a)
andMaybe (a, a, a)
can be given a lawfulMonad
instance, although they are obviouslyApplicative
.These functors have no tricks - no
Void
orbottom
anywhere, no tricky laziness/strictness, no infinite structures, and no type class constraints. TheApplicative
instance is completely standard. The functionsreturn
andbind
can be implemented for these functors but will not satisfy the laws of the monad. In other words, these functors are not monads because a specific structure is missing (but it is not easy to understand what exactly is missing). As an example, a small change in the functor can make it into a monad:data Maybe a = Nothing | Just a
is a monad. Another similar functordata P12 a = Either a (a, a)
is also a monad.Constructions for polynomial monads
In general, here are some constructions that produce lawful
Monad
s out of polynomial types. In all these constructions,M
is a monad:type M a = Either c (w, a)
wherew
is any monoidtype M a = m (Either c (w, a))
wherem
is any monad andw
is any monoidtype M a = (m1 a, m2 a)
wherem1
andm2
are any monadstype M a = Either a (m a)
wherem
is any monadThe first construction is
WriterT w (Either c)
, the second construction isWriterT w (EitherT c m)
. The third construction is a component-wise product of monads:pure @M
is defined as the component-wise product ofpure @m1
andpure @m2
, andjoin @M
is defined by omitting cross-product data (e.g.m1 (m1 a, m2 a)
is mapped tom1 (m1 a)
by omitting the second part of the tuple):The fourth construction is defined as
I have checked that all four constructions produce lawful monads.
I conjecture that there are no other constructions for polynomial monads. For example, the functor
Maybe (Either (a, a) (a, a, a, a))
is not obtained through any of these constructions and so is not monadic. However,Either (a, a) (a, a, a)
is monadic because it is isomorphic to the product of three monadsa
,a
, andMaybe a
. Also,Either (a,a) (a,a,a,a)
is monadic because it is isomorphic to the product ofa
andEither a (a, a, a)
.The four constructions shown above will allow us to obtain any sum of any number of products of any number of
a
's, for exampleEither (Either (a, a) (a, a, a, a)) (a, a, a, a, a))
and so on. All such type constructors will have (at least one)Monad
instance.It remains to be seen, of course, what use cases might exist for such monads. Another issue is that the
Monad
instances derived via constructions 1-4 are in general not unique. For example, the type constructortype F a = Either a (a, a)
can be given aMonad
instance in two ways: by construction 4 using the monad(a, a)
, and by construction 3 using the type isomorphismEither a (a, a) = (a, Maybe a)
. Again, finding use cases for these implementations is not immediately obvious.A question remains - given an arbitrary polynomial data type, how to recognize whether it has a
Monad
instance. I do not know how to prove that there are no other constructions for polynomial monads. I don't think any theory exists so far to answer this question.