不久前,我学到了Monoidal
是表示Applicative
的另一种方式。在Typeclassopedia上有一个有趣的问题:
- (棘手的) 证明根据你从第一个练习中得出的实现 [使用
unit
和(**)
编写的pure
和(<*>)
以及另一种方法],通常的Applicative
法则和上述Monoidal
法则是等价的。
以下是这些类和规则:
-- 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.
使用其他组合子编写组合子并不是什么大问题:
unit = pure ()
f ** g = (,) <$> f <*> g = liftA2 (,) f g
pure x = const x <$> unit
f <*> g = uncurry ($) <$> (f ** g)
以下是我对为什么法律告诉我们相同的事情的理解:
u <*> pure y = pure ($ y) <*> u -- Interchange: Applicative law.
我们首先需要注意的是,
($ y) ≅ y
(更正式地说:(y -> a) -> a ≅ y
)。有了这个想法后,交换律简单地告诉我们(a, b) ≅ (b, a)
。pure id <*> v = v -- Identity: Applicative law.
我认为id
本身就是一个单元,因为它是类型forall a. a -> a
的唯一成员。因此,这个定律给出了左单位元:
unit ** v = v -- Left Identity: Monoidal law.
现在我们可以使用
(a, b) ≅ (b, a)
来写出右单位元:u ** unit = u -- Right Identity: Monoidal law.
组合定律:
u <*> (v <*> w) = pure (.) <*> u <*> v <*> w -- Composition: Applicative law.
我认为这个定律与Monoidal
的结合律是同一件事:
u ** (v ** w) ≅ (u ** v) ** w
也就是说,
(a, (b, c)) ≅ ((a, b), c)
。而Applicative
只是增加了一层应用。因此,我们已经覆盖了所有的
Monoidal
法则。我认为没有必要反过来做,因为我们将使用相同的同构关系。但是有人可能会注意到一些奇怪的东西——我们没有使用同态Applicative
法则:pure f <*> pure x = pure (f x)
我试图通过自然性自由定理理解同态,这里的 Monoidal
是指单子范畴:
fmap (g *** h) (u ** v) = fmap g u ** fmap h v
但是很奇怪,同态并不处理副作用,然而自然性却可以正常工作。
所以,我有三个问题:
- 我的推理正确吗?
- 同态在这张图片中的位置是什么?
- 我们如何从应用角度理解自然性自由定理?
($ y) ≅ y
",我认为这完全不正确。 - Will Ness\ t -> t id
;从右到左 -\ t -> ($ t)
。我错在哪里了? - Zhiltsoff Igory
和($ y)
是值?也许我没有完全理解你的意思。 - Will Ness$
类型运算符。我猜它很笨拙,但对于直觉来说似乎很合适。这是一个不好的表达方式吗?老实说,我所有关于这种证明的经验都只是像你所说的那样机械化的工作。如果你能给我一些例子,说明这种风格被正确地执行了,我会非常感激。 - Zhiltsoff Igor