仿函数的这个属性比单子强吗？

Question

在思考如何推广monad时,我想出了一个仿函数F的以下属性:

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

- 这应该是a和b中的自然变换.

如果没有更好的名称,如果存在上面显示的自然变换,我将函数F称为可绑定inject.

主要问题是,这个属性是否已经知道并且有一个名称,它是如何与仿函数的其他众所周知的属性相关的(例如,应用,monadic,尖头,可遍历等)

名称"可绑定"的动机来自以下考虑:假设M是monad而F是"可绑定"仿函数.然后有一个具有以下自然态射:

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

这类似于monadic"bind",

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

除了结果用仿函数F装饰.

背后的想法fbind是,广义的monadic操作不仅可以产生单个结果M b,而且可以产生这种结果的"函数"F.我想表达一个monadic操作产生几个"计算线"而不仅仅是一个的情况; 每个"计算链"再次成为一元计算.

注意,每个仿函数F都具有态射

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

这与"注入"相反.但并非每个仿函数F都有"注入".

具有"注入"的仿函数的示例:F t = (t,t,t) 或者F t = c -> (t,t)其中c是常量类型.F t = cFunctor(常量仿函数)或F t = (c,t)不是"可绑定"(即没有"注入").延续仿函数F t = (t -> r) -> r似乎也没有inject.

"注入"的存在可以以不同的方式表达.考虑"reader"仿函数R t = c -> t,其中c是常量类型.(这个仿函数是应用的和monadic,但这不是重点.)然后,"注入"属性意味着R (F t) -> F (R t)R与F通勤.注意,这与F可遍历的要求不同; 本来可以的F (R t) -> R (F t),对于任何一个函子F来说总是满足于R.

到目前为止,我能够证明"注入"意味着任何monad M.的"fbind".

另外,我展示了每个具有"注入"的仿函数F也将具有以下附加属性:

• 有针对性的

point :: t -> F t

• 如果F是"可绑定的"并且适用,则F也是monad

• 如果F和G是"可绑定的"那么对子函子F*G(但不是F + G)也是如此

• 如果F是"可绑定"而A是任何一个profunctor,则(pro)仿函数G t = A t -> F t是可绑定的

• 身份仿函数是可绑定的.

开放式问题:

• 是"可绑定"的属性相当于其他一些众所周知的属性,还是一个通常不被考虑的仿函数的新属性？

• 仿冒"F"的其他属性是否跟随"注入"的存在？

• 我们是否需要任何"注射"法律,这会有用吗？例如,我们可以要求R(F t)在一个或两个方向上与F(R t)同构.

Answer 1

为了稍微改进术语,我建议将这些仿函数称为"刚性"而不是"可绑定".说"僵硬"的动机将在下面解释.

如果仿函数具有如图所示的方法,则该仿函数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)

如果一个刚性的仿函数是适用的那么它是自动的monadic:

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

刚性的性质与monadic的性质不具有可比性(既不弱也不强):如果算子是刚性的,似乎并不是因为它是自动的monadic(虽然我不知道这个案例的具体反例) ).如果一个仿函数是monadic,那么它并不是因为它是刚性的(有反例).

不严格的monadic仿函数的基本反例是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在所有情况下我们都被迫返回.这不符合非简并法则.

因此,我们可以实现injectif f t是一个"固定形状"的容器(只有一个构造函数).因此名称"刚性".

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

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

哪里id :: f a -> f a.这表明我们可以f a -> a为任何类型都有一个f代数a,只要它包含在里面f.任何单子都有代数是不正确的; 例如,各种"未来"monad以及IOmonad描述的类型计算f a不允许我们提取类型的值a- f a -> a即使包装在f-container中,我们也不应该有类型的方法.这表明"未来"的monad和IOmonad并不是僵化的.

强度大于刚性的属性是E. Kmett的一个包装的分配.函子f是分配的,如果我们可以交换顺序在p (f t) -> f (p t)为任何函子p.刚性与仅能够与"读者"仿函数交换顺序相同r t = a -> t.所以,所有的分配仿函数都是僵化的.

所有分配仿函数都必须是可表示的,这意味着它们等同于c -> t具有某种固定类型的"reader"仿函数c.然而,并非所有刚性函子都是可表示的.一个例子是由g定义的仿函数

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

仿函数g不等同于c -> t固定类型c.

刚性函子中不表示的(即,不是"分配")的其它实例是以下形式的仿函数a t -> f t,其中a是任何 contrafunctor和f是刚性仿函数.此外,笛卡尔积和两个刚性仿函数的组合也是刚性的.通过这种方式,我们可以在指数多项式类函数中生成许多刚性函子的例子.

我的回答是什么是QuickCheck推广功能的一般情况？还列出了刚性仿函数的结构.

最后,我找到了两个用于刚性仿函数的用例.

第一个用例是考虑刚性仿函数的最初动机:我们希望一次返回几个monadic结果.如果f = Identity是monad并且我们希望f如问题所示,我们需要g僵化.然后我们就可以实现h t = (f t, g t)了

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

f对于任何monad,我们可以使用monadic操作返回多个monadic结果(或者更一般地说,一个monadic结果的刚性函数)g.

第二个用例是出于以下考虑.假设我们有一个h t = f (g t)内部使用函数的程序f.现在,我们注意到函数g非常慢,我们想通过替换h t = g t -> f tmonadic"future"或"task" 来重构程序,或者通常使用Kleisli箭头替换r ()某些monad ().当然,我们希望该计划r ()也将成为monadic : point (). 我们的任务是重构point成r.

重构分两步进行:首先,我们重构程序,Maybe以便函数Either明确地作为参数List.假设这个已经做了,所以现在我们已经f在那里

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

其次,我们替换t m a = f (m a)为f.我们现在假设f并且g给出了.我们想构建type r a = (a -> p) -> a该类型的新程序

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

这样p.现在的问题是,我们是否可以定义将重构一般组合子f成t m a = f (m a),

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

事实证明,inject只有在t m a是一个严格的函子才能构造.在试图实现m,我们基本上发现了同样的问题,当我们试图实现m a = r -> a的inject:我们正在给一个函数t,可以返回不同的一元效应m -> Identity的不同r,但我们需要构造t m a -> t Id a,它必须代表所有相同的单子效果m.例如,如果fbind是具有多个构造函数的monad ,则这不起作用.

如果f是僵硬的(我们不需要要求fbindmonad),我们可以实现fbind:

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

如果m不是僵化的,我们就不能重构任意程序.到目前为止,我们已经看到,延续单子是刚性的,但"未来"般的单子和p :: a单子不是刚性的.这再次表明,在某种意义上,刚性比一性更强.

Answer 2

我最近一直在做一些实验以更好地理解Distributive。令人高兴的是，我的结果似乎与你的严格函子密切相关，在某种程度上澄清了它们。

首先，这是刚性函子的一种可能表示。我冒昧地把你的名字改了一下，原因我很快就会明白：

flap :: Functor f => f (a -> b) -> a -> f b
flap u a = ($ a) <$> u 

class Functor g => Rigid g where
    fflip :: (a -> g b) -> g (a -> b)
    fflip f = (. f) <$> extractors

    extractors :: g (g a -> a)
    extractors = fflip id

-- "Left inverse"/non-degeneracy law: flap . fflip = id

instance Rigid ((->) r) where
    fflip = flip

关于我的措辞的一些评论：

• 我已将injectand的名称更改eject为fflipand flap，主要是因为在我看来，它flap看起来更像是注射，原因如下：

  sweep :: Functor f => f a -> b -> f (a, b)
  sweep u b = flap ((,) <$> u) b
  

• 我从protolude取了这个flap名字。这是一个对 的游戏，这是合适的，因为它是概括它的两种对称方式之一。（我们可以将函数拉出任意的，如，或将函子拉出函数，如。）flipFunctorflapRigidfflip

• 我第一次意识到的意义extractors，同时摆弄Distributive，但它没有发生，我认为这可能是有意义的不同类的一部分。extractors并且fflip是可相互定义的，例如，可以为搜索/选择 monad 编写这个相当简洁的实例：

  newtype Sel r a = Sel { runSel :: (a -> r) -> a }
      deriving (Functor, Applicative, Monad) via SelectT r Identity
  
  instance Rigid (Sel r) where
      -- Sel r (Sel r a -> a) ~ ((Sel r a -> a) -> r) -> Sel r a -> a
      extractors = Sel $ \k m -> m `runSel` \a -> k (const a)
  

每个分配函子都是刚性的：

fflipDistrib :: Distributive g => (a -> g b) -> g (a -> b)
fflipDistrib = distribute @_ @((->) _)
-- From this point on, I will pretend Rigid is a superclass of Distributive.
-- There would be some tough questions about interface ergonomics if we were
-- writing this into a library. We don't have to worry about that right now,
-- though.

从另一个方向，我们可以编写一个模仿distributeusing签名的函数Rigid：

infuse :: (Rigid g, Functor f) => f (g a) -> g (f a)
infuse u = (<$> u) <$> extractors

infuse，然而，不是distribute。正如您所注意到的，有些刚性函子不是分布式的，例如Sel。因此，我们必须得出结论infuse，在一般情况下，不遵循分配规律。

（旁白：在可以通过基数论证建立的情况下，这infuse不是合法distribute的Sel。如果infuse遵循分配律，我们将有infuse . infuse = id任何两个刚性函子。但是，类似infuse @((->) Bool) @(Sel r)导致结果类型的居民少于参数类型；因此，它不可能有左逆。）

星座中的一个地方

在这一点上，这将是相关的磨砺区分正是我们的图片Distributive从Rigid。鉴于您的严格定律是flap . fflip = id，直觉表明同构的另一半，fflip . flap = id，在 的情况下可能成立Distributive。检查该假设需要绕道而行Distributive。

Distributive(和Rigid)有另一种表示，其中distribute(或fflip) 通过函数函子进行分解。更具体地说，任何类型的函数值g a都可以转换为带有forall x. g x -> x提取器的 CPS 暂停：

-- The existential wrapper is needed to prevent undue specialisation by GHC.
-- With pen and paper, we can leave it implicit.
-- Note this isn't necessarily the best implementation available; see also
-- /sf/ask/3977871341/
data Ev g a where
    Ev :: ((g x -> x) -> a) -> Ev g a

-- Existential aside, this is ultimately just a function type.
deriving instance Functor (Ev g)

-- Morally, evert = flip id
evert :: g a -> Ev g a
evert u = Ev $ \e -> e u

如果g是Rigid，我们可以往另一个方向走，从悬浮中恢复函子值：

-- Morally, revert = flip fmap extractors
revert :: Rigid g => Ev g a -> g a
revert (Ev s) = s <$> extractors

Ev g本身是Distributive，不管是什么g——毕竟，它只是一个函数：

-- We need unsafeCoerce (yikes!) because GHC can't be persuaded that we aren't
-- doing anything untoward with the existential.
-- Note that flip = fflip @((->) _)
instance Rigid (Ev g) where
    fflip = Ev . flip . fmap (\(Ev s) -> unsafeCoerce s)

-- Analogously, flap = distribute @((->) _)
instance Distributive (Ev g) where
    distribute = Ev . flap . fmap (\(Ev s) -> unsafeCoerce s) 

此外，fflip和distribute任意Rigid/Distributive函子可通过路由evert和revert：

-- fflip @(Ev g) ~ flip = distribute @((->) _) @((->) _)
fflipEv :: Rigid g => (a -> g b) -> g (a -> b)
fflipEv = revert . fflip . fmap evert

-- distribute @(Ev g) ~ flap = distribute @((->) _) _
distributeEv :: (Rigid g, Functor f) => f (g a) -> g (f a) 
distributeEv = revert . distribute . fmap evert

revert，事实上，就足以实现Distributive. 在这种情况下，分配律相当于要求evert和revert相反：

revert . evert = id  -- "home" roundtrip, right inverse law
evert . revert = id  -- "away" roundtrip, left inverse law

两次往返分别对应于两个非自由分配律：

fmap runIdentity . distribute = runIdentity                               -- identity
fmap getCompose . distribute = distribute . fmap distribute . getCompose  -- composition

（文档distribute . distribute = id中所述的要求Data.Distributive最终相当于这两条法律，加上自然性。）

早些时候，我推测了一个涉及的同构fflip：

flap . fflip = id  -- "home" roundtrip, left inverse Rigid law  
fflip . flap = id  -- "away" roundtrip, would-be right inverse law

可以直接验证刚性定律，flap . fflip = id，等价于另一个“家”往返，revert . evert = id。另一个方向比较棘手。所谓的同构可以像这样链接：

                        g (a -> b)        
    {fflip => <= flap}              {evert => <= revert}
a -> g b                                                   Ev g (a -> b)
    {fmap evert => <= fmap revert} {distribute => <= distribute}
                             a -> Ev g b

让我们假设严格的法律成立。我们想证明fflip . flap = id当且仅当evert . revert = id，所以我们必须处理两个方向：

• 首先，让我们假设evert . revert = id. 绕方格的逆时针方式从a -> g b到g (a -> b)等于fflip（见fflipEv上面的定义）。由于逆时针方式由三个同构组成，因此它fflip具有逆。由于flap是它的左逆（根据刚性定律），它也必定是它的逆。因此fflip . flap = id。

• 其次，让我们假设fflip . flap = id. 同样，从a -> g bto逆时针的方式g (a -> b)是fflip，但现在我们知道它有一个逆时针，即flap。因此，构成逆时针方式的每个函数都必须有一个逆函数。特别是，revert必须有一个逆。由于evert是它的右逆（根据刚性定律），它也必定是它的逆。因此，evert . revert = id。

上面的结果使我们能够精确定位Rigid与 相关的位置Distributive。刚性函子是一种可能的分配，除了它只遵循分配的恒等律，而不是复合的恒等律。制作fflip一个同构，flap作为它的逆，相当于升级Rigid到Distributive。

杂记

• 看fflip和flap从一个单子来看，我们可以说，刚性单子都配备有Kleisli箭头内射转换静态箭头。使用分布式单子，转换升级为同构，这是如何Applicative和Monad等价Reader的推广。

• extractors浓缩了大部分Distributive内容。对于任何分布函子g，都有一个g (g a -> a)值，其中每个位置都填充有匹配的g a -> a提取器函数。似乎准确地说，当我们从 移动到 时Distributive，Rigid我们失去了位置和提取器将匹配的保证，并且失去了从无到有重建适当函数形状的能力。在这种情况下，值得再看一下本答案早期的extractors实现Sel。任何a -> r函数都对应一个Sel r a -> a提取器，这意味着通常会有无数我们无法枚举的提取器，因此我们必须满足非同构fflip和infuse（事后看来，const这出现在extractors已经放弃游戏的实现中）。这感觉有点像缺少Traversable函数实例。（不过，在这种情况下，如果函数的域类型是可枚举的，Data.Universe样式，则有一种方法可以作弊。我不确定实际上是否有这样的解决方法，无论是不切实际的，对于Sel.）

• 我在很大程度上通过镜像 的形状和内容分解（对偶类）的工作方式获得了关于revert同构的结果。（探索形状和内容主题的一篇非常易读的论文是Bird 等人的《Understanding Idiomatic Traversals Backwards and Forwards》）。虽然更详细地介绍可能最好留到单独的帖子中，但至少有一个问题值得在这里提出：类似于 的概念是否有意义？我相信它确实如此，尽管我的感觉是它听起来不如DistributiveTraversableRigidTraversableRigid可能。“co-rigid”伪遍历的一个例子是一个数据结构，它配备了一个遍历复制效果，然后在重建应用层下的结构时丢弃相应的重复元素，以便遵循恒等律——但不是组合之一。

• 说到revert，Ev构造本身就很有意义：它是自由分配函子的编码。特别是，evertandrevert可liftF与retract自由单子相媲美，以及与其他自由结构的类似功能。（在这种情况下，revert完全相反evert暗示了Distributive它的强度。在某些情况下，撤回丢弃信息更为常见，就像在 的一般情况下发生的那样Rigid。）

• 最后，但并非最不重要的是，还有另一种理解 的方式Ev：这意味着多态提取器类型表示分配函子，在Representable某种意义上，evert对应于index、 和revert、tabulate。不幸的是，量化使得在 Haskell 中用实际Representable接口表达它非常尴尬。（这是一种症状，我不得不伸手unsafeCoerce去提供Ev它的自然Rigid和Distributive实例。）如果它是一种安慰，无论如何它都不会是一个非常实用的表示：如果我已经拥有一个多态提取器，我实际上并没有需要index提取值。