不是Functor/Functor/Applicative/Monad的好例子？

Question

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

所以,我请求示例:

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

我认为Monad到处都有很多例子,但Monad的一个很好的例子与之前的例子有一些关系可以完成图片.

我寻找彼此相似的示例,区别仅在于属于特定类型类的重要方面.

如果有人能够设法在这个层次结构的某个地方隐藏一个Arrow的例子(它是在Applicative和Monad之间吗？),那也会很棒!

Answer 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

一个类型构造函数,它是一个函子,但不适用于:

我没有一个很好的例子.有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}

您可以使用以下内容制作应用程序:

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}

不能是一个Functor.如果是,我们就有

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.滚动你自己.

飞机赶上......

Answer 3

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

一个类型构造函数,它是一个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 -th函数应用于第i个元素.(标准<*>on []产生了将第i个函数应用于第j个元素的所有可能组合.)但是没有明智的方法来定义monad(参见这篇文章).

箭头如何适应functor/applicative/monad层次结构？ 看到成语是不经意的,箭头是一丝不苟的,单身是由Sam Lindley,Philip Wadler,Jeremy Yallop混淆的.MSFP 2008.(他们称之为applicative functors 成语.)摘要:

我们重新审视了三个计算概念之间的联系:Moggi的monads,Hughes的箭头和McBride和Paterson的习语(也称为applicative functors).我们证明成语相当于满足类型同构A~> B = 1~>(A - > B)的箭头,并且monad相当于满足类型同构的箭头A~> B = A - >(1~ > B).此外,成语嵌入箭头和箭头嵌入monad.

Answer 4

对于不是仿函数的类型构造函数,一个很好的例子是Set:你无法实现fmap :: (a -> b) -> f a -> f b,因为没有额外的约束Ord b你就无法构造f b.

Answer 5

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

类型构造函数何时无法具有类型类实例？

通常,有两个原因导致类型构造函数无法拥有某个类型类的实例:

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

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

具体的例子

• 一个类型构造函数,由于无法实现类型,因此无法使用仿函数实例:

a

这是一个反向函数,而不是仿函数,因为它a在逆变位置使用类型参数.实现具有类型签名的功能是不可能的(a -> b) -> F z a -> F z b.

• 即使fmap可以实现类型签名,也不是合法仿函数的类型构造函数:

fmap

这个例子的奇怪之处在于我们可以实现F正确的类型,即使它a不可能是一个仿函数,因为它fmap在逆变位置使用.因此,fmap id上面显示的这种实现具有误导性 - 即使它具有正确的类型签名(我相信这是该类型签名的唯一可能实现),但是不满足仿函数法则(这需要一些简单的计算来检查).

事实上,id它只是一个变形金刚,它既不是算子也不是反向函数.

• 由于类型签名let (Q(f,_)) = fmap id (Q(read,"123")) in f "456"无法实现而不适用的合法仿函数:使用Writer monad 123并删除let (Q(f,_)) = id (Q(read,"123")) in f "456"应该是monoid 的约束.它是那么不可能构造类型的值456出来的F.

• 一个不适用的仿函数,因为类型签名pure无法实现:(a, w).

• 即使可以实现类型类方法,也不是合法应用程序的仿函数:

w

类型构造函数(a, w)是一个仿函数,因为它a仅在协变位置使用.

data F z a = F (a -> z)

类型签名的唯一可能实现<*>是始终返回的函数data F a = Either (Int -> a) (String -> a):

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!

但是这种实现不满足应用函子的身份定律.

• 一个函数,P但不是a因为类型签名<*>无法实现.

我不知道这样的例子!

• 算符是Nothing,但不是Applicative因为法律不能被满足,即使类型签名Monad可以实现.

这个例子产生了相当多的讨论,因此可以肯定地说,证明这个例子是正确的并不容易.但有几个人通过不同的方法独立验证了这一点.请参阅`数据PoE a =空| 对aa`一个monad？进一步讨论.

data P a = P ((a -> Int) -> Maybe a)

证明没有合法的bind实例有点麻烦.非monadic行为的原因是Applicative当函数Monad可以返回时bind或者Monad对于不同的值时没有自然的实现方式bind.

或许可以更清楚地考虑f :: a -> B b,这也不是一个单子,并试图Nothing为此实施.人们会发现没有直观合理的实施方式Just.

instance Functor P where
   fmap :: (a -> b) -> P a -> P b
   fmap fab (P pa) = P (\q -> fmap fab $ pa (q . fab))

在所指出的情况下a,似乎很清楚,我们不能Maybe (a, a, a)以任何合理和对称的方式从六种不同的类型中产生join.我们当然可以选择这六个值中的一些任意子集 - 例如,总是采用第一个非空join- 但这不符合monad的定律.返回???也不符合法律.

• 一种树状的数据结构,即使它具有相关性,Just (z1, z2, z3)但不是单子,但却没有同一性.

通常的树状单子(或"带有仿函数形状的树枝的树")被定义为

 (<*>) :: P (a -> b) -> P a -> P b
 (P pfab) <*> (P pa) = \_ -> Nothing  -- fails the laws!

这是一个关于仿函数的免费monad a.数据的形状是树,其中每个分支点是子树的"函数".将使用标准二叉树获得Maybe.

如果我们通过制作Nothing仿函数形状的叶子来修改这个数据结构,我们就得到了我称之为"semimonad"的东西 - 它bind满足了自然性和相关性定律,但它的f方法不符合一个身份定律."Semimonads是endofunctors类别中的半群,问题是什么？" 这是类型类type f a = (a, a).

为简单起见,我定义f方法而不是bind:

 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

分枝嫁接是标准的,但叶嫁接是非标准的,并产生一个pure.这不是关联法律的问题,而是打破了身份法之一.

多项式类型何时具有monad实例？

无论是仿函数的Bind和join可以给出一个合法的bind情况下,尽管他们显然Branch.

这些仿函数没有任何技巧 - 没有Maybe (a, a)或Maybe (a, a, a)任何地方,没有棘手的懒惰/严格,没有无限的结构,也没有类型类约束.该Monad实例完全是标准的.功能Applicative和Void可以为这些仿函数来实现,但不会满足单子法律.换句话说,这些仿函数不是monad,因为缺少特定的结构(但不容易理解究竟缺少什么).作为一个例子,仿函数的一个小变化可以使它成为一个monad:bottom是一个monad.另一个类似的仿函数Applicative也是monad.

多项式monad的构造

通常,这里有一些return从多项式类型中产生合法的结构.在所有这些结构中,bind是monad:

1. data Maybe a = Nothing | Just a哪里data P12 a = Either a (a, a)有幺半群
2. Monad哪里M是monad并且type M a = Either c (w, a)是任何monoid
3. w哪里type M a = m (Either c (w, a))和m任何单子
4. w哪个type M a = (m1 a, m2 a)是monad

第一个建筑是m1,第二个建筑是m2.第三结构是单子的成分之积:type M a = Either a (m a)被定义为的成分之积m和WriterT w (Either c),并WriterT w (EitherT c m)通过省略跨产品数据(例如定义pure @M映射到pure @m1通过省略元组的第二部分):

 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.

第四种结构定义为

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

我已经检查过所有四种结构都产生了合法的单子.

我猜想多项式monad没有其他结构.例如,仿函数pure @m2不是通过任何这些结构获得的,因此不是monadic.然而,join @M是一元,因为它是同构于三个单子的产品m1 (m1 a, m2 a),m1 (m1 a)和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实例.

当然,还有待观察,这些monad可能存在哪些用例.另一个问题是Either a (a, a, a)通过结构1-4导出的实例通常不是唯一的.例如,类型构造函数a可以通过Either (Either (a, a) (a, a, a, a)) (a, a, a, a, a))两种方式给出一个实例:使用monad构造4 Monad,使用类型同构构造3 Monad.同样,找到这些实现的用例并不是很明显.

问题仍然存在 - 给定一个任意多项式数据类型,如何识别它是否有type F a = Either a (a, a)实例.我不知道如何证明多项式monad没有其他结构.到目前为止,我认为没有任何理论可以回答这个问题.