这个特殊的仿函数结构叫什么？

Question

假设F是一个具有附加定律的应用函子(使用Haskell语法):

1. pure (const ()) <*> m === pure ()
2. pure (\a b -> (a, b)) <*> m <*> n === pure (\a b -> (b, a)) <*> n <*> m
3. pure (\a b -> (a, b)) <*> m <*> m === pure (\a -> (a, a)) <*> m

如果省略(3.),所谓的结构是什么？

我在哪里可以找到有关这些法律/结构的更多信息？

对评论的评论

满足(2.)的函数通常被称为可交换的.

现在的问题是,(1.)是否暗示(2.)以及如何描述这些结构.我对满足(1-2.)但不满足(3.)的结构特别感兴趣

例子:

• 读者monad满足(1-3.)
• 交换幺半群上的作家monad只满足(2.)
• 下面F给出的monad 满足(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.)是独立的.

为了证明这一点,我们还需要两个例子:

• 下面G给出的单子满足(3.)但不满足(1-2.)
• 下面G'给出的monad 满足(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.

Answer 1

你的第一部法律是一项非常强烈的要求; 这意味着仿函数不具有独立于参数部分的独特"形状".这排除了包含额外值的任何仿函数(State,Writer,&C)以及任何使用仿函数和类型(Either,[],&C).所以这限制了我们使用固定大小的容器.

你的第二定律要求交换性,这意味着嵌套的顺序(即函子组成)并不重要.这可能实际上是由第一定律暗示的,因为我们已经知道仿函数不能包含除参数值之外的任何信息,并且您明确要求在此保留它.

你的第三定律要求算子也是幂等的,这意味着使用fmap在其内部嵌套某些东西就等同于它自己.这可能意味着如果仿函数也是一个monad,则join涉及某种"对角线".基本上,这意味着liftA2 (,)应该表现得像zip笛卡尔产品.

第二个和第三个一起暗示无论函子可能具有多少"基元",任何组合等同于以任何顺序组合每个基元中的至多一个.第一个暗示如果你抛弃参数信息,任何基元组合都与使用none完全相同.

总之,我认为你所拥有的是类同形函数Reader.也就是说,仿函数f a描述了a由其他类型索引的类型的值,例如自然数的子集(对于固定大小的容器)或任意类型(如同Reader).

不幸的是,我不确定如何令人信服地证明上述大部分内容.