13

The user 'singpolyma' asked on reddit if there was some general structure underlying:

data FailList a e = Done | Next a (FailList a e) | Fail e

A free monad was suggested, but I wondered if this could be modeled more generally via applicative functors. In Abstracting with Applicatives, Bazerman shows us that the sum of two applicative functors is also an applicative functor, with bias to the left/right, provided we have a natural transformation in the direction of the bias. This sounds like it's what we need! Thus, I started my proposal, but then quickly ran into problems. Can anyone see solutions to these problems?:

Firstly, we start with the definition of the sum of two functors. I started here because we want to model sum types - either successes or successes and a failure.

data Sum f g a = InL (f a) | InR (g a)

And the two functors we want to work with are:

data Success a = Success [a]
data Failure e a = Failure e [a]

Success is straight forward - it's essentially Const [a]. However, Failure e I'm not so sure about. It's not an applicative functor, because pure doesn't have any definition. It is, however, an instance of Apply:

instance Functor Success where
  fmap f (Success a) = Success a

instance Functor (Failure e) where
  fmap f (Failure e a) = Failure e a

instance Apply (Failure e) where
  (Failure e a) <.> (Failure _ b) = Failure e a

instance Apply Success where
  (Success a) <.> (Success b) = Success (a <> b)

instance Applicative Success where
  pure = const (Success [])
  a <*> b = a <.> b

Next, we can define the sum of these functors, with a natural transformation from right to left (so a left bias):

instance (Apply f, Apply g, Applicative g, Natural g f) => Applicative (Sum f g) where
  pure x = InR $ pure x
  (InL f) <*> (InL x) = InL (f <*> x)
  (InR g) <*> (InR y) = InR (g <*> y)
  (InL f) <*> (InR x) = InL (f <.> eta x)
  (InR g) <*> (InL x) = InL (eta g <.> x)

And the only thing we now have to do is define our natural transformation, and this is where it all comes crumbling down.

instance Natural Success (Failure e) where
  eta (Success a) = Failure ???? a

The inability to create a Failure seems to be the problem. Furthermore, even being hacky and using ⊥ isn't an option, because this will be evaluated, in the case where you have InR (Success ...) <*> InL (Failure ...).

I feel like I'm missing something, but I have no idea what it is.

Can this be done?

4

2 回答 2

5

我很确定“正确”的答案是制作e一个幺半群，就像您不喜欢 reddit 讨论中的想法一样。

考虑Failure "oops" [(*1),(*2),(*3)] <*> Failure "doh" [1,2,3]结果应该有“oops”还是“doh”作为失败？通过制作e幺半群，我们捕捉到没有规范选择的事实，并让消费者选择他们的毒药（无论是First, Last, [], 等等）

请注意，此解决方案与(Maybe e, [a])表示非常相似，不能正确处理流式传输/可能无限的数据，因为它对结束列表是否失败很严格。

根据后续帖子（http://comonad.com/reader/2013/algebras-of-applicatives/），不同的编码将使用应用程序的固定点。

然后你获取那里呈现的列表表示 ( FixF (ProductF Embed (Sum (Const ()))) a) 并通过将你的错误幺半群粘贴在单位位置来改变它，以获得以下信息：

Monid mon => FixF (ProductF Embed (Sum (Const mon))) a

请注意，您可以使用 aMaybe而不是 monoid 来获得准确的 a FailList，但就像FailList您一样，除非您编写一个指定组合错误的正确方法，否则不会免费获得应用实例。

另请注意，使用定点方法，如果我们有等价物，Success [(*1),(*2),(*3)] <*> Failure "doh" [1,2,3,4,5]那么我们会返回Success带有三个元素的 a（即，我们在失败时确实是非严格的），而在您建议的方法中，我们会返回Failure带有三个元素的 a 和来自五个元素的错误元素失败列表。这就是流媒体与严格的权衡。

最后，也是最直接的，我们可以type FailList e = Product (Const (First e)) ZipList使用标准的应用机制，得到非常接近原始数据类型的东西。

于 2013-03-21T20:35:53.227 回答
2 
{-# LANGUAGE FlexibleInstances #-}

instance Applicative (Sum Success (Failure e)) where
  pure x = InL $ pure x
  (InL f) <*> (InL x) = InL (f <*> x)
  (InR (Failure e fs)) <*> (InR (Failure _ gs)) = InR (Failure e (fs <*> gs))
  (InR (Failure e fs)) <*> (InL (Success gs)) = InR (Failure e (fs <*> gs))
  (InL (Success gs)) <*> (InR (Failure e fs)) = InR (Failure e (gs <*> fs))

这是因为您始终可以将失败添加到成功列表中；）

你也可以使用这个类型类来代替Natural f g：

class Transplant f g where
  transplant :: f a -> g b -> f b

instance Transplant (Failure e) Success where
  transplant (Failure e _) (Success a) = Failure e a

不知道它在类别理论方面意味着什么。

于 2013-03-17T17:12:24.000 回答