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

问题描述 投票:196回答:5

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

所以,我请求示例:

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

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

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

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

haskell monads functor applicative
5个回答
93
投票

一个不是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语义。

有关底部(link)或不安全函数(link)的文章,请参阅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 :: * -> * -> *

82
投票

我的手机可能会让我的风格变得狭窄,但是现在这样。

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 TrueBoo False,因此

join . return == id

不可能举行。

哦,是的,我差点忘了

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

是Monad。滚动你自己。

飞机赶上......


67
投票

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

一个类型构造函数,它是一个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没有明智的方法(参见this post)。


箭头如何适应functor / applicative / monad层次结构?请参阅Sam Lindley,Philip Wadler,Jeremy Yallop撰写的Idioms are oblivious, arrows are meticulous, monads are promiscuous。 MSFP 2008.(他们称之为applicative functors成语。)摘要:

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


20
投票

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


7
投票

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

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

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

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

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

具体的例子

  • 一个类型构造函数,由于无法实现类型,因此无法使用仿函数实例: 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只是一个变形金刚,它既不是算子也不是反向函数。

  • 由于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而不是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实例有点麻烦。非monadic行为的原因是当一个函数bind可以为f :: a -> B b的不同值返回NothingJust时,没有自然的方法来实现a

或许更清楚的是考虑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.

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

  • 一种树状数据结构,即使它与bind具有关联性,也不是monad - 但是没有同一性。

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

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

这是一个免费的monad over the functor f。数据的形状是树,其中每个分支点是子树的“函子”。标准二叉树将使用type f a = (a, a)获得。

如果我们通过制作仿函数f形状的叶子来修改这个数据结构,我们得到我称之为“semimonad” - 它有bind满足自然性和相关性定律,但它的pure方法失败了一个身份法律。 “Semimonads是endofunctors类别中的半群,问题是什么?”这是类型类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

这些仿函数没有任何技巧 - 任何地方都没有Voidbottom,没有棘手的懒惰/严格,没有无限的结构,也没有类型类约束。 Applicative实例是完全标准的。函数returnbind可以为这些函子实现,但不符合monad的定律。换句话说,这些仿函数不是monad,因为缺少特定的结构(但不容易理解究竟缺少什么)。作为一个例子,仿函数的一个小变化可以使它成为一个monad:data Maybe a = Nothing | Just a是一个monad。另一个类似的仿函数data P12 a = Either a (a, a)也是一个monad。

Constructions for polynomial monads

一般来说,这里有一些结构可以用多项式类型产生合法的Monads。在所有这些结构中,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),其中m1m2是任何monad
  4. type M a = Either a (m a),其中m是任何monad

第一个建筑是WriterT w (Either c),第二个建筑是WriterT w (EitherT c m)。第三种结构是monads的成分产品:pure @M被定义为pure @m1pure @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

我已经检查过所有四个结构都产生了合法的monad。

我猜想多项式monad没有其他结构。例如,仿函数Maybe (Either (a, a) (a, a, a, a))不是通过任何这些结构获得的,因此不是monadic。然而,Either (a, a) (a, a, a)是monadic,因为它与三个monad aaMaybe a的产物同构。此外,Either (a,a) (a,a,a,a)是monadic,因为它与aEither a (a, a, a)的产品同构。

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

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

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

热门问题
推荐问题
最新问题