Not a Functor/Functor/Applicative/Monad 的好例子？

不是 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，但我想不出。当您深入了解时，所有类型基本上都是数字、枚举、乘积、总和或函数。您可以在下面看到 pigworker 和我不同意 Data.Void 是否是 Monoid；

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

由于 _|_ 是 Haskell 中的合法值，并且实际上是 Data.Void 的唯一合法值，因此这符合 Monoid 规则。我不确定 unsafeCoerce 与它有什么关系，因为一旦您使用任何 unsafe 函数，您的程序就不再保证不会违反 Haskell 语义。

有关底部 (link) 或不安全函数 (link) 的文章，请参阅 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 :: * -> *

但，

Arrow :: * -> * -> *

---

我的风格可能会被我的手机束缚，但就这样吧。

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)

但它不能是 Monad。要了解为什么不这样做，请观察返回值必须始终为 Boo True 或 Boo False，因此

join . return == id

不可能持有。

哦对了，差点忘了

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

是一个单子。自己滚。

飞机要赶...

---

我相信其他答案错过了一些简单而常见的例子：

一个类型构造函数，它是 Functor 但不是 Applicative。一个简单的例子是一对：

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

但是，如果不对 r 施加额外限制，就无法定义它的 Applicative 实例。特别是，无法为任意 r 定义 pure :: a -> (r, a)。

一个类型构造函数，它是一个 Applicative，但不是 Monad。 一个众所周知的例子是 ZipList。 （它是一个包装列表并为它们提供不同 Applicative 实例的 newtype。）

fmap 以通常的方式定义。但是 pure 和 <*> 被定义为

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

所以 pure 通过重复给定的值创建一个无限列表，并且 <*> 用一个值列表压缩一个函数列表 - 将第 i 个函数应用于 i -th 元素。 （[] 上的标准 <*> 产生了将第 i 个函数应用于第 j 个元素的所有可能组合。）但是没有明智的方法来定义一个单子（见 this post）。

箭头如何适应函子/应用程序/monad 层次结构？参见 Sam Lindley、Philip Wadler、Jeremy Yallop 的Idioms are oblivious, arrows are meticulous, monads are promiscuous。 MSFP 2008。（他们称应用函子 idioms。）摘要：

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

---

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

---

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

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

通常，类型构造函数无法拥有某个类型类的实例有两个原因：

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

第一种的例子比第二种容易，因为第一种，我们只需要检查一个给定类型签名的函数是否可以实现，而第二种，我们需要证明没有实现可能会满足法律。

具体例子

由于无法实现类型而不能具有仿函数实例的类型构造函数：data F za = F (a -> z)

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

即使 fmap 的类型签名可以实现，但不是合法函子的类型构造函数： data Q a = Q(a -> Int, a) fmap :: (a -> b) -> Q a -> Q b fmap f (Q(g, x)) = Q(\_ -> gx, fx) - 这不符合函子定律！

这个例子的奇怪之处在于我们可以实现正确类型的 fmap，即使 F 不可能是函子，因为它在逆变位置使用 a。因此，上面显示的 fmap 的这种实现具有误导性——即使它具有正确的类型签名（我相信这是该类型签名的唯一可能实现），但函子定律并不满足。例如，fmap id ≠ id，因为 let (Q(f,_)) = fmap id (Q(read,"123")) in f "456" 是 123，而 let (Q(f,_)) = id (Q(read,"123")) in f "456" 是 456。

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

一个不适用的合法函子，因为 pure 的类型签名无法实现：采用 Writer monad (a, w) 并删除 w 应该是一个幺半群的约束。这样就不可能从 a 中构造一个类型为 (a, w) 的值。

由于无法实现 <*> 的类型签名而不适用的函子：data F a = Either (Int -> a) (String -> a)。

即使可以实现类型类方法也不能合法应用的函子：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!

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

一个 Applicative 但不是 Monad 的函子，因为无法实现 bind 的类型签名。

我不知道任何这样的例子！

一个 Applicative 但不是 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) 可能更清楚，它也不是一个 monad，并尝试为此实现 join。人们会发现没有直观合理的方式来实现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——但这不满足单子定律。返回 Nothing 也不会满足法律。

一种树状数据结构，它不是单子，即使它具有绑定的关联性 - 但不符合恒等律。

通常的树状单子（或“具有函子形分支的树”）定义为

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

这是函子 f 上的一个自由单子。数据的形状是一棵树，其中每个分支点都是子树的“函子”。标准二叉树将通过 type f a = (a, a) 获得。

如果我们修改这个数据结构，也将叶子做成仿函数 f 的形状，我们会得到我所说的“半单子”——它有 bind，它满足自然性和结合律，但它的 pure方法不符合身份定律之一。 “半单子是内函子范畴中的半群，有什么问题？”这是类型类 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)

枝接是标准的，而叶接是非标准的，产生Branch。这对结合律来说不是问题，但违反了恒等律之一。

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

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

这些函子没有任何技巧 - 任何地方都没有 Void 或 bottom，没有棘手的惰性/严格性，没有无限结构，也没有类型类约束。 Applicative 实例是完全标准的。函数 return 和 bind 可以为这些函子实现，但不满足单子定律。换句话说，这些函子不是 monad，因为缺少特定的结构（但很难理解到底缺少了什么）。例如，函子中的一个小改动可以使它变成一个 monad：data Maybe a = Nothing | Just a 是一个 monad。另一个类似的仿函数 data P12 a = Either a (a, a) 也是一个 monad。

多项式单子的构造

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

类型 M a = Either c (w, a) 其中 w 是任何幺半群类型 M a = m (Either c (w, a)) 其中 m 是任何单子并且 w 是任何幺半群类型 M a = (m1 a, m2 a ) 其中 m1 和 m2 是任何单子类型 M a = Either a (ma) 其中 m 是任何单子

第一个结构是WriterT w (Either c)，第二个结构是WriterT w (EitherT c m)。第三种构造是 monad 的组件式乘积：pure @M 定义为 pure @m1 和 pure @m2 的组件式乘积，join @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, a)) 不是通过任何这些结构获得的，因此不是一元的。然而，Either (a, a) (a, a, a) 是单子的，因为它与三个单子 a、a 和 Maybe a 的乘积同构。此外，Either (a,a) (a,a,a,a) 是一元的，因为它与 a 和 Either a (a, a, a) 的乘积同构。

上面显示的四种结构将允许我们获得任意数量的 a 的任意数量的乘积的任意总和，例如 Either (Either (a, a) (a, a, a, a)) (a, a, a, a, a)) 等等。所有此类类型构造函数都将具有（至少一个）Monad 实例。

当然，这些单子可能存在哪些用例还有待观察。另一个问题是通过构造 1-4 派生的 Monad 实例通常不是唯一的。例如，可以通过两种方式给类型构造函数 type F a = Either a (a, a) 一个 Monad 实例：使用 monad (a, a) 构造 4，以及使用类型同构 Either a (a, a) = (a, Maybe a) 构造 3。同样，找到这些实现的用例并不是很明显。

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

---