haskell - 这种特殊的仿函数结构叫什么？

Question

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

pure (const ()) <*> m === pure ()

pure (\a b -> (a, b)) <*> m <*> n === pure (\a b -> (b, a)) <*> n <*> m

pure (\a b -> (a, b)) <*> m <*> m === pure (\a -> (a, a)) <*> m

如果我们省略(3.)，结构叫什么？

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

评论评论

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

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

例子:

读者单子(monad)满足 (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)

评论 C. A. 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 .

Answer 1

你的第一定律是一个非常强烈的要求；这意味着仿函数不能有独立于参数部分的可区分的“形状”。这排除了任何包含额外值(State、Writer 等)的仿函数以及任何使用求和类型(Either、[] 等)的仿函数。所以这将我们限制在固定大小的容器之类的东西上。

您的第二定律需要交换性，这意味着嵌套顺序(即仿函数组合)无关紧要。这实际上可能由第一定律暗示，因为我们已经知道仿函数不能包含除参数值之外的任何信息，并且您明确要求在此处保留该信息。

您的第三定律要求仿函数也是幂等的，这意味着使用 fmap 将某些内容嵌套在自身内部等同于自身。这可能意味着如果仿函数也是一个单子(monad)，join涉及某种“取对角线”。基本上，这意味着 liftA2 (,)应该表现得像 zip ，而不是笛卡尔积。

第二个和第三个一起意味着无论仿函数可能有多少“原语”，任何组合都相当于以任何顺序组合每个原语中的最多一个。第一个意味着如果你丢弃参数信息，任何原语组合都与完全不使用相同。

总之，我认为您拥有的是the class of functors isomorphic to Reader .也就是说，f a 的仿函数描述 a 类型的值由其他类型索引，例如自然数的子集(对于固定大小的容器)或任意类型(如 Reader )。

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