在向某人解释什么是类型类X时,我很难找到正好是X的数据结构的好例子 .
所以,我请求示例:
-
一个不是Functor的类型构造函数 .
-
一个类型构造函数,它是一个Functor,但不是Applicative .
-
一个类型构造函数,它是一个Applicative,但不是Monad .
-
一个Monad的类型构造函数 .
我认为Monad到处都有很多例子,但Monad的一个很好的例子与之前的例子有一些关系可以完成图片 .
我查找了彼此相似的示例,仅在属于特定类型类的重要方面有所不同 .
如果有人能够设法在这个层次结构的某个地方隐藏一个Arrow的例子(在Applicative和Monad之间吗?),那也会很棒!
5 回答
A type constructor which is not a Functor:
你可以用它来制作逆变函子,但不能用(协变)函子 . 尝试写
fmap
然后你就会失败 . 请注意,逆变仿函数版本是相反的:A type constructor which is a functor, but not Applicative:
我没有一个很好的例子 . 有
Const
,但最好是我想到的 . 当您开始使用时,所有类型基本上都是数字,枚举,产品,总和或函数 . 你可以看到下面的pigworker,我不同意Data.Void
是否Monoid
;由于
_|_
在Haskell中是合法值,并且实际上是Data.Void
的唯一合法值,因此符合Monoid规则 . 我不确定unsafeCoerce
与它有什么关系,因为你的程序不再保证在你使用任何unsafe
函数时不会违反Haskell语义 .有关底部(link)或不安全函数(link)的文章,请参阅Haskell Wiki .
我想知道是否可以使用更丰富的类型系统创建这样的类型构造函数,例如具有各种扩展的Agda或Haskell .
A type constructor which is an Applicative, but not a Monad:
您可以使用以下内容制作应用程序:
但是如果你把它变成monad,你就会得到尺寸不匹配 . 我怀疑像这样的例子在实践中很少见 .
A type constructor which is a Monad:
About Arrows:
询问箭头在这个层次结构上的位置就像问什么样的形状“红色” . 注意种类不匹配:
但,
我的风格可能会被我的手机弄得一团糟,但是现在这样 .
不能是一个Functor . 如果是,我们就有
月亮将由绿色奶酪制成 .
与此同时
是一个算符
但不能适用,或者我们有
和绿色将由月亮奶酪制成(实际上可以发生,但仅在晚上) .
(额外注意:
Void
,如Data.Void
是一个空数据类型 . 如果你试图使用undefined
来证明它's a Monoid, I' ll使用unsafeCoerce
来证明它不是 . )欢悦,
在很多方面是适用的,例如Dijkstra会有的,
但它不能是Monad . 要明白为什么不这样做,请注意返回必须经常
Boo True
或Boo False
,因此不可能举行 .
哦,是的,我差点忘了
是Monad . 滚动你自己 .
飞机赶上......
我相信其他答案错过了一些简单而常见的例子:
A type constructor which is a Functor but not an Applicative. 一个简单的例子是一对:
但是如何在不对
r
施加额外限制的情况下如何定义其Applicative
实例 . 特别是,没有办法如何为任意r
定义pure :: a -> (r, a)
.A type constructor which is an Applicative, but is not a Monad. 一个众所周知的例子是ZipList . (它是
newtype
包装列表并为它们提供不同的Applicative
实例 . )fmap
以通常的方式定义 . 但pure
和<*>
被定义为所以
pure
通过重复给定的值创建一个无限列表,并且<*>
用一个值列表压缩一个函数列表 - 将第i个函数应用于第i个元素 . ([]
上的标准<*>
产生了将第i个函数应用于第j个元素的所有可能组合 . )但是如何定义monad没有明智的方法(参见this post) .How arrows fit into the functor/applicative/monad hierarchy? 见Sam Lindley,Philip Wadler,Jeremy Yallop撰写的Idioms are oblivious, arrows are meticulous, monads are promiscuous . MSFP 2008.(他们称之为applicative functors成语 . )摘要:
对于不是仿函数的类型构造函数,一个很好的例子是
Set
:你不能实现fmap :: (a -> b) -> f a -> f b
,因为没有额外的约束Ord b
你不能构造f b
.我想提出一个更系统的方法来回答这个问题,并举例说明不使用任何特殊技巧,如“底部”值或无限数据类型或类似的东西 .
类型构造函数何时无法具有类型类实例?
通常,有两个原因导致类型构造函数无法拥有某个类型类的实例:
无法从类型类实现所需方法的类型签名 .
可以实现类型签名但不能满足所需的法律 .
第一类的例子比第二类的例子容易,因为对于第一类,我们只需要检查是否可以实现具有给定类型签名的函数,而对于第二类,我们需要证明没有实现可能会满足法律 .
具体例子
data F a = F (a -> Int)
这是一个反向函数,而不是仿函数,因为它在逆变位置使用类型参数
a
. 实现类型签名(a -> b) -> F a -> F 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
的这种实现具有误导性 - 即使它具有正确的类型签名(我相信这是该类型签名的唯一可能实现),但是不满足算子定律(这需要一些简单的计算来检查) .事实上,
F
只是一个变形金刚,它既不是算子也不是反向函数 .A lawful functor that is not applicative 因为
pure
的类型签名无法实现:取Writer monad(a, w)
并删除w
应该是monoid的约束 . 然后,不可能在a
中构造(a, w)
类型的值 .A functor that is not applicative 因为无法实现
<*>
的类型签名:data F a = Either (Int -> a) (String -> a)
.A functor that is not lawful applicative 即使可以实现类型类方法:
data P a = P ((a -> Int) -> Maybe a)
类型构造函数
P
是一个仿函数,因为它仅在协变位置使用a
.<*>
类型签名的唯一可能实现是始终返回Nothing
的函数:但是这种实现不满足应用函子的身份定律 .
bind
的类型签名无法实现 .我不知道这样的例子!
bind
的类型签名,也无法满足法律 .这个例子产生了相当多的讨论,所以可以肯定地说,证明这个例子是正确的并不容易 . 但有几个人通过不同的方法独立验证了这一点 . 有关其他讨论,请参见Is
data PoE a = Empty | Pair a a
a monad? .证明没有合法的
Monad
实例有点麻烦 . 非monadic行为的原因是当函数f :: a -> B b
可以为a
的不同值返回Nothing
或Just
时,没有自然的方法来实现bind
.或许更清楚的是考虑
Maybe (a, a, a)
,它也不是monad,并尝试实现join
. 人们会发现没有直观合理的方式来实施join
.在由
???
指示的情况下,似乎很清楚我们不能以六种不同的a
类型的值以任何合理和对称的方式产生Just (z1, z2, z3)
. 我们当然可以选择这六个值中的一些任意子集 - 例如,总是采用第一个非空Maybe
- 但这不符合monad的定律 . 返回Nothing
也不符合法律规定 .bind
具有关联性 - 但未通过身份法律 .通常的树状单子(或“带有仿函数形状的树枝的树”)被定义为
这是一个关于函子
f
的免费monad . 数据的形状是树,其中每个分支点是子树的"functor-ful" . 使用type f a = (a, a)
可以获得标准二叉树 .如果我们通过使函子
f
形状的叶子也修改这个数据结构,我们得到了我称之为"semimonad"的bind
它满足了自然性和相关性定律,但它的pure
方法失败了一个身份定律 . "Semimonads are semigroups in the category of endofunctors, what's the problem?"这是类型类Bind
.为简单起见,我定义
join
方法而不是bind
:分枝嫁接是标准的,但叶嫁接是非标准的并产生
Branch
. 这不是关联法律的问题,而是打破了身份法之一 .多项式类型何时具有monad实例?
这些仿函数
Maybe (a, a)
和Maybe (a, a, a)
都不能给出合法的Monad
实例,尽管它们显然是Applicative
.这些仿函数没有任何技巧 - 没有
Void
或bottom
任何地方,没有棘手的懒惰/严格,没有无限的结构,没有类型类约束 .Applicative
实例是完全标准的 . 函数return
和bind
可以为这些仿函数实现,但不符合monad的规律 . 换句话说,这些仿函数不是monad,因为缺少特定的结构(但不容易理解究竟缺少什么) . 作为一个例子,仿函数的一个小变化可以使它成为一个monad:data Maybe a = Nothing | Just a
是一个monad . 另一个类似的仿函数data P12 a = Either a (a, a)
也是一个monad .多项式monad的构造
一般来说,这里有一些结构可以产生多项式类型的合法
Monad
. 在所有这些结构中,M
是一个monad:type M a = Either c (w, a)
其中w
是任何幺半群type M a = m (Either c (w, a))
其中m
是任何monad,w
是任何monoidtype M a = (m1 a, m2 a)
其中m1
和m2
是任何monadtype M a = Either a (m a)
其中m
是任何monad第一个建筑是
WriterT w (Either c)
,第二个建筑是WriterT w (EitherT c m)
. 第三个构造是monads的组件产品:pure @M
被定义为pure @m1
和pure @m2
的组件产品,而join @M
是通过省略跨产品数据来定义的(例如,m1 (m1 a, m2 a)
通过省略第二部分来映射到m1 (m1 a)
元组):第四种结构定义为
我已经检查过所有四种结构都会产生合法的单子 .
我猜想多项式monad没有其他结构 . 例如,仿函数
Maybe (Either (a, a) (a, a, a, a))
不是通过任何这些结构获得的,因此不是monadic . 但是,Either (a, a) (a, a, a)
是monadic,因为它与三个monada
,a
和Maybe a
的乘积同构 . 此外,Either (a,a) (a,a,a,a)
是monadic,因为它与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,使用类型isomorphismEither a (a, a) = (a, Maybe a)
构造3 . 同样,找到这些实现的用例并不是很明显 .问题仍然存在 - 给定任意多项式数据类型,如何识别它是否具有
Monad
实例 . 我不知道如何证明多项式monad没有其他结构 . 到目前为止,我认为没有任何理论可以回答这个问题 .