假设 F 是具有附加定律的应用函子（使用 Haskell 语法）：
pure (const ()) <*> m===pure ()pure (\a b -> (a, b)) <*> m <*> n===pure (\a b -> (b, a)) <*> n <*> mpure (\a b -> (a, b)) <*> m <*> m===pure (\a -> (a, a)) <*> m
如果我们省略（3.），结构叫什么？
我在哪里可以找到有关这些法律/结构的更多信息？
评论评论
满足 (2.) 的函子通常称为可交换函子。
现在的问题是，（1.）是否暗示（2.）以及如何描述这些结构。我对满足 (1-2.) 但不满足 (3.) 的结构特别感兴趣
例子：
- 读者单子满足 (1-3.)
- 可交换幺半群上的 writer monad 仅满足 (2.)
- 下面给出的 monad
F满足 (1-2.) 但不满足 (3.)
的定义F：
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RankNTypes #-}
import Control.Monad.State
newtype X i = X Integer deriving (Eq)
newtype F i a = F (State Integer a) deriving (Monad)
new :: F i (X i)
new = F $ modify (+1) >> gets X
evalF :: (forall i . F i a) -> a
evalF (F m) = evalState m 0
我们只导出类型X、、、、F和实例new。evalF
检查以下是否成立：
liftM (const ()) m===return ()liftM2 (\a b -> (a, b)) m n===liftM2 (\a b -> (b, a)) n m
另一方面，liftM2 (,) new new不能替换为liftM (\a -> (a,a)) new：
test = evalF (liftM (uncurry (==)) $ liftM2 (,) new new)
/= evalF (liftM (uncurry (==)) $ liftM (\a -> (a,a)) new)
评论 CA McCann 的回答
我有一个证明草图，证明 (1.) 暗示 (2.)
pure (,) <*> m <*> n
=
pure (const id) <*> pure () <*> (pure (,) <*> m <*> n)
=
pure (const id) <*> (pure (const ()) <*> n) <*> (pure (,) <*> m <*> n)
=
pure (.) <*> pure (const id) <*> pure (const ()) <*> n <*> (pure (,) <*> m <*> n)
=
pure const <*> n <*> (pure (,) <*> m <*> n)
= ... =
pure (\_ a b -> (a, b)) <*> n <*> m <*> n
= 见下文 =
pure (\b a _ -> (a, b)) <*> n <*> m <*> n
= ... =
pure (\b a -> (a, b)) <*> n <*> m
=
pure (flip (,)) <*> n <*> m
观察
对于缺失的部分，首先考虑
pure (\_ _ b -> b) <*> n <*> m <*> n
= ... =
pure (\_ b -> b) <*> n <*> n
= ... =
pure (\b -> b) <*> n
= ... =
pure (\b _ -> b) <*> n <*> n
= ... =
pure (\b _ _ -> b) <*> n <*> m <*> n
引理
我们使用以下引理：
pure f1 <*> m === pure g1 <*> m
pure f2 <*> m === pure g2 <*> m
暗示
pure (\x -> (f1 x, f2 x)) m === pure (\x -> (g1 x, g2 x)) m
我只能间接地证明这个引理。
缺失的部分
有了这个引理和第一个观察，我们可以证明
pure (\_ a b -> (a, b)) <*> n <*> m <*> n
=
pure (\b a _ -> (a, b)) <*> n <*> m <*> n
这是缺少的部分。
问题
这是否已经在某个地方得到证明（可能是广义的形式）？
评论
(1.) 暗示 (2.) 但否则 (1-3.) 是独立的。
为了证明这一点，我们还需要两个例子：
- 下面给出的 monad
G满足 (3.) 但不满足 (1-2.) - 下面给出的 monad
G'满足 (2-3.) 但不满足 (1.)
的定义G：
newtype G a = G (State Bool a) deriving (Monad)
putTrue :: G ()
putTrue = G $ put True
getBool :: G Bool
getBool = G get
evalG :: G a -> a
evalG (G m) = evalState m False
我们只导出类型G、putTrue、getBool、evalG和Monad实例。
的定义G'与 的定义类似，但G有以下区别：
我们定义和导出execG：
execG :: G' a -> Bool
execG (G m) = execState m False
我们不出口 getBool。