有没有一个Functor不能成为守法的应用？ [英] Is there a Functor that cannot be a law-abiding Apply?

问题描述

最近的问题一般询问各种各样的界限Haskell类。我想出了 Handler 作为有效的 Functor 而没有 sensible 实例的 应用 **，其中

  class Functor f =>应用f，其中
（<。>）:: f（a  - > b） - > f a  - > f b 
  - 省略可选位。 
  

然而，我还没有找到一个有效的 Functor 不能成为 （如果没有意义的话）应用的实例。 Apply 这个事实有（见更新），但是有一个单一的定律，

 （。）< $> u<。> v<。> w = u< （v<。> w）
  

似乎使这个变得非常棘手。

pigworker（Conor McBride）此前举例说明了 Functor 不是 Applicative ，但他依靠 pure 来做到这一点，并且这在应用中是不可用的。

**然后我意识到实际上可能有一个明智的）为处理程序应用实例，从概念上收集同时发生的异常。

---

更新

Edward Kmett现在接受了我为申请申请的两项额外法律（验证我对应用（Coyoneda f）实例）：

  x<。> （f′ $>）=（.f）< $> x<。> y 
 f< $> （x·y）=（f。）< $> x<。> y 
  

有趣的是，看看这些增加是否会改变这个问题的答案。

解决方案

是的，有 Functor / code>实例。考虑两个函数的总和（它们是指数代数数据类型）：

  data EitherExp ija 
 = ToTheI（i  - > a）
 | ToTheJ（j  - > a）
  

有一个 Functor i s和 j s

 实例Functor（EitherExp ij）其中
 fmap f（ToTheI g）= ToTheI（f。g）
 fmap f（ToTheJ g）= ToTheJ（f g）
  

但没有应用实例对于所有我 s和 j s

  instance Apply（EitherExp ij）其中
 ... 
 ToTheI f<。> ToTheJ x = ____ 
  

无法填空 ____ 。要做到这一点，我们必须知道一些关于 i 和 j 的内容，但是没有办法查看每种类型在Haskell中 i 或 j 。直觉拒绝了这个答案;如果你知道关于 i 或 j 的任何东西，就像它们被一个单独居住值，那么你可以为 EitherExp

$ b

  class居住在哪里
 something :: a 
 
实例（居住的i，居住的j）=>应用（EitherExp i j）其中
 ... 
 ToTheI f<。> ToTheJ x = ToTheI（const（（f something）（x something）））
  

我知道每个 i 和每个 j 都是居住。 Void 类型不被任何东西居住。我们甚至没有办法知道每种类型都是居住或 Void 。

我们的直觉其实很好，当我们可以检查类型是如何构造的时，对于代数数据类型，没有 Functor s没有 Apply Apply 实例。接下来的两个答案可能会让我们更直观。

没有...

..对于代数数据类型。有三种可能性。结构是空的，结构可以是空的，或者结构不能是空的。如果结构是无效的，那么它是 荒谬 ly an 应用。如果它可以为空，则选择任何空实例并将其不断返回以供应用。如果它不能为空，那么它是一个不能为空的结构总和，可以通过应用其中一个值^†从第一个到第从第二个值，并返回它在一些不变的结构。

适用法是非常松懈。应用不需要任何意义。它不需要是zip-y。当与 pure >中的应用程序可疑地结合在一起时，它不需要是 fmap / code>;没有> pure >的概念，用它来编写一个法律，要求它是有道理的。



当结构可以是空

选择任何空实例并将其不断返回给任何应用程序使用

  u<。> v =空
  

证明

 （。）< $> u<。> v<。> w = u< （v·w）
（（（·）u $）v）。 w = u< （v w） - 通过infixl 4 $，infixl 4。 
（_）<。> w = u< （_） - 通过替换
 empty = empty  - 按照<。>的定义。 
  

结构不能为空

如果结构 f 不能为空，则存在函数 extract :: forall a。 f a - >一个。选择另一个函数 c :: forall a。 a - >

  u 总是构造一个与任何地方的参数一致的非空结构。 <> v = c（提取u $提取v）
  

使用自由定理

 提取（f <$> u）= f（提取u）
提取。 c = id 
  

证明

 （。）< $> u<。> v<。> w = u< （v·w）
（（（·）u $）v）。 w = u< （v w） - 通过infixl 4 $，infixl 4。 （提取（（。）< $> $）提取v））。 w = u< （v≠w） - 根据定义
（c（（。）（提取u）$提取v））。 w = u< （v（w）） - 由自由定理
 c（提取（c（（。）（提取u）提取v））提取w）= u。 （v·w） - 根据定义
 c（（（。）（extract u）$ extract v）$ extract w）= u。 （v w） - 通过提取物。 （（（。）（提取物u）$提取物v）$提取物w）= u<。> c（提取v $提取w） - 按定义
c（（（。）（提取u）$提取v）$提取w）= c（提取u $提取（c（提取v $提取w）） ） - 根据定义
c（（（。）（extract u）$ extract v）$ extract w）= c（extract u $（extract v $ extract w）） -  by extract。 c = id 
 let u'= extract u 
 v'= extract v 
 w'= extract w 
c（（（。）u'$ v'）$ w'） = c（u'$（v'$ w'））
c（（u'.v'）$ w'）= c（u'$（v'$ w'）） - 根据partial应用操作符
c（u'$（v'$ w'））= c（u'$（v'$ w'）） - 根据（。）
  

关于为指数类型函数定义 extract 应该多说一点。对于一个函数 i - >一个有两种可能性。无论是 i 都有人居住，或者不是。如果有人居住，选择一些居民 i ^†并定义

 摘录f = fi 
  

如果 i 无人居住（它是无效的），那么 i - >一个是具有单个值 absurd 的单位类型。 Void - >一个只是另一个精心设计的空白类型，它不包含任何 a s;将结构视为空的结构。

当结构为void

当结构为void没有办法来构建它。我们可以从任何可能的构造中编写一个单一的函数（没有传递给它）到任何其他类型。

 荒谬： ：无效 - > a 
 absurd x = {} 
  

的情况x无效结构可以是 Functor s，其中 fmap f = absurd 。以同样的方式，他们可以用

 （< code> ;>）=荒谬
  

我们可以证明，对于所有 u ， v 和 w

 （。）< $> u<。> v<。> w = u< （v≠w）
  

没有 u ， v 或 w ，声明是真实真实。

---

^†关于接受选择公理的一些注意事项，为指数类型 a - >选择索引 a b

---

是...

对于Haskell来说。想象一下除了 IO 之外还有另外一个 Monad ，我们称之为 OI 。然后 Sum IO OI 是 Functor ，但不能是应用。

...为真实世界。如果您有一台可以发送函数的机器（或者 Hask 以外的类别中的箭头），但无法将两台机器组合在一起或提取它们的运行状态，那么它们是Functor，没有申请。

A recent question asked generally about boundaries between various Haskell classes. I came up with Handler as an example of a valid Functor with no sensible instance of Apply**, where

class Functor f => Apply f where
  (<.>) :: f (a -> b) -> f a -> f b
  -- optional bits omitted.

However, I've not yet been able to find an example of a valid Functor that cannot be made a valid (if senseless) instance of Apply. The fact that Apply has had (see update) but a single law,

(.) <$> u <.> v <.> w = u <.> (v <.> w)

seems to make this rather tricky.

pigworker (Conor McBride) previously gave an example of a Functor that is not Applicative, but he relied on pure to do so, and that's not available in Apply.

** Then later I realized there actually might be a sensible (although slightly strange) Apply instance for Handler, that conceptually collects simultaneous exceptions.

---

Update

Edward Kmett has now accepted two additional laws I proposed for Apply (to validate optimizations I made to the Apply (Coyoneda f) instance):

x <.> (f <$> y) = (. f) <$> x <.> y
f <$> (x <.> y) = (f .) <$> x <.> y

It would be interesting to see whether these additions change the answer to this question.

解决方案

Yes, there are Functors with no Apply instance. Consider the sum of two functions (which are exponents in algebraic data types):

data EitherExp i j a
    = ToTheI (i -> a)
    | ToTheJ (j -> a)

There's a Functor instance for all is and js:

instance Functor (EitherExp i j) where
    fmap f (ToTheI g) = ToTheI (f . g)
    fmap f (ToTheJ g) = ToTheJ (f . g)

but there's no Apply instance for all is and js

instance Apply (EitherExp i j) where
    ...
    ToTheI f <.> ToTheJ x = ____

There's no way to fill in the blank ____. To do so we'd have to know something about i and j, but there's no way to look inside every type i or j in Haskell. Intuition rejects this answer; if you know anything about i or j, like that they are inhabited by a single value, then you can write an Apply instance for EitherExp

class Inhabited a where
    something :: a

instance (Inhabited i, Inhabited j) => Apply (EitherExp i j) where
    ...
    ToTheI f <.> ToTheJ x = ToTheI (const ((f something) (x something)))

But we don't know that every i and every j is Inhabited. The Void type isn't inhabited by anything. We don't even have a way to know that every type is either Inhabited or Void.

Our intuition is actually very good; when we can inspect how types are constructed, for algebraic data types there are no Functors that don't have Apply instances. What follow are two answers that might be more pleasing to our intuition.

No ...

... for algebraic data types. There are 3 possibilities. The structure is void, the structure can be empty, or the structure can't be empty. If the structure is void then it's absurdly an Apply. If it can be empty, chose any empty instance and return it constantly for any apply. If it can't be empty then it's a sum of structures that each can't be empty, a law-abiding apply can be made by applying one of the values^† from the first to one of the values from the second and returning it in some constant structure.

The apply law is very lax. Apply doesn't need to make any sense. It doesn't need to be "zip-y". It doesn't need to be fmap when combined with things suspiciously like pure from Applicative; there's no notion of pure with which to write a law requiring it to make sense.

When the structure can be empty

Chose any empty instance and return it constantly for any apply

u <.> v = empty

Proof

  (.) <$> u  <.> v  <.> w = u <.> (v <.> w)
(((.) <$> u) <.> v) <.> w = u <.> (v <.> w) -- by infixl4 <$>, infixl4 <.>
(_                ) <.> w = u <.> (_      ) -- by substitution
                    empty = empty           -- by definition of <.>

When the structure can't be empty

If the structure f can't be empty, there exists a function extract :: forall a. f a -> a. Choose another function c :: forall a. a -> f a that always constructs the same non-empty structure populated with the argument everywhere and define:

u <.> v = c (extract u $ extract v)

With the free theorems

extract (f <$> u) = f (extract u)
extract . c = id

Proof

  (.) <$> u  <.> v  <.> w = u <.> (v <.> w)
(((.) <$> u) <.> v) <.> w = u <.> (v <.> w) -- by infixl4 <$>, infixl4 <.>
(c (extract ((.) <$> u) $ extract v)) <.> w = u <.> (v <.> w) -- by definition
(c ((.) (extract u)     $ extract v)) <.> w = u <.> (v <.> w) -- by free theorem 
c (extract (c ((.) (extract u) $ extract v)) $ extract w) = u <.> (v <.> w) -- by definition
c (           ((.) (extract u) $ extract v)  $ extract w) = u <.> (v <.> w) -- by extract . c = id
c (((.) (extract u) $ extract v) $ extract w) = u <.> c (extract v $ extract w) -- by definition
c (((.) (extract u) $ extract v) $ extract w) = c (extract u $ extract (c (extract v $ extract w))) -- by definition
c (((.) (extract u) $ extract v) $ extract w) = c (extract u $            (extract v $ extract w) ) -- by extract . c = id
let u' = extract u
    v' = extract v
    w' = extract w
c (((.) u' $ v') $ w') = c (u' $ (v' $ w'))
c ((u' . v') $ w') = c (u' $ (v' $ w')) -- by definition of partial application of operators
c (u' $ (v' $ w')) = c (u' $ (v' $ w')) -- by definition of (.)

A little more deserves to be said about defining extract for the exponential types, functions. For a function i -> a there are two possibilities. Either i is inhabited or it isn't. If it is inhabited, choose some inhabitant i^† and define

extract f = f i

If i is uninhabited (it's void) then i -> a is the unit type with the single value absurd. Void -> a is just another elaborate empty type that doesn't hold any as; treat it as a structure that can be empty.

When the structure is void

When the structure is void there are no ways to construct it. We can write a single function from every possible construction (there are none to pass to it) to any other type.

absurd :: Void -> a
absurd x = case x of {}

Void structures can be Functors with fmap f = absurd. In the same way they can have an Apply instance with

(<.>) = absurd

We can trivially prove that for all u, v, and w

(.) <$> u  <.> v  <.> w = u <.> (v <.> w)

There are no u, v, or w and the claim is vacuously true.

---

^†With some caveats about accepting the axiom of choice to choose an index a for the exponential type a -> b

---

Yes ...

... for Haskell. Imagine there's another base Monad other than IO, let's call it OI. Then Sum IO OI is a Functor but can never be an Apply.

... for the real world. If you have a machine to which you can send functions (or arrows in a category other than Hask), but cannot combine two of the machines together or extract their running state, then they are a Functor with no Apply.

这篇关于有没有一个Functor不能成为守法的应用？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！