Ben*_*ood 31 haskell functor category-theory applicative
应用函子是众所周知的,并且在Haskellers中广受欢迎,因为它们能够在有效的环境中应用函数.
在类别理论术语中,可以证明以下方法Applicative:
pure :: a -> f a
(<*>) :: f (a -> b) -> f a -> f b
Run Code Online (Sandbox Code Playgroud)
相当于有一个Functor f操作:
unit :: f ()
(**) :: (f a, f b) -> f (a,b)
Run Code Online (Sandbox Code Playgroud)
这个想法是写pure你只是用给定的值替换()in unit,并写(<*>)你将函数和参数压缩到一个元组,然后在它上面映射一个合适的应用程序函数.
此外,这种对应关系变成了Applicative法律成左右自然monoidal十岁上下的法律unit和(**),所以实际上是一个适用函子也恰恰是一类理论家称之为一个宽松monoidal仿函数(松懈,因为(**)仅仅是一个自然的转变,而不是同构).
好的,很好,很棒.这是众所周知的.但是,这只是一个家庭不严monoidal函子-那些尊重的monoidal结构产品.松散的幺正算子涉及两种幺半群结构的选择,在源头和目的地:如果你把产品变成总和,你就会得到:
class PtS f where
unit :: f Void
(**) :: f a -> f b -> f (Either a b)
-- some example instances
instance PtS Maybe where
unit = Nothing
Nothing ** Nothing = Nothing
Just a ** Nothing = Just (Left a)
Nothing ** Just b = Just (Right b)
Just a ** Just b = Just (Left a) -- ick, but it does satisfy the laws
instance PtS [] where
unit = []
xs ** ys = map Left xs ++ map Right ys
Run Code Online (Sandbox Code Playgroud)
似乎通过unit :: Void -> f Void唯一确定将其转换为其他幺半群结构变得不那么有趣,所以你真的有更多的半群继续.但仍然:
Applicative吗?Cir*_*dec 16
"整齐的替代演示" Applicative基于以下两个等价物
pure a = fmap (const a) unit
unit = pure ()
ff <*> fa = fmap (\(f,a) -> f a) $ ff ** fa
fa ** fb = pure (,) <*> fa <*> fb
Run Code Online (Sandbox Code Playgroud)
获得这个"整洁的替代演示" Applicative的技巧与诀窍相同zipWith- 在接口中替换显式类型和构造函数,以及可以传递类型或构造函数以恢复原始接口的内容.
unit :: f ()
Run Code Online (Sandbox Code Playgroud)
替换为pure我们可以替换类型()和构造函数() :: ()进行恢复unit.
pure :: a -> f a
pure () :: f ()
Run Code Online (Sandbox Code Playgroud)
并且类似地(尽管不是那么简单)用于取代类型(a,b)和构造(,) :: a -> b -> (a,b)成liftA2以回收**.
liftA2 :: (a -> b -> c) -> f a -> f b -> f c
liftA2 (,) :: f a -> f b -> f (a,b)
Run Code Online (Sandbox Code Playgroud)
Applicative然后<*>通过将函数应用程序提升($) :: (a -> b) -> a -> b到仿函数中来获得好的运算符.
(<*>) :: f (a -> b) -> f a -> f b
(<*>) = liftA2 ($)
Run Code Online (Sandbox Code Playgroud)
为了找到PtS我们需要找到的"整洁的替代演示"
Void来恢复unitEither a b和构造函数替换Left :: a -> Either a b并Right :: b -> Either a b恢复的东西**(如果你注意到我们已经有了一些构造函数Left并且Right可以传递给你,你可以**在不遵循我使用的步骤的情况下找出我们可以替换的内容;直到我解决之后我才注意到这一点)
这立即让我们成为unit总和的替代方案:
empty :: f a
empty = fmap absurd unit
unit :: f Void
unit = empty
Run Code Online (Sandbox Code Playgroud)
我们想找到一个替代品(**).有一种替代方法可以将Either它们作为产品的功能编写.它在面向对象的编程语言中显示为访问者模式,其中sum不存在.
data Either a b = Left a | Right b
{-# LANGUAGE RankNTypes #-}
type Sum a b = forall c. (a -> c) -> (b -> c) -> c
Run Code Online (Sandbox Code Playgroud)
如果您更改了either参数的顺序并部分应用它们,那么这就是您所获得的.
either :: (a -> c) -> (b -> c) -> Either a b -> c
toSum :: Either a b -> Sum a b
toSum e = \forA forB -> either forA forB e
toEither :: Sum a b -> Either a b
toEither s = s Left Right
Run Code Online (Sandbox Code Playgroud)
我们可以看到Either a b ? Sum a b.这允许我们重写类型(**)
(**) :: f a -> f b -> f (Either a b)
(**) :: f a -> f b -> f (Sum a b)
(**) :: f a -> f b -> f ((a -> c) -> (b -> c) -> c)
Run Code Online (Sandbox Code Playgroud)
现在很明显是**做什么的.它将fmap某些内容延迟到它的两个参数上,并结合了这两个映射的结果.如果我们引入一个新的运算符,<||> :: f c -> f c -> f c它只是假设fmap已经完成了ing,那么我们可以看到
fmap (\f -> f forA forB) (fa ** fb) = fmap forA fa <||> fmap forB fb
Run Code Online (Sandbox Code Playgroud)
或者回到以下方面Either:
fa ** fb = fmap Left fa <||> fmap Right fb
fa1 <||> fa2 = fmap (either id id) $ fa1 ** fa2
Run Code Online (Sandbox Code Playgroud)
所以我们可以PtS用下面的类来表达所有可以表达的内容,并且PtS可以实现的所有内容都可以实现以下类:
class Functor f => AlmostAlternative f where
empty :: f a
(<||>) :: f a -> f a -> f a
Run Code Online (Sandbox Code Playgroud)
这几乎可以肯定是一样的Alternative类,但我们并没有要求该Functor会Applicative.
这只是一个Functor这是一个Monoid所有类型.它等同于以下内容:
class (Functor f, forall a. Monoid (f a)) => MonoidalFunctor f
Run Code Online (Sandbox Code Playgroud)
所述forall a. Monoid (f a)约束是伪代码; 我不知道如何在Haskell中表达这样的约束.
lef*_*out 15
在你甚至可以谈论幺半群算子之前,你需要确保你处于幺半群类别.碰巧Hask是以下列方式的幺半群类别:
() 作为身份(,) 作为bifunctor(a,()) ? ((),a) ? a和(a,(b,c)) ? ((a,b),c).就像你看到,它也是一个monoidal范畴,当你交换()的Void和(,)为Either.
然而,monoidal不会让你走得太远 - 让Hask如此强大的原因在于它是笛卡尔闭合的.这给了我们currying和相关的技术,没有它们,应用程序将毫无用处.
甲monoidal范畴可以是笛卡儿闭当且仅当其身份是终端对象,即类型到其中存在正好一个(当然,我们忽略⟂这里)箭头.A -> ()任何类型都有一个功能A,即const ().A -> Void但是没有任何功能.相反,Void是初始对象:存在恰好一个箭头从它,即absurd :: Void -> a方法.这样的幺半群类别不能是笛卡尔闭合的.
当然,现在您可以通过绕箭头方向轻松切换初始和终端.这总是让你处于双重结构中,所以我们得到了一个cocartesian封闭的类别.但这意味着您还需要翻转幺半体仿函数中的箭头.那些被称为决定性的仿函数(并推广comonads).凭借Conor一直如此惊人的命名方案,
class (Functor f) => Decisive f where
nogood :: f Void -> Void
orwell :: f (Either s t) -> Either (f s) (f t)
Run Code Online (Sandbox Code Playgroud)
我在类别理论方面的背景非常有限,但是FWIW,你的PtS课让我想起了这个Alternative类,看起来基本上是这样的:
class Applicative f => Alternative f where
empty :: f a
(<|>) :: f a -> f a -> f a
Run Code Online (Sandbox Code Playgroud)
唯一的问题当然是它Alternative的延伸Applicative.然而,也许人们可以想象它是单独呈现的,那么组合Applicative就会让人联想到具有非交换环状结构的仿函数,两个幺半群结构作为环的操作?IIRC Applicative和AlternativeIIRC 之间也有分配法.