Welcome to OGeek Q&A Community for programmer and developer-Open, Learning and Share
Welcome To Ask or Share your Answers For Others

Categories

0 votes
723 views
in Technique[技术] by (71.8m points)

haskell - To what extent are Applicative/Monad instances uniquely determined?

As described this question/answers, Functor instances are uniquely determined, if they exists.

For lists, there are two well know Applicative instances: [] and ZipList. So Applicative isn't unique (see also Can GHC derive Functor and Applicative instances for a monad transformer? and Why is there no -XDeriveApplicative extension?). However, ZipList needs infinite lists, as its pure repeats a given element indefinitely.

  • Are there other, perhaps better examples of data structures that have at least two Applicative instances?
  • Are there any such examples that only involve finite data structures? That is, like if hypothetically Haskell's type system distinguished inductive and coinductive data types, would it be possible to uniquely determine Applicative?

Going further, if we could extend both [] and ZipList to a Monad, we'd have an example where a monad isn't uniquely determined by the data type and its Functor. Alas, ZipList has a Monad instance only if we restrict ourselves to infinite lists (streams). And return for [] creates a single-element list, so it requires finite lists. Therefore:

  • Are Monad instances uniquely determined by the data type? Or is there an example of a data type that can have two distinct Monad instances?

In the case there is an example with two or more distinct instances, an obvious question arises, if they must/can have the same Applicative instance:

  • Are Monad instances uniquely determined by the Applicative instance, or is there an example of an Applicative that can have two distinct Monad instances?
  • Is there an example of a data type with two distinct Monad instances, each having a different Applicative super-instance?

And finally we can ask the same question for Alternative/MonadPlus. This is complicated by the fact that there are two distinct set of MonadPlus laws. Assuming we accept one of the set of laws (and for Applicative we accept right/left distributivity/absorption, see also this question),

  • is Alternative uniquely determined by Applicative, and MonadPlus by Monad, or are there any counter-examples?

If any of the above are unique, I'd be interested in knowing why, to have a hint of a proof. If not, an counter-example.

See Question&Answers more detail:os

与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…
Welcome To Ask or Share your Answers For Others

1 Reply

0 votes
by (71.8m points)

First, since Monoids are not unique, neither are Writer Monads or Applicatives. Consider

data M a = M Int a

then you can give it Applicative and Monad instances isomorphic to either of:

Writer (Sum Int)
Writer (Product Int)

Given a Monoid instance for a type s, another isomorphic pair with different Applicative/Monad instances is:

ReaderT s (Writer s)
State s

As for having one Applicative instance extend to two different Monads, I cannot remember any example. However, back when I tried to convince myself completely about whether ZipList really cannot be made a Monad, I found the following pretty strong restriction that holds for any Monad:

join (fmap (x -> fmap (y -> f x y) ys) xs) = f <$> xs <*> ys

That doesn't give join for all values though: in the case of lists the restricted values are the ones where all elements have the same length, i.e. lists of lists with "rectangular" shape.

(For Reader monads, where the "shape" of monadic values doesn't vary, these are in fact all the m (m x) values, so those do have unique extension. EDIT: Come to think of it, Either, Maybe and Writer also have only "rectangular" m (m x) values, so their extension from Applicative to Monad is also unique.)

I wouldn't be surprised if an Applicative with two Monads exists, though.

For Alternative/MonadPlus, I cannot recall any law for instances using the Left Distribution law instead of Left Catch, I see nothing preventing you from just swapping (<|>) with flip (<|>). I don't know if there's a less trivial variation.

ADDENDUM: I suddenly remembered I had found an example of an Applicative with two Monads. Namely, finite lists. There's the usual Monad [] instance, but you can then replace its join by the following function (essentially making empty lists "infectious"):

ljoin xs
  | any null xs = []
  | otherwise   = concat xs

(Alas, the lists need to be finite because otherwise the null check will never finish, and that would ruin the join . fmap return == id monad law.)

This has the same value as join/concat on rectangular lists of lists, so will give the same Applicative. As I recall, it turns out that the first two monad laws are automatic from that, and you just need to check ljoin . ljoin == ljoin . fmap ljoin.


与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…
OGeek|极客中国-欢迎来到极客的世界,一个免费开放的程序员编程交流平台!开放,进步,分享!让技术改变生活,让极客改变未来! Welcome to OGeek Q&A Community for programmer and developer-Open, Learning and Share
Click Here to Ask a Question

...