Good examples of Not a Functor/Functor/Applicative/Monad?
Asked Answered
F

5

234

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!

Ferebee answered 28/8, 2011 at 10:42 Comment(8)
Is it possible to make a type constructor (* -> *) for which there exists no suitable fmap?Craftwork
Owen, I think a -> String is not a functor.Ferebee
@Ferebee @Craftwork a -> String is a mathematical functor, but not a Haskell Functor, to be clear.Glazer
@J. Abrahamson, in what sense is it a mathematical functor then? Are you talking about the category with arrows reversed?Ferebee
@Ferebee yep, exactly—a contravariant functor.Glazer
For people don't know, a contravariant functor has an fmap of type (a -> b) -> f b -> f aHemitrope
See Typeclassopedia (and make it better by adding examples from here where appropriate).Kirwan
blog.functorial.com/posts/2015-12-06-Counterexamples.htmlFrediafredie
E
108

A type constructor which is not a Functor:

newtype T a = T (a -> Int)

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:

fmap      :: Functor f       => (a -> b) -> f a -> f b
contramap :: Contravariant f => (a -> b) -> f b -> f a

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 whether Data.Void is a Monoid;

instance Monoid Data.Void where
    mempty = undefined
    mappend _ _ = undefined
    mconcat _ = undefined

Since _|_ is a legal value in Haskell, and in fact the only legal value of Data.Void, this meets the Monoid rules. I am unsure what unsafeCoerce has to do with it, because your program is no longer guaranteed not to violate Haskell semantics as soon as you use any unsafe 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:

newtype T a = T {multidimensional array of a}

You can make an Applicative out of it, with something like:

mkarray [(+10), (+100), id] <*> mkarray [1, 2]
  == mkarray [[11, 101, 1], [12, 102, 2]]

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:

Functor :: * -> *
Applicative :: * -> *
Monad :: * -> *

but,

Arrow :: * -> * -> *
Ethel answered 28/8, 2011 at 11:4 Comment(38)
Good list! I would suggest using something simpler like Either a as an example for the last case, as it is easier to understand.Adulterine
Thank you! However, I thought more like <*> is the 'main' function for Applicative. An example of a functor without <*> would be nice too! Or does <*> without pure not make sense?Ferebee
@Rotsor: Hm, my wording is off. The problem is that you can implement both, but the applicative functor identities will break. I'll fix the wording.Ethel
@Dietrich, OK, I see how pure is broken (it has nowhere to take a value for Int from), but <*> could work by doing intersection of the map domains. Doesn't this bring Map Int half-way from Functor to Applicative in some(which?) sense?Ferebee
Wasn't there a recent post on planet.haskell.org that proved, that arrows are nothing more than applicative functors?Adulterine
I suspect that Map Int has a "padding" applicative behaviour. <*> combines maps pointwise where either is defined, using the image at 0 as a default if it exists. Make pure defined only at 0 and you've got your fmap behaviour.Stephan
@pigworker: I removed the example, I had thought that one of the applicative laws would break but on more thinking I realized I was wrong, since the applicative laws weren't symmetrical in the way I had intuited.Ethel
One can change Map Int to forall b. Map b to make pure impossible.Ferebee
@Rotsor: With such a type, pure _ = undefined would be a legal and correct implementation, since there are no legal values of the type anyway.Ethel
@Rotsor: Whoops, I meant pure _ = T empty, because that is the only legal value.Ethel
I meant something like forall b. Ord b => Applicative (Map b), so that the values are possible, but we don't know how to create them.Ferebee
@Rotsor: In such a case, pure x could simply be T $ fromList [(0::Int,x)], and <*> could apply the leftmost element of the left operand to all of the values in the right operand, keeping the keys, so you could make a legal Applicative instance.Ethel
@Dietrich, if you can implement Monoid for sums and products in generic way, you may want a function type to have some difficulty! :)Ferebee
@Rotsor: Unfortunately, you can create a Monoid for any function whose result is a Monoid.Ethel
Floating point numbers are, strictly, speaking, not genuine Monoids because they fail associativity, no?Shall
@sclv: Anything with a finite set of values can considered to be a cyclic Monoid, whether it makes sense to do so or not.Ethel
And of course I just realized that anything with a total ordering can be a monoid on min/max (and you can assign just about anything an arbitrary enough partial ordering) so... erp.Shall
If you're still looking for a type constructor that's Applicative but not a Monad, a very common example would be ZipList.Wyrick
@JohnL: My new favorite example in this particular category is "parallelizeable database transactions", which are forced to be serial when made into a Monad.Ethel
_|_ inhabits every type in *, but the point of Void is you should have to bend over backwards to construct one or you've destroyed its value. This is why its not an instance of Enum, Monoid, etc. If you already have one, I'm happy to let you mash them together (giving you a Semigroup) but mempty, but I give no tools for explicitly constructing a value of type Void in void. You have to load the gun and point it at your foot and pull the trigger yourself.Bacteria
Pedantically, I think your notion of Cofunctor is wrong. The dual of a functor is a functor, because you flip both the input and the output and end up with just the same thing. The notion you are looking for is probably "contravariant functor", which is slightly different.Distinguished
@BenMillwood: I'm using "contravariant functor" as the definition for "cofunctor" because "contravariant functor" is an inconveniently long name for a type constructor. Wikipedia supports this usage.Ethel
@DietrichEpp: I believe this usage to be incorrect (there's no citation), have asked math.SE if they agree with me.Distinguished
Arrow fits perfectly between Applicative and Monad. Every Monad can be made into an Arrow (Kleisli Arrows) and every Arrow (with the first parameter given) is Applicative (WrappedArrow). The kind mismatch is irrelevant.Gallstone
Hello, sorry for bringing up old question, but is there some unobvious example of basic Haskell built-in type (meaning not some esoteric one) looking like a monad but not being one?Fulmis
@DanM.: I'm not sure what you mean by "looks like a monad", and there aren't really very many basic built-in types in Haskell (by "built-in" do you mean "in the Prelude"?)Ethel
@DietrichEpp yeah, I mean that are standard and widely used, not your own custom one. I found ZipList, but I'm not that familiar with it (I used zip/ zipWith functions, but didn't know about it. Also Set might be a good example.Fulmis
@DanM.: Set can't be a monad because it's not even a functor, because it imposes structure on its members. ZipList doesn't "look like" a monad to me. One of the problems here is that "looks like a monad" is a very subjective question.Ethel
@DietrichEpp however I've seen some successful(to some degree) attempts at making Set monadic (like by using Cont monad). ALso, there is this package: hackage.haskell.org/package/set-monad Yeah, I guess it's kinda subjective. I was just looking for types that can be confused with monad, but in actuality are not.Fulmis
@DietrichEpp hello, 5 years have passed and now cofunctor is deprecated. Also, according to this MO question, functor is self-dual, so it will be misleading to call contravariant functor cofunctor. Please update the answer, because it is so great for beginners like me!Empery
@AlexVong: "Deprecated" --> people are just using a different package. Talking about "contravariant functor" not "dual of functor", sorry for the confusion. In some contexts I've seen "cofunctor" used to refer to "contravariant functors" because functors are self-dual, but it appears to just be confusing people.Ethel
I think that the multi-dimensional array as an example of an applicative-functor-not-a-monad is not quite correct. Why exactly is it impossible to define a monad instance for that type constructor? Below (in my answer to this question) I give specific examples of applicative functors that are either monads or not monads. In particular, a type constructor F a that contains a product of any number of a's is always a monad.Gun
@winitzki: The reason it is impossible is because of the dimensions mismatch. The rank of the multidimensional array is not encoded in the type, it is encoded in the value. I don't think what you are describing is an equivalent structure.Ethel
@winitzki: If it helps, think of <*> as being a tensor product, except with function application instead of multiplication.Ethel
@DietrichEpp I don't follow what you are saying. Can you point to a specific example code for the multidimensional array? Also I don't see how it helps to look at <*> as tensor product. I'd rather agree that the monoidal operation mult: F a -> F b -> F (a, b) is similar to a tensor product. But I still don't see how this helps to verify that tensor arrays have no monad instance.Gun
It's not that tensors have no monad instance, it's that any monad instance couldn't be an extension of the applicative functor instance I've described.Ethel
For any type e that's not pointed, (e,-) is a functor but not an applicative.Slander
System.Console.GetOpt.ArgDescr for instance is a functor, but not applicative, and cannot be made applicative (or a monoid) either, because it has multiple constructors containing its type argument. An easier example would be data NotApplicative a = NALeft a | NARight a. You'd have to somehow come up with a way to compose the information about if it's NALeft or NARight to get anywhere, which is possible, but I don't think there's anything you could read from the type definition alone.Electrometer
S
91

My style may be cramped by my phone, but here goes.

newtype Not x = Kill {kill :: x -> Void}

cannot be a Functor. If it were, we'd have

kill (fmap (const ()) (Kill id)) () :: Void

and the Moon would be made of green cheese.

Meanwhile

newtype Dead x = Oops {oops :: Void}

is a functor

instance Functor Dead where
  fmap f (Oops corpse) = Oops corpse

but cannot be applicative, or we'd have

oops (pure ()) :: Void

and Green would be made of Moon cheese (which can actually happen, but only later in the evening).

(Extra note: Void, as in Data.Void is an empty datatype. If you try to use undefined to prove it's a Monoid, I'll use unsafeCoerce to prove that it isn't.)

Joyously,

newtype Boo x = Boo {boo :: Bool}

is applicative in many ways, e.g., as Dijkstra would have it,

instance Applicative Boo where
  pure _ = Boo True
  Boo b1 <*> Boo b2 = Boo (b1 == b2)

but it cannot be a Monad. To see why not, observe that return must be constantly Boo True or Boo False, and hence that

join . return == id

cannot possibly hold.

Oh yeah, I nearly forgot

newtype Thud x = The {only :: ()}

is a Monad. Roll your own.

Plane to catch...

Stephan answered 28/8, 2011 at 12:9 Comment(21)
I was under the impression that Dead x could be applicative as long as Void is a Monoid, which is certainly the case if it is a singleton... what is Void, exactly?Ethel
Void is empty! Morally, anyhow.Stephan
Void is a type with 0 constructors, I assume. It's not a monoid because there is no mempty.Ferebee
If it has no constructors, then pure _ = undefined and _ <*> _ = undefined are legal and follow the Applicative rules.Ethel
@Dietrich, undefined is not really a value, so this reasoning is broken. <*> is indeed possible, but it requires a pattern-match with 0 clauses, syntactically prohibited in Haskell, but pure can be called, but can not possibly return a value.Ferebee
undefined? How rude! Sadly, unsafeCoerce (unsafeCoerce () <*> undefined) is not (), so in real life, there are observations which violate the laws.Stephan
What? Undefined (or _|_) is really a value... it is the only value of type Void, for instance. Since Oops is strict, all values of type Dead x are therefore also _|_.Ethel
@pigworker: unsafeCoerce has the word "unsafe" in it, which indicates that it CAN be used to violate Haskell's semantics. On the other hand, undefined is a well-defined part of Haskell's semantics.Ethel
@Dietrich, this may be a valid point. It shows that Haskell does not have empty data types then.Ferebee
In the usual semantics, which tolerates exactly one kind of undefined, you're quite right. There are other semanticses, of course. Void does not restrict to a submonoid in the total fragment. Nor is it a monoid in a semantics which distinguishes modes of failure. When I have a moment with easier than phone-based editing, I'll clarify that my example works only in a semantics for which there is not exactly one kind of undefined.Stephan
@Dietrich Epp: Let's say that we've chosen, as Curry said, not to run away from paradoxes. _|_ is a "value" in some senses, but obviously we can't observe it directly. However, we can observe aspects of a _|_ in other ways, such as by catching exceptions in IO, or personally observing nontermination vs. error. So, as we leave the "close your eyes and pretend this is Agda" realm that calls Void an empty type, can you show that your proposed Applicative instance will obey the laws as applied to what sort of _|_ it produces?Diannediannne
@C. A. McCann: Catching exceptions in the IO monad is the kind of "open secret" way to violate Haskell semantics; which is why IO is called "impure" even though it is monadically well-typed. You are essentially asking a function f :: _|_ -> _|_ to preserve the precise bottom value, when, according to Haskell's denotational semantics there is only one such value in the first place. And if the Applicative laws were not written for Haskell's denotational semantics, what were they written for?Ethel
@Dietrich Epp: That type doesn't make sense. _|_ is a value, not a type, and in fact I don't believe there's even anything that says _|_ values of different types can be compared, even conceptually. I doubt it even makes sense to consider equality of _|_s of the same type, so I'm not sure that satisfying type class laws is even a well-formed question in the first place without introducing something that lets you compare _|_ values somehow.Diannediannne
@C. A. McCann: _|_ in the type signature was shorthand for a type which contains only that value. (Denotational semantics are clear: there is only one _|_.) However, I think the root problem here is that we don't really grok how _|_ is supposed to interact with these identities in the first place, choosing Void is just forcing us to deal with it. On different lines, if we decide that we cannot consider equality of _|_, then newtype T a = T Void also fails to be a Functor, in addition to failing to be Applicative.Ethel
@Dietrich Epp: There's also only one [], but asking whether empty lists of different types are equal remains nonsense; also, I'm not sure if semantic uniqueness actually justifies using _|_ in... equivalences? Equalities? Identities? Whatever type class laws actually are, if that's even well-defined (I'm actually pretty sure they can't be identities). The Functor instance is far less questionable because it dodges the issue by merely preserving an existing _|_ rather than introducing or removing _|_ values.Diannediannne
@C. A. McCann: I'm not sure why you think I'm comparing values of different types. The real problem here, as I said, is we never really defined what _|_ means in the Applicative laws. But Haskell semantics are about substitutability: I can substitute my 12 for your 12 without complaint, _|_ should not get special treatment. And there's something especially bizarre about complaining about getting the "wrong" value of a Void type.Ethel
@Stephan You claim that unsafeCoerce (unsafeCoerce () <*> undefined) is not () and hence this is a bad Applicative instance, but none of the Applicative laws seems to be of that form. (All the equations with one instance of <*> on some side also have pure on that side, according to this list.) What makes you think this wacky expression ought to evaluate to ()?Bouie
@Dietrich Epp IMO the Applicative laws are written for the PER of total values of Haskell's denotational semantics. See Fast and Loose Reasoning is Morally Correct.Lovato
you can make legitimately make anything from a "value" in Void, for example, a proof of a false equation between types; of course, the only problem is that your data become mined with bottoms, so as long as crashing out or looping with bottom are not considered "going wrong", nothing will go wrongStephan
A recent question got me very curious about Functor instances that cannot be made instances of Apply. If you have the time, I'd love if you'd weigh in.Boulevard
Most of the silly data types used in this answer are isomorphic to real ones. For example, Dead is isomorphic to V1 and Thud is isomorphic to Proxy.Lusitania
W
82

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:

instance Functor ((,) r) where
    fmap f (x,y) = (x, f y)

But there is no way how to define its Applicative instance without imposing additional restrictions on r. In particular, there is no way how to define pure :: a -> (r, a) for an arbitrary r.

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 different Applicative instance for them.)

fmap is defined in the usual way. But pure and <*> are defined as

pure x                    = ZipList (repeat x)
ZipList fs <*> ZipList xs = ZipList (zipWith id fs xs)

so 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:

We revisit the connection between three notions of computation: Moggi's monads, Hughes's arrows and McBride and Paterson's idioms (also called applicative functors). We show that idioms are equivalent to arrows that satisfy the type isomorphism A ~> B = 1 ~> (A -> B) and that monads are equivalent to arrows that satisfy the type isomorphism A ~> B = A -> (1 ~> B). Further, idioms embed into arrows and arrows embed into monads.

Weak answered 27/8, 2012 at 6:32 Comment(3)
So ((,) r) is a functor that is not an applicative; but this is only because you can't generally define pure for all r at once. It's therefore a quirk of language conciseness, of trying to define an (infinite) collection of applicative functors with one definition of pure and <*>; in this sense, there doesn't seem to be anything mathematically deep about this counter-example since, for any concrete r, ((,) r) can be made an applicative functor. Question: Can you think of a CONCRETE functor which fails to be an applicative?Tomkins
See #44125984 as post with this question.Tomkins
@George, no, it is not true. If r does not have any element in it, you cannot implement pure for that even if you can give fmap.Anthropomorphize
M
22

A good example for a type constructor which is not a functor is Set: You can't implement fmap :: (a -> b) -> f a -> f b, because without an additional constraint Ord b you can't construct f b.

Mccall answered 29/8, 2011 at 6:59 Comment(5)
It is actually a good example since mathematically we would really like to make this a functor.Scumble
@AlexandreC. I'd disagree on that, it's not a good example. Mathematically, such a data structure does form a functor. The fact that we cannot implement fmap is just a language/implementation issue. Also, it's possible to wrap Set into the continuation monad, which makes a monad out of it with all the properties we'd expect, see this question (although I'm not sure if it can be done efficiently).Weak
@PetrPudlak, how is this a language issue? Equality of b may be undecidable, in that case you can't define fmap!Putscher
@Putscher Being decidable and definable are two different things. For example it's possible to correctly define equality on lambda terms (programs), even though it's not possible to decide it by an algorithm. In any case, this wasn't the case of this example. Here the problem is that we can't define a Functor instance with the Ord constraint, but it might be possible with a different definition of Functor or better language support. Actually with ConstraintKinds it is possible to define a type class that can be parametrized like this.Weak
Even if we could overcome the ord constraint the fact that a Set cannot contain duplicate entries means that fmap could altar the context. This violates the associativity law.Evalynevan
G
17

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:

  1. Cannot implement the type signatures of the required methods from the type class.
  2. Can implement the type signatures but cannot satisfy the required laws.

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

  • A type constructor that cannot have a functor instance because the type cannot be implemented:

    data F z a = F (a -> z)
    

This is a contrafunctor, not a functor, with respect to the type parameter a, because a in a contravariant position. It is impossible to implement a function with type signature (a -> b) -> F z a -> F z b.

  • A type constructor that is not a lawful functor even though the type signature of 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 though F cannot possibly be a functor because it uses a in a contravariant position. So this implementation of fmap 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. For example, fmap idid, because let (Q(f,_)) = fmap id (Q(read,"123")) in f "456" is 123, but let (Q(f,_)) = id (Q(read,"123")) in f "456" is 456.

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 that w should be a monoid. It is then impossible to construct a value of type (a, w) out of a.

  • 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 uses a only in covariant positions.

instance Functor P where
   fmap :: (a -> b) -> P a -> P b
   fmap fab (P pa) = P (\q -> fmap fab $ pa (q . fab))

The only possible implementation of the type signature of <*> is a function that always returns Nothing:

 (<*>) :: P (a -> b) -> P a -> P b
 (P pfab) <*> (P pa) = \_ -> Nothing  -- fails the laws!

But this implementation does not satisfy the identity law for applicative functors.

  • A functor that is Applicative but not a Monad because the type signature of bind cannot be implemented.

I do not know any such examples!

  • A functor that is Applicative but not a Monad because laws cannot be satisfied even though the type signature of bind 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.

 data B a = Maybe (a, a)
   deriving Functor

 instance Applicative B where
   pure x = Just (x, x)
   b1 <*> b2 = case (b1, b2) of
     (Just (x1, y1), Just (x2, y2)) -> Just((x1, x2), (y1, y2))
     _ -> Nothing

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 implementing bind when a function f :: a -> B b could return Nothing or Just for different values of a.

It is perhaps clearer to consider Maybe (a, a, a), which is also not a monad, and to try implementing join for that. One will find that there is no intuitively reasonable way of implementing join.

 join :: Maybe (Maybe (a, a, a), Maybe (a, a, a), Maybe (a, a, a)) -> Maybe (a, a, a)
 join Nothing = Nothing
 join Just (Nothing, Just (x1,x2,x3), Just (y1,y2,y3)) = ???
 join Just (Just (x1,x2,x3), Nothing, Just (y1,y2,y3)) = ???
 -- etc.

In the cases indicated by ???, it seems clear that we cannot produce Just (z1, z2, z3) in any reasonable and symmetric manner out of six different values of type a. We could certainly choose some arbitrary subset of these six values, -- for instance, always take the first nonempty Maybe - but this would not satisfy the laws of the monad. Returning Nothing will also not satisfy the laws.

  • A tree-like data structure that is not a monad even though it has associativity for bind - but fails the identity laws.

The usual tree-like monad (or "a tree with functor-shaped branches") is defined as

 data Tr f a = Leaf a | Branch (f (Tr f a))

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 with type 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 has bind that satisfies the naturality and the associativity laws, but its pure method fails one of the identity laws. "Semimonads are semigroups in the category of endofunctors, what's the problem?" This is the type class Bind.

For simplicity, I define the join method instead of bind:

 data Trs f a = Leaf (f a) | Branch (f (Trs f a))
 join :: Trs f (Trs f a) -> Trs f a
 join (Leaf ftrs) = Branch ftrs
 join (Branch ftrstrs) = Branch (fmap @f join ftrstrs)

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) and Maybe (a, a, a) can be given a lawful Monad instance, although they are obviously Applicative.

These functors have no tricks - no Void or bottom anywhere, no tricky laziness/strictness, no infinite structures, and no type class constraints. The Applicative instance is completely standard. The functions return and bind 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 functor data P12 a = Either a (a, a) is also a monad.

Constructions for polynomial monads

In general, here are some constructions that produce lawful Monads out of polynomial types. In all these constructions, M is a monad:

  1. type M a = Either c (w, a) where w is any monoid
  2. type M a = m (Either c (w, a)) where m is any monad and w is any monoid
  3. type M a = (m1 a, m2 a) where m1 and m2 are any monads
  4. type M a = Either a (m a) where m is any monad

The first construction is WriterT w (Either c), the second construction is WriterT w (EitherT c m). The third construction is a component-wise product of monads: pure @M is defined as the component-wise product of pure @m1 and pure @m2, and join @M is defined by omitting cross-product data (e.g. m1 (m1 a, m2 a) is mapped to m1 (m1 a) by omitting the second part of the tuple):

 join :: (m1 (m1 a, m2 a), m2 (m1 a, m2 a)) -> (m1 a, m2 a)
 join (m1x, m2x) = (join @m1 (fmap fst m1x), join @m2 (fmap snd m2x))

The fourth construction is defined as

 data M m a = Either a (m a)
 instance Monad m => Monad M m where
    pure x = Left x
    join :: Either (M m a) (m (M m a)) -> M m a
    join (Left mma) = mma
    join (Right me) = Right $ join @m $ fmap @m squash me where
      squash :: M m a -> m a
      squash (Left x) = pure @m x
      squash (Right ma) = ma

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 monads a, a, and Maybe a. Also, Either (a,a) (a,a,a,a) is monadic because it is isomorphic to the product of a and Either 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 example Either (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 constructor type F a = Either a (a, a) can be given a Monad instance in two ways: by construction 4 using the monad (a, a), and by construction 3 using the type isomorphism Either 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.

Gun answered 7/4, 2018 at 4:16 Comment(26)
I think B is a monad. Can you give a counterexample to this bind Pair x y >>= f = case (f x, f y) of (Pair x' _,Pair _ y') -> Pair x' y' ; _ -> Empty?Ephrem
@Ephrem Associativity fails with this definition when you choose f such that f x is Empty but f y is a Pair, and on the next step both are Pair. I checked by hand that the laws do not hold for this implementation or for any other implementation. But it's a fair bit of work to do that. I wish there were an easier way to figure this out!Gun
@Gun How does associativity fail? Wouldn't you get Empty in either case?Hogg
B b1 <*> B b2 = ... makes no sense, since B is not a value constructor. Also, I think Pair (x1, x2) (y1, y2) has the wrong type, should that be Pair (x1 x2) (y1 y2) ?Kris
Yes you are right @Kris - my Haskell syntax is rusty.Gun
Just to clarify: In Either a (m a), did you intend to have a twice? If so, it might bear some explanation -- I don't think that monad former is one of the ones well-known to Haskell folks. If not, then the first case of type L a = Either c (w, a) is completely subsumed by the second case, since (w, a) is the writer monad.Bouie
@DanielWagner Yes, it is specifically intended to have a twice. This is a nontrivial construction.Gun
How do you really prove that there is no Monad instance? Your argument "there is no natural way of implementing bind when a function f :: a -> B b could return Empty or Pair for different values of a" works for Maybe as well.Putscher
@Putscher That argument doesn't apply to Maybe because Maybe doesn't contain different values of a to worry about.Bouie
@Putscher I proved this by a couple of pages of calculations; the argument about "natural way" is just a heuristic explanation. A Monad instance consists of functions return and bind that satisfy laws. There are two implementations of return and 25 implementations of bind that fit the required types. You can show by direct calculation that none of the implementations satisfy the laws. To cut down on the amount of required work, I used join instead of bind and used the identity laws first. But it's been a fair bit of work.Gun
@Hogg I looked back at my calculations and you are right, - it is not associativity that fails in this case, it is one of the identity laws.Gun
The accepted answer to this question, #13034729, claims that Maybe (a, a) is not a monad, and gives a partial proof. I have a complete proof but it's long.Gun
From a comment in that question: So, in short: monads are allowed to throw away information, and that's okay if they're just nested in themselves. But when you have an info-preserving monad and an info-dropping monad, combining the two drops information, even though the info-preserving one needs that info kept to satisfy its own monad laws. So you can't combine arbitrary monads. (This is why you need Traversable monads, which guarantee they won't drop relevant information; they're arbitrarily composable.) Correction: composing works only in one way: (Maybe a, Maybe a) is a monad.Gun
A question with counter examples where the monad fails can be found here: #49742877Ephrem
A very interesting answer. A quick parenthetical question: does your Either a (m a) instance needs Traversable m? I'd suppose so, as if you were writing join it seems you'd need to change m (Either a (m a)) into Either a (m (m a)). (That doesn't qualify as an objection to your instance, as all polynomial functors are Traversable.)Kennethkennett
@Kennethkennett No, I don't think Traversable is needed. m (Either a (m a)) is transformed using pure @m into m (Either (m a) (m a)). Then trivially Either (m a) (m a) -> m a, and we can use join @m. That was the implementation for which I checked the laws.Gun
@Gun Oh, nice! That had escaped me somehow. (I still have to check if instance using Traversable is lawful. I guess it isn't -- not for all m, at least.)Kennethkennett
Though you have already realised that (cf. this comment of yours in the other question), you might want to update this answer to account for Either (a,a) (a,a,a,a) actually being a monad -- it is isomorphic to (a, Either a (a,a,a)).Kennethkennett
@Kennethkennett Yes, thank you - I have updated the answer. Actually, a Monad instance can be defined for any sum of any number of product of any number of as, and possibly in more than one way. The practical usefulness of any of these monads remains to be determined. For example, what could be a use case for something like Either (a, a, a) (a, a, a, a, a)?Gun
@Gun "[...] possibly in more than one way" -- Yup, it's a beautiful mess. Either a (a, a) has the two instances described here, which correspond to (warning: abuse of notation) a + a^2 and a * (1 + a). If you upgrade it to One a | Two a a | Three a a a, you get two instances by factoring it as either a + (a * (a + a^2)) or a + (a^2 * (1 + a)) -- they are subtly different, in a way I can't quite explain in words. Clarifying how emptiness (as in Maybe (a, a) / 1 + a^2) gets in the way might help making sense of it all.Kennethkennett
@Kennethkennett Thank you, I reorganized and edited my answer with your example in mind.Gun
@Gun This expanded answer is really nice. By the way, I should review my own answer about diagonals in the other question -- it feels a little coarse after this discussion.Kennethkennett
The claim that a type-correct fmap for data F a = F (a -> Int) can't be written is false: fmap _ _ = F (\_ -> 0). The only problem with it is that it's unlawful.Lusitania
@JosephSible Thank you, I corrected the text. The example should be correct now. (a -> z instead of a -> Int)Gun
Today I read the original Applicative programming with effects paper. It contains an example of A functor that is Applicative but not a Monad because the type signature of bind can't be implemented.: newtype Accy o a = Acc{acc :: o } contains the phantom type a. As such, (>>=) :: Accy o a → (a → Accy o b) → Accy o b cannot be implemented because there is no way to ever construct an a.Pulmotor
@Pulmotor Yes, this is a good example. It corresponds to a constant functor (that does not depend on its type parameter). Constant functors are monads only when they are of type Unit.Gun

© 2022 - 2024 — McMap. All rights reserved.