我的风格可能会受到手机的限制，但我还是要这么做。

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

不能是函子。如果是的话，我们早就这么做了

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

月球将由绿色奶酪制成。

与此同时

newtype Dead x = Oops {oops :: Void}

是函子

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

但不能应用，否则我们会

oops (pure ()) :: Void

而绿色则是月亮奶酪做的(这种情况确实会发生，但只会在晚上晚些时候发生)。

(额外注意:Void，如Data。Void是一个空数据类型。如果你试图使用undefined来证明它是一个Monoid，我将使用unsafeCoerce来证明它不是。)

愉快,

newtype Boo x = Boo {boo :: Bool}

在很多方面都适用，例如，Dijkstra会说，

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

但它不能是单子。要知道为什么不可以，观察return必须不断地为Boo True或Boo False，因此

join . return == id

不可能坚持。

哦，对了，我差点忘了

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

是单子。自己卷。

飞机去赶…

我的风格可能会受到手机的限制，但我还是要这么做。

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

不能是函子。如果是的话，我们早就这么做了

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

月球将由绿色奶酪制成。

与此同时

newtype Dead x = Oops {oops :: Void}

是函子

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

但不能应用，否则我们会

oops (pure ()) :: Void

而绿色则是月亮奶酪做的(这种情况确实会发生，但只会在晚上晚些时候发生)。

(额外注意:Void，如Data。Void是一个空数据类型。如果你试图使用undefined来证明它是一个Monoid，我将使用unsafeCoerce来证明它不是。)

愉快,

newtype Boo x = Boo {boo :: Bool}

在很多方面都适用，例如，Dijkstra会说，

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

但它不能是单子。要知道为什么不可以，观察return必须不断地为Boo True或Boo False，因此

join . return == id

不可能坚持。

哦，对了，我差点忘了

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

是单子。自己卷。

飞机去赶…

对于不是函子的类型构造函数，一个很好的例子是Set:你不能实现fmap:: (A -> b) -> f A -> f b，因为如果没有额外的约束Ord b，你就不能构造f b。

我认为其他的答案漏掉了一些简单而常见的例子:

类型构造函数是函子而不是应用程序。一个简单的例子是一对:

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

但是没有办法在不对r施加额外限制的情况下定义它的application实例。特别是，没有办法为任意r定义pure:: a -> (r, a)。

一个类型构造函数，它是一个应用程序，但不是一个单子。一个著名的例子是ZipList。(它是一种新类型，包装列表并为它们提供不同的应用程序实例。)

Fmap的定义与通常的方式相同。但是pure和<*>被定义为

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

因此，pure通过重复给定值来创建一个无限列表，而<*>压缩带有值列表的函数列表-将第i个函数应用到第i个元素。([]上的标准<*>产生了将第i个函数应用到第j个元素的所有可能组合。)但是没有合理的方法来定义一个单子(见这篇文章)。

---

箭头如何适合函数/应用程序/单子层次结构? 参见Sam Lindley, Philip Wadler, Jeremy Yallop的《习语are oblivious，箭头are meticulous，单子are promiscuous》。MSFP 2008。(他们称应用函子为习语。)文摘:

我们将重新审视计算的三个概念之间的联系:Moggi的单子、Hughes的箭头和McBride和Paterson的习语(也称为应用函子)。我们证明成语等价于满足类型同构的箭头A ~> B = 1 ~> (A -> B)，单子等价于满足类型同构的箭头A ~> B = A -> (1 ~> B)，并且成语嵌入到箭头中，箭头嵌入到单子中。

不是Functor的类型构造函数:

newtype T a = T (a -> Int)

你可以从中得到一个逆变函子，但不是一个(协变)函子。试着写fmap，你会失败。注意逆变函子版本颠倒了:

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

一个类型构造函数，它是一个函子，但不是Applicative:

我没有一个好的例子。有Const，但理想情况下，我想要一个具体的非monoid，我想不出任何。所有类型基本上都是数值、枚举、乘积、和或函数。你可以在下面看到猪工和我对数据是否存在分歧。Void是一个Monoid;

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

因为_|_在Haskell中是一个合法的值，实际上也是Data的唯一合法值。Void，这符合Monoid规则。我不确定unsafeCoerce与它有什么关系，因为一旦你使用任何不安全的函数，你的程序就不再保证不违反Haskell语义。

请参阅Haskell Wiki中关于底部(链接)或不安全函数(链接)的文章。

我想知道是否有可能使用更丰富的类型系统来创建这样的类型构造函数，比如Agda或Haskell，它们具有各种扩展。

一个类型构造函数，它是Applicative，而不是Monad:

newtype T a = T {multidimensional array of a}

你可以用它来做一个应用程序，比如:

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

但如果你把它做成单子，你就会得到一个不匹配的维度。我怀疑这样的例子在实践中很少见。

一个类型构造函数，它是一个Monad:

[]

箭头:

问箭头在这个层次结构中的位置就像问“红色”是什么形状。注意类型不匹配:

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

but,

Arrow :: * -> * -> *

我想提出一种更系统的方法来回答这个问题，并举例说明不使用任何特殊技巧，如“底部”值或无限数据类型或诸如此类的东西。

什么时候类型构造函数没有类型类实例?

一般来说，类型构造函数不能拥有某个类型类的实例有两个原因:

无法实现类型类中所需方法的类型签名。 可以实现类型签名，但不能满足所需的规则。

第一类例子比第二类例子简单，因为对于第一类例子，我们只需要检查一个函数是否可以用给定的类型签名实现，而对于第二类例子，我们需要证明没有一个实现可能满足这些法则。

具体的例子

类型构造函数不能有函子实例，因为该类型不能被实现: 数据F z a = F (a -> z)

这是一个逆变子，而不是函子，对于类型参数a，因为a在逆变的位置。不可能实现具有类型签名(a -> b) -> F z a -> F z b的函数。

即使可以实现fmap的类型签名，类型构造函数也不是合法的函子: 数据Q = Q(a -> Int, a) fmap::(a -> b) -> Q a -> Q b fmap f (Q(g, x)) = Q(\_ -> g x, f x)——这违反了函子定律!

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 id ≠ id, 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.

事实上，F只是一个泛函子，它既不是泛函子也不是逆函子。

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)

类型构造函数P是一个函子，因为它只在协变位置使用a。

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

<*>类型签名的唯一可能实现是一个总是返回Nothing的函数:

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

但这种实现不满足应用函子的恒等定律。

一个是application而不是Monad的函子，因为bind的类型签名不能实现。

我不知道有这样的例子!

一个是application而不是Monad的函子，因为即使可以实现bind的类型签名，也不能满足法律。

这个例子已经引起了相当多的讨论，所以可以肯定地说，证明这个例子是正确的并不容易。但有几个人用不同的方法独立地验证了这一点。参见Is ' data PoE a = Empty | Pair a a ' a monad?供进一步讨论。

 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

证明不存在合法的Monad实例有点麻烦。非单一行为的原因是，当函数f:: a -> B B对于不同的a值可以返回Nothing或Just时，没有自然的方法来实现bind。

考虑Maybe (a, a, a)可能会更清楚，它也不是一个单子，并尝试为此实现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.

在由??显然，我们不能以任何合理和对称的方式从类型a的六个不同值中产生Just (z1, z2, z3)。我们当然可以从这六个值中选择任意的子集，例如，总是选择第一个非空的Maybe，但这将不满足单子的定律。“返回无”也不符合法律。

一个树状的数据结构，尽管它具有绑定的结合性，但它不是一个单子——但不符合同一性法则。

通常的树状单子(或“具有函数形分支的树”)定义为

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

这是一个在函子f上的自由单子。数据的形状是一个树，其中每个分支点都是一个子树的“函子”。标准二叉树的类型为f a = (a, a)。

如果我们修改这个数据结构，把叶子也做成函子f的形状，我们就得到了我所说的“半单子”——它有满足自然性和结合律的绑定，但它的纯方法没有满足一个恒等律。"半单胞体是内函子范畴内的半群，有什么问题吗"这是类型类Bind。

为了简单起见，我定义了join方法而不是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)

树枝嫁接是标准的，但叶子嫁接是不标准的，会产生树枝。这对结合律来说不是问题，但违反了一个恒等定律。

多项式类型什么时候有单实例?

函数Maybe (a, a)和Maybe (a, a, a)都不能被赋予一个合法的Monad实例，尽管它们显然是适用的。

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.

多项式单子的结构

一般来说，这里有一些由多项式类型产生合法单子的结构。在所有这些结构中，M是一个单子:

type M a = c (w, a)，其中w是任意一个单类 type M a = M (c (w, a))，其中M是任意单子，w是任意单子 type M a = (m1 a, m2 a)，其中m1和m2是任意单子 type M a = a (M a)，其中M是任意单子

第一个结构是WriterT w (Either c)，第二个结构是WriterT w (Either c m)。第三个结构是单元体的组件积:纯@M被定义为纯@m1和纯@m2的组件积，连接@M通过省略跨产品数据来定义(例如，m1 (m1 a, m2 a)通过省略元组的第二部分映射到m1 (m1 a)):

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

第四个结构被定义为

 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

我已经检查了所有四种结构产生合法的单子。

我猜想对于多项式单子没有其他的结构了。例如，函子Maybe (Either (a, a) (a, a, a))不是通过任何这些结构获得的，因此不是单元的。然而，Either (a,a) (a,a,a)是单体的，因为它同构于三个单体的乘积a,a，和Maybe a。同样，Either (a,a) (a,a,a)是单体的，因为它同构于a和Either a (a,a,a)的乘积。

上面所示的四个结构将允许我们得到任意数量的a的任意数量的乘积的任意数量的和，例如Either (Either (a, a) (a, a, a, a)) (a, a, a, a))等等。所有这样的类型构造函数都有(至少一个)Monad实例。

当然，这种单子的用例还有待观察。另一个问题是通过结构1-4派生的Monad实例通常不是唯一的。例如，类型构造函数类型F a = a (a, a)可以以两种方式给定一个Monad实例:通过构造4使用Monad (a, a)，以及通过构造3使用类型同构Either a (a, a) = (a, Maybe a)。再次强调，为这些实现找到用例不是立即明显的。

一个问题仍然存在——给定一个任意的多项式数据类型，如何识别它是否有一个Monad实例。我不知道如何证明多项式单子没有其他结构。我认为目前还没有任何理论可以回答这个问题。