Monad和Functor在Haskell中的Monad和Functor类型类的定律。

huangapple go评论56阅读模式
英文:

Monad and Functor law for Monad and Functor type class in Haskell

问题

I am a somewhat experienced functional programmer, but I have always been confused by the statement “A monad is just a monoid in the category of endofunctors” and the actual implementation of monads/functors in Haskell or other functional languages.

According to the Haskell Wiki,
https://wiki.haskell.org/Functor

class Functor f where
    fmap :: (a -> b) -> f a -> f b
    (<$) :: a -> f b -> f a

Functor Laws

Functors must preserve identity morphisms

fmap id = id

Functors preserve composition of morphisms

fmap (f . g)  ==  fmap f . fmap g

I understand this well, so no further explanation needed; however, when we use the monad operator that is >>=, now we have Monad implementation and Monad laws

https://wiki.haskell.org/Monad_laws

Here, I’m not questioning each implementation and rule. What I’m wondering is if we say “every Monad is an endofunctor because a monad is just a monoid in the category of endofunctors,” I expect a monad instance to satisfy the functor law, but in reality, it does not.

Or, although a monad is an endofunctor, the instance has 2 morphisms which are >>= and fmap. Do these two morphisms have independent laws?

I understand that the functor laws come from category theory and that a monad satisfies Monoid laws. But again, if a monad is an endofunctor, I don’t understand why it does not satisfy functor laws.

For instance,

main :: IO ()
main = do
  print $ [1, 2, 3] >>= \a -> [a]  // [2, 4, 6]

This code does not work if I change

  print $ [1, 2, 3] >>= id   // error "functor law" is not satisfied
英文:

I am a somewhat experienced functional programmer, but I have always been confused by the statement “A monad is just a monoid in the category of endofunctors” and the actual implementation of monads/functors in Haskell or other functional languages.

According to the Haskell Wiki,
https://wiki.haskell.org/Functor

class Functor f where
    fmap :: (a -&gt; b) -&gt; f a -&gt; f b
    (&lt;$) :: a -&gt; f b -&gt; f a

Functor Laws

Functors must preserve identity morphisms

fmap id = id

Functors preserve composition of morphisms

fmap (f . g)  ==  fmap f . fmap g

I understand this well, so no further explanation needed; however, when we uses the monad operator that is &gt;&gt;=, now we have Monad implementation and Monad laws

https://wiki.haskell.org/Monad_laws

Here, I’m not questioning each implementation and rule. What I’m wondering is if we say “every Monad is an endofunctor because a monad is just a monoid in the category of endofunctors”, I expect a monad instance to satisfy the functor law, but in reality, it does not.

Or, although a monad is an endofunctor, the instance has 2 morphisms which are &gt;&gt;= and fmap. Do these two morphisms have independent laws?

I understand that the functor laws come from category theory and that a monad satisfies Monoid laws. But again, if a monad is an endofunctor, I don’t understand why it does not satisfy functor laws.

For intance,

main :: IO ()
main = do
  print $ [1, 2, 3] &gt;&gt;= \a -&gt; [a]  // [2, 4, 6]

This code does not work if I change

  print $ [1, 2, 3] &gt;&gt;= id   // error &quot;functor law&quot; is not satisfied

答案1

得分: 9

以下是您要翻译的内容:

首先,关于monad有两个等价的定义。第一个直接对应于“endofunctors的monoid”:

class Functor m => Monad m where
  return :: a -> m a
  join :: m (m a) -> m a

在这里,我们明确假设m是一个endofunctor。Endofunctors的“tensor product”由它们的组合给出。因此,join是从m的“square”到m的箭头;它定义了我们的monoid中的“乘法”。return是从恒等endofunctor到m的箭头;它定义了monoidal unit。有关joinreturn的三个monoidal法则分别对应于左/右单位和结合性。

在Haskell中使用的Monad定义使用bind >>=而不是join。使用bind定义的monad自动成为endofunctor,其中fmap定义如下:

liftM :: Monad m => (a -> b) -> m a -> m b
liftM f ma = ma >>= return . f

第一个定义中的(相对简单的)monoidal法则翻译成以下法则:

return a >>= k = k a
ma >>= return = ma
ma >>= (\x -> k x >>= h) = (ma >>= k) >>= h

liftM的Functor法则可以从这些法则中推导出。例如,您可以使用以下步骤导出组合法则:

(liftM f . liftM g) ma 
= liftM f (ma >>= (return . g))
= (ma >>= (return . g)) >>= return . f
= ma >>= (\x -> ((return (g x)) >>= return . f))
= ma >>= (\x -> return (f (g x)))
= liftM (f . g) ma

希望这有所帮助!

英文:

To begin with, there are two equivalent definitions of a monad. The first corresponds directly to the "monoid of endofunctors":
<pre>class Functor m => Monad m where
return :: a -> m a
join :: m (m a) -> m a</pre>
Here, we explicitly assume that m is an endofunctor. The monoidal "tensor product" of endofunctors is given by their composition. So join is an arrow from the "square" of m to m; it defines "multiplication" in our monoid. return is an arrow from the identity endofunctor to m; it defines monoidal unit. There are three monoidal laws in terms of join and return corresponding to the left/right unit and associativity.

The Monad definition used in Haskell uses bind &gt;&gt;= instead of join. A monad defined using bind is automatically an endofunctor, with fmap defined as:
<pre>liftM :: Monad m => (a -> b) -> m a -> m b
liftM f ma = ma >>= return . f</pre>
The (relatively simple) monoidal laws from the first definition translate into the following laws:
<pre>
return a >>= k = k a
ma >>= return = ma
ma >>= (\x -> k x >>= h) = (ma >>= k) >>= h
</pre>
Functor laws for liftM follow from these laws. For instance, you can derive the composition law using these steps:
<pre>
(liftM f . liftM g) ma
= liftM f (ma >>= (return . g))
= (ma >>= (return . g)) >>= return . f
= ma >>= (\x -> ((return (g x)) >>= return . f))
= ma >>= (\x -> return (f (g x)))
= liftM (f . g) ma
</pre>

答案2

得分: 8

对于理论目的,通常最好忘记 &gt;&gt;=,我们不需要它。这些类型类的数学风格定义如下:

class Functor f where
  fmap :: (a -> b) -> f a -> f b
class Functor f => Applicative f where -- 也称为 Monoidal
  pure :: a -> f a
  liftA2 :: (a -> b -> c) -> f a -> f b -> f c  -- †
class Applicative m => Monad m where
  join :: m (m a) -> m a

(然后你可以继续定义 x&gt;&gt;=f = join (fmap f x),但这只是为了方便。)

从这个定义可以清楚地看出,讨论 [1, 2, 3] &gt;&gt;= id 对于确定单子是否是函子的问题是不相关的。单子是否是函子的含义就在类头中:MonadFunctor 的子类。因此,任何单子也都具有 fmap 可用,而这个 fmap 仍然需要满足函子法则,不管你现在是否也有那些更高级的方法可用。

是否 liftA2 还是 &lt;*&gt; 更数学化存在争议。原则上,我们应该讨论具有签名 (a⊗b -> c) -> f a⊗f b -> f c 的函数,但严格来说,这只适用于_关联张量积_。Haskell 元组近似实现了这一点,但只在笨拙的 "((a,b),c) 等同于 (a,(b,c))" 陈述下才成立。&lt;*&gt; 的好处是柯里化的函数在内部隐藏了这种关联性,但要付出的代价是我们需要处理_指数对象_,这使一切变得更加复杂。无论如何,我总是觉得 liftA2&lt;*&gt; 更容易理解。

英文:

For theory purposes it's usually best to forget about &gt;&gt;=, we don't need it. The maths-style definition of these type classes looks thus:

class Functor f where
  fmap :: (a -&gt; b) -&gt; f a -&gt; f b
class Functor f =&gt; Applicative f where -- aka Monoidal
  pure :: a -&gt; f a
  liftA2 :: (a -&gt; b -&gt; c) -&gt; f a -&gt; f b -&gt; f c  -- †
class Applicative m =&gt; Monad m where
  join :: m (m a) -&gt; m a

(You could then go on to define x&gt;&gt;=f = join (fmap f x), but that's just a matter of convenience.)

From this it should be clear that any discussion of [1, 2, 3] &gt;&gt;= id is pretty irrelevant for the question whether monads are functors. What it means for a monad to be a functor is right there in the class heads: Monad is a subclass of Functor. So any monad also has fmap available, and this fmap is still what needs to fulfill the functor laws, regardless of the fact that you now also have those fancier methods available.

<hr>

†<sub>It's arguable whether liftA2 or &lt;*&gt; are more mathematical. In principle we should be talking about the function with the signature (a⊗b -&gt; c) -&gt; f a⊗f b -&gt; f c, but strictly speaking that only works with an associative tensor product. Haskell tuples approximate this, but only under awkward "((a,b),c) is isomorphic to (a,(b,c))" caveats. The nice thing about &lt;*&gt; is that curried functions have this associativity hidden under the hood, but the price to pay is that we need to deal with exponential objects and it all gets yet a bit more confusing. At any rate, I always found liftA2 to be easier to understand than &lt;*&gt;.</sub>

huangapple
  • 本文由 发表于 2023年5月30日 04:36:46
  • 转载请务必保留本文链接:https://go.coder-hub.com/76360208.html
匿名

发表评论

匿名网友

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen:

确定