223

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

因此，我请求以下示例：

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

我认为到处都有很多 Monad 的例子，但是一个很好的 Monad 例子与前面的例子有一些关系可以完成这幅画。

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

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

4

5 回答 5

104

不是 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是 a Monoid;

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

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

有关底部（链接）或不安全函数（链接）的文章，请参阅 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 :: * -> * -> *
于 2011-08-28T11:04:52.857 回答
91

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

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，因为 inData.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 Trueor Boo False，因此

join . return == id

不可能持有。

哦对了，差点忘了

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

是一个单子。自己滚。

飞机要赶...

于 2011-08-28T12:09:58.697 回答
78

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

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

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

但是如果Applicative不对r. 特别是，没有办法pure :: a -> (r, a)为任意定义r。

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

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

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

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

箭头如何适应函子/应用程序/单子层次结构？ 请参阅Sam Lindley、Philip Wadler、Jeremy Yallop 的成语是不经意的，箭头是细致的，单子是混杂的。MSFP 2008。（他们称应用函子成语。）摘要：

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

于 2012-08-27T06:32:47.723 回答
21

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

于 2011-08-29T06:59:11.220 回答
15

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

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

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

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

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

具体例子

  • 由于无法实现类型而不能具有仿函数实例的类型构造函数：

    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应该是 monoid 的约束。那么就不可能构造出一个类型为 的(a, w)值a。

  • 一个不适用的函子，<*>因为无法实现的类型签名： 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但不是，Monadbind因为无法实现的类型签名。

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

  • 一个函子，Applicative但不是 aMonad，因为即使bind可以实现 的类型签名，也无法满足法律。

这个例子引起了相当多的讨论，所以可以肯定地说，证明这个例子是正确的并不容易。但有几个人通过不同的方法独立验证了这一点。请参阅是否`数据 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事例有点麻烦。非单子行为的原因是没有自然的方式来实现bind函数何时f :: a -> B b可以返回Nothing或Just不同的a.

考虑一下可能更清楚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.

在 指出的情况下???，很明显我们不能Just (z1, z2, z3)以任何合理和对称的方式从六个不同的类型值中产生a。我们当然可以选择这六个值的任意子集——例如，总是取第一个非空值Maybe——但这不满足单子定律。回归Nothing也不会满足法律。

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

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

 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：data Maybe a = Nothing | Just a是一个 monad。另一个类似的函子data P12 a = Either a (a, a)也是一个单子。

多项式单子的构造

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

  1. type M a = Either c (w, a)w任何幺半群在哪里
  2. type M a = m (Either c (w, a))哪里m是任何单子并且w是任何幺半群
  3. type M a = (m1 a, m2 a)哪里m1有m2任何单子
  4. type M a = Either a (m a)m单子在哪里

第一个构造是WriterT w (Either c)，第二个构造是WriterT w (EitherT c m)。第三种构造是 monads 的组件式乘积：pure @M定义为 和 的组件式乘积，并pure @m1通过省略叉积数据定义（例如，通过省略元组的第二部分映射到）：pure @m2join @Mm1 (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)的乘积同构。此外，是一元的，因为它与 和 的乘积同构。aaMaybe aEither (a,a) (a,a,a,a)aEither a (a, a, a)

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

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

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

于 2018-04-07T04:16:50.350 回答