为什么单调律和适用法告诉我们的是同一件事? [英] Why are Monoidal and Applicative laws telling us the same thing?

问题描述

不久前，我了解到Monoidal是表示Applicative的另一种方式.关于 Typeclassopedia :

I have learnt about Monoidal being an alternative way to represent Applicative not so long ago. There is an interesting question on Typeclassopedia:

1. (Tricky)证明从第一个练习[使用unit和(**)写下的pure和(<*>)以及相反的方法]，常规的Applicative律和上述法律是等效的.

1. (Tricky) Prove that given your implementations from the first exercise [pure and (<*>) written down using unit and (**) and the other way around], the usual Applicative laws and the Monoidal laws stated above are equivalent.

以下是这些类别和法律:

Here are these classes and laws:

-- A note from https://wiki.haskell.org/Typeclassopedia#Alternative_formulation:
-- In this and the following laws, ≅ refers to isomorphism rather than equality. 
-- In particular we consider (x,()) ≅ x ≅ ((),x) and ((x,y),z) ≅ (x,(y,z)).

-- Monoidal.
class Functor f => Monoidal f where
  unit :: f ()
  (**) :: f a -> f b -> f (a,b)

-- unit ** v ≅ v - Left Identity.
-- u ** unit ≅ u - Right Identity.
-- u ** (v ** w) ≅ (u ** v) ** w - Associativity.

-- Applicative. 
class Functor f => Applicative f where
  pure  :: a -> f a
  infixl 4 <*>, ...
  (<*>) :: f (a -> b) -> f a -> f b
  ...

-- pure id <*> v = v - Identity.
-- pure f <*> pure x = pure (f x) - Homomorphism.
-- u <*> pure y = pure ($ y) <*> u - Interchange.
-- u <*> (v <*> w) = pure (.) <*> u <*> v <*> w - Composition.

使用其他脚本写下组合器没什么大不了的:

Writing down combinators using others is no big deal:

unit   = pure ()
f ** g = (,) <$> f <*> g = liftA2 (,) f g

pure x  = const x <$> unit
f <*> g = uncurry ($) <$> (f ** g)

这是我对法律为什么告诉我们同一件事的理解:

Here is my understanding of why the laws are telling us the same thing:

u <*> pure y = pure ($ y) <*> u -- Interchange: Applicative law.

我们要注意的第一件事是($ y) ≅ y(更正式地是:(y -> a) -> a ≅ y).考虑到这一点，交换法简单地告诉我们(a, b) ≅ (b, a).

The first thing we shall notice is that ($ y) ≅ y (more formally: (y -> a) -> a ≅ y). Having that in mind, Interchange law simply tells us that (a, b) ≅ (b, a).

pure id <*> v = v -- Identity: Applicative law.

我认为id本身就是一个单元，因为它是forall a. a -> a类型的唯一居民.因此，该法则赋予我们左身份:

I reckon id to be something of a unit itself as it is the only inhabitant of type forall a. a -> a. Therefore, this law gives us the Left Identity:

unit ** v = v -- Left Identity: Monoidal law.

现在，我们可以使用该(a, b) ≅ (b, a)写下正确的身份信息:

Now we can use that (a, b) ≅ (b, a) to write the Right Identity down:

u ** unit = u -- Right Identity: Monoidal law.

《组成法》:

u <*> (v <*> w) = pure (.) <*> u <*> v <*> w -- Composition: Applicative law.

我认为这条定律与Monoidal的关联性相同:

I reckon this law to tell the same thing as Associativity for Monoidal:

u ** (v ** w) ≅ (u ** v) ** w

即(a, (b, c)) ≅ ((a, b), c). Applicative只是添加了一层应用程序.

That is, (a, (b, c)) ≅ ((a, b), c). Applicative just adds a layer of application.

因此，我们涵盖了所有Monoidal法律.我相信没有必要做其他事情，因为我们将使用相同的同构.但是可能有人注意到了一些奇怪的事情-我们没有使用同构Applicative法则:

So, we have covered all of the Monoidal laws. I believe there is no need to do it the other way around as we are going to use the same isomorphisms. But one could have noticed something odd - we did not use the Homomorphism Applicative law:

pure f <*> pure x = pure (f x)

我尝试根据Monoidal的自然自由定理理解同态:

I tried understanding Homomorphism in terms of the Naturality free theorem for Monoidal:

fmap (g *** h) (u ** v) = fmap g u ** fmap h v

但是，由于同态不能处理副作用，因此看起来很奇怪，但是自然性可以很好地解决这些问题.

But it seems odd as Homomorphism does not deal with side-effects, yet Naturality works with them just fine.

所以，我有3个问题:

1. 我的推理对吗?
2. 同构在这张图片中代表什么位置?
3. 如何用Applicative理解自然自由定理?

1. Is my reasoning right?
2. Where does Homomorphism stand in this picture?
3. How can we understand the Naturality free theorem in terms of Applicative?

推荐答案

我们有

-- Monoidal.
class Functor f => Monoidal f where
  unit :: f ()
  (**) :: f a -> f b -> f (a,b)

-- unit ** v ≅ v - Left Identity.
-- u ** unit ≅ u - Right Identity.
-- u ** (v ** w) ≅ (u ** v) ** w - Associativity.

-- Applicative,
class Functor f => Applicative f where
  pure  :: a -> f a
  infixl 4 <*>
  (<*>) :: f (a -> b) -> f a -> f b

-- pure id <*> v = v - Identity.
-- pure f <*> pure x = pure (f x) - Homomorphism.
-- u <*> pure y = pure ($ y) <*> u - Interchange.
-- u <*> (v <*> w) = pure (.) <*> u <*> v <*> w - Composition.

实施方式1.适用-> Monoidal

Implementation 1. Applicative --> Monoidal

unit     = pure ()
xs ** ys = pure (,) <*> xs <*> ys

实施2.单项式->适用

Implementation 2. Monoidal --> Applicative

pure x  = const x <$> unit
fs <*> xs = uncurry ($) <$> (fs ** xs)

现在根据适用法律和实施1证明单等律:

Now prove Monoidal Laws given Applicative Laws and Implementation 1:

左身份. unit ** v ≅ v

unit ** v = pure () ** v
          = pure (,) <*> pure () <*> v
          = pure (\x -> (,) () x) <*> v
          = pure (\x -> (() , x)) <*> v
          = pure (() ,) <*> v
          ≅ pure id <*> v
          = v

正确的身份. u ** unit ≅ u

u ** unit = u ** pure ()
          = pure (,) <*> u <*> pure ()
          = pure ($ ()) <*> (pure (,) <*> u)  -- u <*> pure y = pure ($ y) <*> u 
          -- u <*> (v <*> w) = pure (.) <*> u <*> v <*> w
          = pure (.) <*> pure ($ ()) <*> pure (,) <*> u
          = pure ((.) ($ ())) <*> pure (,) <*> u
          = pure ((.) ($ ()) (,)) <*> u
          = pure (\x -> (.) ($ ()) (,) x) <*> u
          = pure (\x -> ($ ()) ((,) x)) <*> u
          = pure (\x -> (,) x ()) <*> u
          = pure (\x -> (x , ())) <*> u
          = pure (, ()) <*> u
          ≅ pure id <*> u
          = u

关联性. u ** (v ** w) ≅ (u ** v) ** w

u ** (v ** w) = ......

您应该可以继续执行此操作.我希望我没有在这里犯任何错误，但是如果有的话，请改正它们.

You should be able to continue this. I hope I didn't make any mistakes here, but if I did, correct them.

这篇关于为什么单调律和适用法告诉我们的是同一件事?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！