理解组合仿函数类型的操作

Mar*_*lli 11 haskell functional-programming functor

根据几个消息来源,构成仿函数的Haskell实现或多或少如下:

import Data.Functor.Compose

newtype Compose f g a = Compose { getCompose :: f (g a) }

instance (Functor f, Functor g) => Functor (Compose f g) where
    fmap f (Compose x) = Compose (fmap (fmap f) x)
Run Code Online (Sandbox Code Playgroud)

我的问题是:最后一个定义中x的类型什么?

我会说是f g a,但即使在那里我也很难"看到"计算fmap (fmap f) x

任何人都可以为这一点提供一个明确而完整的工作实例吗?什么fmapping一个TreeMaybe的关注两者Empty的和Node的?

先感谢您.

And*_*ács 18

最后一个定义中x的类型是什么?

在谈论此事之前:你可以问GHC!GHC 7.8及更高版本支持TypedHoles,这意味着如果在表达式(非模式)中放置下划线,并点击加载或编译,则会得到一条消息,其中包含下划线的预期类型和本地范围中的变量类型.

newtype Compose f g a = Compose { getCompose :: f (g a) }

instance (Functor f, Functor g) => Functor (Compose f g) where
    fmap f (Compose x) = _
Run Code Online (Sandbox Code Playgroud)

GHC现在说,省略了一些部分:

Notes.hs:6:26: Found hole ‘_’ with type: Compose f g b …
    -- omitted type variable bindings --
    Relevant bindings include
      x :: f (g a)
        (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:21)
      f :: a -> b
        (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:10)
      fmap :: (a -> b) -> Compose f g a -> Compose f g b
        (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:5)
    In the expression: _
    In an equation for ‘fmap’: fmap f (Compose x) = _
    In the instance declaration for ‘Functor (Compose f g)’
Run Code Online (Sandbox Code Playgroud)

你去,x :: f (g a).经过一些练习,TypedHoles可以帮助您找出复杂的多态代码.让我们试着通过从头开始写出右边来找出我们当前的代码.

我们已经看到这个洞有类型Compose f g b.因此,我们必须有一个Compose _右侧:

instance (Functor f, Functor g) => Functor (Compose f g) where
    fmap f (Compose x) = Compose _
Run Code Online (Sandbox Code Playgroud)

新洞有类型f (g b).现在我们应该看看上下文:

Relevant bindings include
  x :: f (g a)
    (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:21)
  f :: a -> b
    (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:10)
  fmap :: (a -> b) -> Compose f g a -> Compose f g b
    (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:5)
Run Code Online (Sandbox Code Playgroud)

目标是f (g b)在上下文中找到成分.该fmap在上面的清单不幸是指被定义的功能,这有时是有益的,但不是在这里.我们最好知道这些f并且g都是仿函数,因此它们可以被fmap解雇.既然我们有x :: f (g a),我们猜想我们应该fmap做些什么x来获得f (g b):

fmap f (Compose x) = Compose (fmap _ x)
Run Code Online (Sandbox Code Playgroud)

现在洞变成了g a -> g b.但g a -> g b现在非常容易,因为我们拥有f :: a -> b并且gFunctor,所以我们也拥有fmap :: (a -> b) -> g a -> g b,因此fmap f :: g a -> g b.

fmap f (Compose x) = Compose (fmap (fmap f) x)
Run Code Online (Sandbox Code Playgroud)

我们已经完成了.

结束这项技术:

  1. 首先在您不知道如何继续的地方放一个洞.在这里,我们首先将孔放在整个右侧,但通常您会对实现的大多数部分有一个很好的了解,并且您需要在特定的有问题的子表达式中存在漏洞.

  2. 通过查看类型,尝试缩小哪些实现可能导致目标,哪些不可能.填写新表达式并重新定位孔.在证明助理行话中,这被称为"精炼".

  3. 重复步骤2直到你有目标,在这种情况下你已经完成,或者目前的目标似乎是不可能的,在这种情况下回溯直到最后一个非显而易见的选择,并尝试替代精炼.

上述技术有时被称为"类型俄罗斯方块".一个可能的缺点是你可以通过播放"俄罗斯方块"来实现复杂的代码,而无需真正了解你正在做的事情.有时候在走得太远之后,你会严重陷入游戏中,然后你必须开始考虑问题.但最终它可以让你理解那些本来很难掌握的代码.

我个人使用TypedHoles 的所有时间,基本上作为一个反射.我已经非常依赖它了,所以当我不得不回到GHC 7.6时,我感到相当不舒服(幸运的是你甚至可以模仿那里的).


chi*_*chi 4

的类型xf (g a). 例如,x可能是整数树的列表:([Tree Int]也可以写成这样[] (Tree Int),以便f (g x)更紧密地匹配)。

作为示例,考虑succ :: Int -> Int将整数加一的函数。然后,函数fmap succ :: Tree Int -> Tree Int将增加树中的每个整数。此外,fmap (fmap succ) :: [Tree Int] -> [Tree Int]会将前一个应用于fmap succ列表中的所有树,因此它将增加树列表中的每个整数。

相反,如果您有Tree (Maybe Int),则将fmap (fmap succ)增加该树中的每个整数。表单树中的值Nothing不会受到影响,但值Just xx增加。

示例:(GHCi 会话)

> :set -XDeriveFunctor
> data Tree a = Node a (Tree a) (Tree a) | Empty deriving (Show, Functor)
> let x1 = [Node 1 Empty Empty]
> fmap (fmap succ) x1
[Node 2 Empty Empty]
> let x2 = [Node 1 Empty Empty, Node 2 (Node 3 Empty Empty) Empty]
> fmap (fmap succ) x2
[Node 2 Empty Empty,Node 3 (Node 4 Empty Empty) Empty]
> let x3 = Just (Node 1 Empty Empty)
> fmap (fmap succ) x3
Just (Node 2 Empty Empty)
Run Code Online (Sandbox Code Playgroud)