haskell - 仿函数的这种特性比单子(monad)更强吗？

Question

在考虑如何推广单子(monad)时，我想到了函子F的以下属性:

inject :: (a -> F b) -> F(a -> b) 

-这对a和b来说都是自然的转变。

在没有更好的名字的情况下，如果存在上面显示的自然转换 inject，我将其称为函子F 可绑定(bind)。

主要问题是，此属性是否已知并具有名称，以及它与函子的其他众所周知的属性(例如，可应用的，单子(monad)函数的，尖的，可遍历的等)如何相关？

名称“可绑定(bind)”的动机来自以下考虑:假设M是单子(monad)，而F是“可绑定(bind)”函子。然后一个人具有以下自然态素:

fbind :: M a -> (a -> F(M b)) -> F(M b)

这类似于单子(monad)的“绑定(bind)”，

bind :: M a -> (a -> M b) -> M b

除了结果用函子F装饰。
fbind背后的想法是，广义的单子(monad)运算不仅可以产生单个结果M b，而且可以产生此类结果的“函数式”F。我想表达一种情况，一元运算产生多个“计算链”，而不是一个。每个“计算链”又是单子(monad)计算。

请注意，每个函子F都有态

eject :: F(a -> b) -> a -> F b

这与“注入(inject)”相反。但是，并非每个函子F都有“注入(inject)”。

具有“注入(inject)”的函子的示例: F t = (t,t,t)或 F t = c -> (t,t)，其中c是常量类型。函子 F t = c(常数函子)或 F t = (c,t)不可“绑定(bind)”(即没有“inject”)。延续函子 F t = (t -> r) -> r似乎也没有 inject。

“注入(inject)”的存在可以用不同的方式来表述。考虑“阅读器”函子 R t = c -> t，其中c是常量类型。 (此函子是可应用的和单调的，但这不重要。)然后，“inject”属性意味着 R (F t) -> F (R t)，换句话说，R与F交换。原来是 F (R t) -> R (F t)，对于R而言，对于任何仿函数F总是满意的。

到目前为止，我能够证明“注入(inject)”对任何单子(monad)M都意味着“结合”。

此外，我展示了每个具有“注入(inject)”功能的函子F还将具有以下附加属性:

指向

point :: t -> F t

如果F是“可绑定(bind)的”且适用，则F也是monad

如果F和G是“可绑定(bind)的”，则对函子F * G(但不是F + G)

如果F是“可绑定(bind)的”并且A是任何发音者，则(pro)功能G t = A t -> F t是可绑定(bind)的

身份函子是可绑定(bind)的。

公开问题:

是等同于某些其他知名属性的“可绑定(bind)”属性，还是通常不考虑的函子的新属性？

从“注入(inject)”的存在开始，函子“F”还有其他属性吗？

我们是否需要任何“注入(inject)”法则，这会有用吗？例如，我们可能要求R(F t)在一个或两个方向上与F(R t)同构。

Answer 1

为了稍微改善术语，我建议将这些函子称为“刚性”，而不是“可绑定(bind)”。下面将说明说“刚性”的动机。

定义

如果函子f具有inject方法，则将其称为，刚性。请注意，每个函子都有eject方法。

class (Functor f) => Rigid f where
  inject :: (a -> f b) -> f(a -> b)

  eject :: f(a -> b) -> a -> f b
  eject fab x = fmap (\ab -> ab x) fab

“不堕落”法则必须遵守:

eject . inject = id

物产

刚性函子总是指向:

instance (Rigid f) => Pointed f where
  point :: t -> f t
  point x = fmap (const x) (inject id)

如果刚性函子是可应用的，那么它将自动为单子(monad)函数:

instance (Rigid f, Applicative f) => Monad f where
  bind :: f a -> (a -> f b) -> f b
  bind fa afb = (inject afb) <*> fa

刚性的特性与单子(monad)性的特性不可比(既不弱也不强):如果函子是刚性的，则似乎并不能得出它是自动单子(monad)性的(尽管我不知道这种情况下的具体反例) )。如果函子是一元函数，就不能认为它是刚性的(有反例)。

非刚性单子(monad)函子的基本反例是 Maybe和 List。这些函子具有多个构造函数:此类函子不能是严格的。

为 inject实现 Maybe的问题在于， inject必须将 a -> Maybe b类型的函数转换为 Maybe(a -> b)，而 Maybe具有两个构造函数。类型 a -> Maybe b的函数可以为 a的不同值返回不同的构造函数。但是，我们应该构造一个 Maybe(a -> b)类型的值。如果给定的函数为 a生成 Nothing，则我们没有 b，因此我们无法生成总函数 a->b。因此，我们无法返回 Just(a->b)；只要给定函数生成 Nothing，即使对于 Nothing的一个值，我们也必须返回 a。但是我们不能检查 a -> Maybe b类型的给定函数是否为 Just(...)的所有值产生 a。因此，在所有情况下我们都必须返回 Nothing。这将不能满足非简并定律。

因此，如果 inject是“固定形状”的容器(只有一个构造函数)，我们可以实现 f t。因此，名称为“刚性”。

关于为什么刚性比一般性更具限制性的另一种解释是考虑自然定义的表达式

(inject id) :: f(f a -> a) 

其中 id :: f a -> f a。这表明我们可以将f-代数 f a -> a封装为 a内的任何类型 f。莫纳德有代数是不正确的。例如，各种“ future ”单子(monad)以及 IO单子(monad)都描述了 f a类型的计算，这些计算不允许我们提取 a类型的值-即使包装在 f a -> a-容器。这表明“ future ”单子(monad)和 f单子(monad)不是严格的。

严格比刚性强的属性是E. Kmett的软件包中的 distributivity。如果我们可以像任何其他函子 IO一样按 f交换顺序，则函子 p (f t) -> f (p t)是分布式的。刚性与仅能针对“阅读器”函子 p交换顺序相同。因此，所有分配函子都是刚性的。

所有分布式函子都必须是可表示的，这意味着它们等效于具有某些固定类型 r t = a -> t的“阅读器”函子 c -> t。但是，并非所有刚性函子都是可表示的。一个示例是由定义的函子 c

type g t = (t -> r) -> t

函子 g不等同于具有固定类型 g的 c -> t。

结构和示例

不能表示的刚性函子的其他示例(即不是“分布”)是 c形式的函子，其中 a t -> f t是任何矛盾函数，而 a是刚性函子。同样，笛卡尔乘积和两个刚性函子的组成也是刚性的。这样，我们可以在指数多项式函子类中产生许多刚性函子的例子。

我对 What is the general case of QuickCheck's promote function?的回答还列出了刚性函子的结构:

f

如果f = Identity和f都是严格的，则函子乘积g也是严格的

如果h t = (f t, g t)和f都是严格的，则合成g也是严格的

如果h t = f (g t)是刚性的，并且f是任何反函数，则函子g是刚性

刚性函子的另一特性是 h t = g t -> f t类型与 r ()等效，即 ()类型只有一个不同的值。该值是 r ()，其中 point ()在上面为任何刚性函子 point定义。 (我有一个证明，但这里我不会写，因为我找不到简单的单行证明。)结果是，刚性函子必须只有一个构造函数。这立即表明 r， Maybe， Either等不能是严格的。

与单子(monad)连接

如果 List是具有“外部合成”类型的monad转换器的monad，即 f，则 t m a = f (m a)是刚性函子。

“刚性单子(monad)”可能是刚性函子的子集，因为如果 f也是刚性单子(monad)而不是任意刚性函子，则构造4仅会产生刚性单子(monad)(但反函子 f仍然可以是任意的)。但是，我没有刚性函子的例子，该函子也不是单子(monad)。

刚性monad的最简单示例是 g，即“搜索monad”。 (此处 type r a = (a -> p) -> a是固定类型。)

为了证明带有“外部组成”转换器 p的monad f也具有 t m a = f (m a)方法，我们将选择了外部monad inject的转换器 t m a选作阅读器monad m。然后将具有正确类型签名的 m a = r -> a函数定义为

 inject = join @t . return @r . (fmap @m (fmap @f return @m))

选择适当的类型参数。

非简并性定律遵循 inject的单子(monad)自然性:将单子(monad)态态 t(将 m -> Identity类型的值代入阅读器)提升为单子(monad)态态 r。我省略了此证明的细节。

用例

最后，我发现了两个刚性函子的用例。

第一个用例是考虑使用刚性函子的原始动机:我们想一次返回几个单子(monad)结果。如果 t m a -> t Id a是monad，并且我们想要问题中所示的 m，则需要 fbind严格。然后我们可以实现 f为

fbind :: m a -> (a -> f (m b)) -> f (m b)
fbind ma afmb = fmap (bind ma) (inject afmb)

对于任何monad fbind，我们可以使用 fbind来执行返回单项结果(或者更一般地，刚性的单项结果)的单项操作。

第二个用例来自以下考虑。假设我们有一个 m程序，在内部使用了 p :: a函数。现在，我们注意到 f :: b -> c函数非常慢，并且我们想通过用单子(monad)“future”或“task”或用Kleisli箭头 f代替monad f来替换 f' :: b -> m c来重构程序。当然，我们希望程序 m也将变为monadic: p。我们的任务是将 p' :: m a重构为 p。

重构过程分为两个步骤:首先，我们重构程序 p'，以便函数 p明确是 f的参数。假设已经完成，所以现在我们有了 p其中

q :: (b -> c) -> a

其次，我们将 p = q f替换为 f。现在我们假设给出了 f'和 q。我们想构造新的程序类型 f'

q' :: (b -> m c) -> m a

这样 q'。问题是我们是否可以定义一个通用组合器，将 p' = q' f'重构为 q，

refactor :: ((b -> c) -> a) -> (b -> m c) -> m a

事实证明，只有在 q'是刚性函子的情况下，才能构造 refactor。在尝试实现 m时，我们发现了与尝试为 refactor实现 inject时基本相同的问题:我们给了 Maybe函数，该函数可以为不同的 f' :: b -> m c返回不同​​的单调效果 m c，但是我们需要构造 b，该 m a必须表示所有 b的单调效果相同。例如，如果 m是具有多个构造函数的monad，则此方法不起作用。

如果 m是严格的(并且我们不需要 m是monad)，则可以实现 refactor:

refactor bca bmc = fmap bca (inject bmc)

如果 m不严格，我们将无法重构任意程序。到目前为止，我们已经看到延续单子(monad)是刚性的，但是像“ future ”一样的单子(monad)和 IO单子(monad)不是刚性的。这再次表明，从某种意义上讲，刚性是比普通性更强的特性。