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

Posted 2023-02-23

【中文标题】Not a Functor/Functor/Applicative/Monad 的好例子？

【英文标题】：Good examples of Not a Functor/Functor/Applicative/Monad?

【发布时间】：2011-11-05 10:23:51

【问题描述】：

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

所以，我请求以下示例：

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

我认为到处都有很多 Monad 的例子，但是一个很好的 Monad 例子与前面的例子有一些关系。

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

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

【问题讨论】：

是否可以为存在 no 的类型构造函数 (* -> *) 制作适合的fmap？

欧文，我认为a -> String 不是函子。

@Rotsor @Owen a -> String 是一个数学函子，但不是 Haskell Functor，要清楚。

@J.亚伯拉罕森，那么它在什么意义上是数学函子？你说的是反箭头的类别吗？

人们不知道，逆变函子的 fmap 类型为 (a -> b) -> f b -> f a

【参考方案1】：

不是 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

你可以用它做一个 Applicative，比如：

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

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

类型构造函数，它是 Monad：

[]

关于箭头：

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

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

但是，

Arrow :: * -> * -> *

【讨论】：

好清单！我建议使用像Either a 这样更简单的东西作为最后一种情况的示例，因为它更容易理解。

如果您仍在寻找 Applicative 但不是 Monad 的类型构造函数，一个非常常见的示例是 ZipList。

_|_ 存在于 * 中的每一种类型中，但Void 的重点是你必须向后弯腰才能构造一个，否则你已经破坏了它的价值。这就是为什么它不是 Enum、Monoid 等实例的原因。如果你已经有一个，我很高兴让你将它们混合在一起（给你一个 Semigroup）但 mempty，但我没有明确给出任何工具在void 中构造一个Void 类型的值。你必须给枪装上子弹，把它对准你的脚，然后自己扣动扳机。

学究式地，我认为您对 Cofunctor 的概念是错误的。函子的对偶是函子，因为您将 both 输入 和 输出翻转并最终得到相同的东西。您正在寻找的概念可能是“逆变函子”，它略有不同。

@DietrichEpp：我认为这种用法不正确（没有引用），如果他们同意我的观点，请提供asked math.SE。

【参考方案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。要了解为什么不这样做，请注意返回必须始终为 Boo True 或 Boo False，因此

join . return == id

不可能坚持。

哦，是的，我差点忘记了

newtype Thud x = The only :: ()

是一个 Monad。自己动手。

要赶飞机……

【讨论】：

虚空是空的！无论如何，从道德上讲。

Void 是一个有 0 个构造函数的类型，我假设。它不是幺半群，因为没有mempty。

未定义？真没礼貌！可悲的是，unsafeCoerce (unsafeCoerce () undefined) 不是 ()，所以在现实生活中，存在违反法律的观察。

在通常的语义中，它只容忍一种未定义，你是对的。当然，还有其他语义。 Void 不限于总片段中的亚类。它也不是区分失败模式的语义中的幺半群。当我有一个比基于电话的编辑更容易的时刻时，我会澄清我的示例仅适用于没有完全一种未定义的语义。

@Dietrich Epp IMO 应用定律是为 Haskell 指称语义的总值的 PER 编写的。见Fast and Loose Reasoning is Morally Correct。

【参考方案3】：

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

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

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

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

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

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

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

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

---

箭头如何适应函子/应用程序/单子层次结构？ 请参阅 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)。此外，成语嵌入箭头，箭头嵌入单子。

【讨论】：

所以((,) r) 是一个函子，不是一个应用程序；但这只是因为您通常不能一次为所有r 定义pure。因此，这是一种语言简洁的怪癖，试图用pure 和<*> 的一个定义来定义一个（无限的）应用函子集合；从这个意义上说，这个反例似乎没有任何数学深度，因为对于任何具体的r，((,) r) 可以 成为一个应用函子。问题：你能想到一个不能成为应用程序的CONCRETE functor吗？

看到***.com/questions/44125484/…这个问题的帖子。

【参考方案4】：

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

【讨论】：

这实际上是一个很好的例子，因为在数学上我们真的想把它变成一个函子。

@AlexandreC。我不同意这一点，这不是一个很好的例子。从数学上讲，这样的数据结构确实形成了函子。我们无法实现fmap 的事实只是语言/实现问题。此外，可以将Set 包装到延续 monad 中，这使得 monad 具有我们期望的所有属性，请参阅this question（尽管我不确定它是否可以有效地完成）。

@PetrPudlak，这是一个语言问题吗？ b 的相等性可能无法确定，在这种情况下，您无法定义 fmap！

@Turion 可判定和可定义是两件不同的事情。例如，可以正确定义 lambda 项（程序）上的相等性，即使不可能通过算法来决定它。无论如何，这不是这个例子的情况。这里的问题是我们不能使用Ord 约束来定义Functor 实例，但是使用Functor 的不同定义或更好的语言支持可能是可能的。实际上用 ConstraintKinds it is possible 来定义一个可以像这样参数化的类型类。

即使我们可以克服ord 约束，Set 不能包含重复条目的事实意味着fmap 可以祭坛上下文。这违反了结合律。

【参考方案5】：

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

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

一般来说，类型构造函数无法拥有某个类型类的实例有两个原因：

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

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

具体例子

不能有仿函数实例的类型构造函数，因为该类型无法实现：

data F z a = 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(\_ -> g x, f x)  -- this fails the functor laws!

这个例子的奇怪之处在于我们可以实现正确类型的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) 可能更清楚，它也不是单子，并为此尝试实现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 也不符合法律规定。

不是 monad 的树状数据结构

，尽管它具有 bind 的关联性 - 但不符合恒等律。

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

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

这是函子 f 上的免费 monad。数据的形状是一棵树，其中每个分支点都是子树的“函子”。标准二叉树将通过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。这对结合律来说不是问题，但违反了恒等律之一。

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

仿函数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。

多项式单子的构造

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

type M a = Either c (w, a) 其中w 是任何幺半群 type M a = m (Either c (w, a)) 其中m 是任何monad，w 是任何monoid type M a = (m1 a, m2 a) 其中m1 和m2 是任何单子 type M a = Either a (m a) 其中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 实例：构造4 使用单子(a, a)，构造3 使用类型同构Either a (a, a) = (a, Maybe a)。同样，找到这些实现的用例并不是很明显。

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

【讨论】：

我认为B 是一个单子。你能给这个绑定Pair x y >>= f = case (f x, f y) of (Pair x' _,Pair _ y') -> Pair x' y' ; _ -> Empty举个反例吗？

@Franky Associativity 在您选择f 时因此定义而失败，这样f x 是Empty，但f y 是Pair，下一步都是Pair .我手动检查了法律不适用于此实施或任何其他实施。但要做到这一点是一项相当大的工作。我希望有一种更简单的方法来解决这个问题！

@Turion 该论点不适用于Maybe，因为Maybe 不包含需要担心的a 的不同值。

@Turion 我用几页计算证明了这一点；关于“自然方式”的争论只是一种启发式的解释。 Monad 实例由满足法律的函数 return 和 bind 组成。 return 的两个实现和bind 的 25 个实现适合所需的类型。您可以通过直接计算表明没有一个实现满足法律。为了减少所需的工作量，我使用join 而不是bind 并首先使用身份法则。但这是一项相当大的工作。

@duplode 不，我认为不需要Traversable。 m (Either a (m a)) 使用 pure @m 转换为 m (Either (m a) (m a))。然后简单地Either (m a) (m a) -> m a，我们可以使用join @m。这就是我检查法律的实施。