使用Applicative和Functor的Haskell函数

Question

我有一个练习题，其中给了我一个函数：

sequence :: Applicative f => [f a] -> f[a]
sequence = foldr (_hole (:)) (pure [])

问题说：

"What type is required for the function that needs to be placed at 
_hole in the following expression? Also give a definition for the 
expression using  and <$> and <*>".

我无法理解问题在问什么。因此，对于我所尝试的，我假设我需要指定运算符，因为它使用的是折叠器，所以我假设它类似于序列 = foldr((+) (:)) (pure[])。

然后对于表达式的定义，我写了这样的东西：

sequence :: <*> f => [f a] -> f[a]
sequence = foldr <$> pure []

我很确定我不是 100% 正确的，所以希望对任何更正有所帮助。

Answer 1

该练习希望您假设某个值_hole是在某处定义的，并且上面的代码类型会检查。然后，目标是确定该_hole的类型。然后，它会询问_hole的可能定义。

例如，如果我们被给予

foo :: Int
foo = 3 + _hole

答案应该是_hole :: Int，因为这就是我们使上面的代码工作所需要的。对于定义_hole = 2是可以的。

相反，在

foo :: Int -> Bool
foo = const _hole "hello" True

然后我们需要_hole :: Bool -> Int -> Bool，例如_hole = b i -> b.

您自己的代码更复杂，因此最好写下所有步骤：

sequence :: Applicative f => [f a] -> f[a]
sequence = foldr (_hole (:)) (pure [])

这里使用了foldr，它(在列表中)具有类型

foldr :: (b -> c -> c) -> c -> [b] -> c

若要进行类型检查，参数必须具有类型

_hole (:) :: b -> c -> c
pure [] :: c

foldr的结果是，只用两个参数调用

sequence :: [b] -> c

由于这必须与上述sequence类型匹配，因此我们得到

[b] = [f a]
c = f [a]

因此，b = f a和

_hole (:) :: f a -> f [a] -> f [a]
pure [] :: f [a]

pure []部件类型按原样检查。另一方面，我们需要

_hole :: (type of (:)) -> f a -> f [a] -> f [a]

即由于(:) :: d -> [d] -> [d]对于任何d，我们得到

_hole :: (d -> [d] -> [d]) -> f a -> f [a] -> f [a]

d可以任意挑选的地方。不过，选择d=a是"自然的"，这样我们就可以得到

_hole :: (a -> [a] -> [a]) -> f a -> f [a] -> f [a]

现在，我们需要根据<$>和<*>编写定义_hole f x y = ??。本质上，我们需要从库中重新实现liftA2。您现在应该能够解决最后一部分。

Answer 2

让我们一步一步地做，逐渐发现我们的定义中涉及的实体的类型。我们被给予

sequence :: Applicative f => [f a] -> f [a]               --  (1)
sequence = foldr (_hole (:)) (pure [])                    --  (2)

这样sequence = mksequence g一些g：

mksequence g xs = foldr (g (:)) (pure []) xs              --  (3)
mksequence g [a,b,...,n] = r where                        --  (4)
r = g (:) a $ g (:) b $ ... $ g (:) n (pure [])       --  (5)
mksequence g [a] = g (:) a (pure [])                      --  (6)
mksequence g []  = pure []                                --  (7)
-- [a,b,...,n] :: [f a]                     <-(4,1)       --  (8)
--  a,b,...,n  ::  f a                      <-(8)         --  (9)
--  r          :: f [a]                     <-(4,1)       --  (10)
-- pure []     :: f [a]                     <-(7,1)       --  (11)
-- g (:)       :: f a -> f [a] -> f [a]     <-(6,8,11,1)

最后，我们找到了g (:)的类型！将其与

(<*>)  :: f (a -> t) -> f a -> f t          , _A :: f (a -> t)
(_A <*> _C)                 :: f t          , _C :: f  a
(_B <*> _C)                 :: f (t -> s)   , _B :: f (a -> (t -> s))
((_B <*> _C) <*> _D)        :: f       s    , _D :: f        t

这样我们就有，

 _B _C _D -> ((_B <*> _C) <*> _D)  
:: f (a -> (t  ->  s)) -> f a -> f  t  -> f  s
g ((:) ::    a -> [a] -> [a]) :: f a -> f [a] -> f [a]

签名几乎匹配！只需轻轻一推，我们就有

g (:) = ( _B _C _D -> ((_B <*> _C) <*> _D)) (pure (:))

所以，概括一下，

g  f2  fa  ft  =  pure f2  <*>  fa  <*>  ft

因为(<*>)与左边有关。重新检查类型，

g  f2  fa  ft  =  pure f2  <*>  fa  <*>  ft
=       f2  <$>  fa  <*>  ft
-- fa                 :: f a
-- f2                 ::   a -> t -> s
-- f2 <$> fa          :: f     (t -> s)
-- ft                 :: f      t
-- (f2 <$> fa) <*> ft :: f           s

事实上，这个定义已经存在，并被命名为liftA2- 用于将二进制函数(f2)"提升"到应用"上下文"(f)：

f2 ::   a ->   t ->   s
liftA2 f2 :: f a -> f t -> f s