不是函子/函子/应用/单子的好例子？

Question

在向某人解释什么是类型类 X 时，我很难找到恰好是 X 的数据结构的好示例。

因此，我请求以下示例：

• 不是函子的类型构造函数。
• 类型构造函数是 Functor，但不是 Applicative。
• 类型构造函数是 Applicative，但不是 Monad。
• 类型构造函数是 Monad。

我认为到处都有很多 Monad 的例子，但是一个与前面的例子有一定关系的 Monad 的好例子可以完整地描述这一情况。

我寻找彼此相似的示例，仅在属于特定类型类的重要方面有所不同。

如果有人能够设法在这个层次结构中的某个地方（是在 Applicative 和 Monad 之间吗？）偷偷拿一个 Arrow 的例子，那也太好了！

Answer 1

不是函子的类型构造函数：

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 语义。

请参阅 Haskell Wiki，获取有关底部 (链接) 或不安全函数 (链接）。

我想知道是否可以使用更丰富的类型系统（例如具有各种扩展的 Agda 或 Haskell）创建这样的类型构造函数。

一个类型构造函数，它是一个 Applicative，但不是一个 Monad：

newtype T a = T {multidimensional array of a}

你可以用它来创建一个 Applicative，类似于：

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

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

作为 Monad 的类型构造函数：

[]

关于箭头：

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

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

但是，

Arrow :: * -> * -> *

Answer 2

我的风格可能会受到手机的限制，但就这样吧。

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。要了解原因，请观察 return 必须始终为 Boo True 或 Boo False，因此

join . return == id

不可能成立。

哦，是的，我差点忘了

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

这是一个 Monad。自己滚。

飞机去赶...

Answer 3

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

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

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

但无法定义其 适用的实例，不对r施加额外的限制。特别是，没有办法如何定义pure::a -> (r, a) 表示任意 r。

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

fmap 以通常的方式定义。但是 pure 和 <*> 的定义如下：

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

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

---

箭头如何适应函子/应用/单子层次结构？
请参阅习语是不经意的，箭头是细致的，单子是混杂的作者：萨姆·林德利、菲利普·瓦德勒、杰里米·雅洛普。 MSFP 2008。（他们称之为应用函子习语。）摘要：

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

Answer 4

对于不是函子的类型构造函数来说，Set 是一个很好的例子：您无法实现 fmap :: (a -> b) ->发-> f b，因为如果没有额外的约束 Ord b，您就无法构造 f b。

Answer 5

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

什么时候类型构造函数无法拥有类型类实例？

一般来说，类型构造函数无法获得特定类型类的实例有两个原因：

1. 无法从类型类实现所需方法的类型签名。
2. 可以实现类型签名，但无法满足所需的法律。

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

具体示例

• 无法拥有函子实例的类型构造函数，因为类型无法实现：

  数据 F za = F (a -> z)
  

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

• 类型构造函数不是合法函子，即使可以实现 fmap 的类型签名：

  data Q a = Q(a -> Int, a)
  fmap::(a -> b) ->问一-> Qb
  fmap f (Q(g, x)) = Q(\_ -> gx, fx) ——这违反了函子定律！
  

这个例子的奇怪之处在于我们可以实现正确类型的fmap，即使F不可能是函子，因为它在a中使用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 是一个函子，因为它使用 < code>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的类型签名可以满足法则，也无法满足规则予以实施。

这个例子引起了相当多的讨论，所以可以肯定地说，证明这个例子的正确性并不容易。但有几个人通过不同的方法独立验证了这一点。请参阅 `data PoE a = 空 |将 aa` 与 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 -> 时，没有自然的方式来实现 bind。对于 a 的不同值，B b 可以返回 Nothing 或 Just。

考虑 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.

在 ??? 所示的情况下，很明显我们不能以任何合理且对称的方式从 6 个不同的值中生成 Just (z1, z2, z3)输入a。我们当然可以选择这六个值的任意子集——例如，总是采用第一个非空的Maybe——但这不能满足单子定律。返回 Nothing 也不符合法律。

• 不是 monad 的树状数据结构，尽管它具有 bind 的关联性 - 但不符合恒等法则。

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

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

这是函子f上的自由单子。数据的形状是一棵树，其中每个分支点都是一个“功能齐全”的子树。标准二叉树将通过type fa = (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 >。这对于结合律来说不是问题，但违反了恒等律之一。

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

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

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

多项式单子的构造

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

1. type M a = Either c (w, a) 其中 w 是任何幺半群
2. type M a = m (Either c (w, a)) 其中 m 是任何 monad，w 是任何 monoid
3. type M a = ( m1 a, m2 a) 其中m1 和 m2 是任何 monad
4. type M a = Either a (ma) 其中 m 是任何 monad

第一个构造是WriterT w (Either c)，第二个构造是WriterT w (EitherT cm)。第三个构造是 monad 的组件式乘积：pure @M 被定义为 pure @m1 和 pure @m2 的组件式乘积code> ，并且 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 和也许是。另外，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 构造 4 (a, a)，并通过使用类型同构 Either a (a, a) = (a, Maybe a) 的构造 3。同样，找到这些实现的用例并不是立即显而易见的。

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