理解 (,) <$> length <*> head 的类型

Question

我有这对函数

(,) <$> length :: Foldable t => t a -> b -> (Int, b)

并且

head :: [a] -> a

我想了解

的类型

(,) <$> length <*> head

在(<*>) :: Applicative f => f (a -> b) -> f a -> f b中键入签名，

f :: (->) [a]

a :: b

b :: (Int -> b)

因此，实例化类型为：

(->) [a] (Int, b)

然而，我发现它的类型确实是：

(->) [a] (Int, a)

两个问题，如果可以的话：

为什么 b 切换为 a？
这个类型签名计算的步骤是什么？

Answer 1

让我们继续使用签名

(,) <$> length :: Foldable t => t a -> b -> (Int, b)

但改变

(<*>) :: Applicative f => f (a -> b) -> f a -> f b

到

(<*>) :: Applicative f => f (x -> y) -> f x -> f y

所以不会混淆。正如您所注意到的，显然 f ~ (->) [a]（假设我们正在使用 foldable 的列表实例），因此 x -> y ~ b -> (Int, b)，因此 x ~ b 和 y ~ (Int, b)。这是您错过的部分，可能是由于命名混乱：第二个参数是 f x 或 [a] -> b，您传入 head，即 [a] -> a。这强制 b 与 a 相同，否则类型将无法计算。结果是 f y 或 [a] -> (Int, b)，除了 b 现在是 a，给你 [a] -> (Int, a) 签名。

Answer 2

推导 (,) <$> length <*> head 类型的一种方法是对 length 和 head 进行抽象，然后考虑生成的 lambda 表达式

\l -> \h -> (,) <$> l <*> h

类型

Applicative f => f a -> f b -> f (a, b)

我们需要 length 和 head 的类型 [x] -> Int 和 [x] -> x

f a ~ [x] -> Int
f b ~ [x] -> x

因此

f ~ (->) [x]  -- hom-functor aka Reader 
a ~ Int
b ~ x

产生

([x] -> Int) -> ([x] -> x) -> ([x] -> (Int, x))

作为上述 lambda 表达式的类型。

Answer 3

推导 (,) <$> length <*> head 类型的另一种方法是通过在每一步应用定义来逐步计算它：

(,)                     ::        a   ->       b -> (a, b) 
-- (<$>)                ::       (a   ->         c        ) -> f a -> f c
(,) <$>                 :: f      a   -> f    (b -> (a, b)) -- f a -> f c
--      length          :: [t] -> Int
(,) <$> length          ::             [t] -> (b -> (Int, b))
--            (<*>)     ::             f      (s -> q        ) -> f s -> f q
(,) <$> length <*>      ::  ([t] -> b) -> ([t] -> (Int, b))    -- f s -> f q
--                 head ::   [t] -> t
(,) <$> length <*> head ::                 [t] -> (Int, t)

最棘手的部分是在第三步和第四步中为 f 正确应用 (->) [t]。

Answer 4

我们可以尝试先得出一些更容易理解的公式，这样它的类型就变得“显而易见”。我们有

       (,) <$> length <*> head
=
pure   (,) <*> length <*> head
=
liftA2 (,)     length     head

for any Applicative，由Applicative laws和定义liftA2.

所以我们 (,) 结合了应用值 length 和 head:

包含的/携带的/产生的结果

              (,)
             /   \
            /     \
       length      head

但是length和head是函数，对于函数我们有

              (,)
             /   \
            /     \
       length      head
            \     /
             \   /
               x

即

liftA2 (,)     length     head   x
=
       (,)    (length x) (head   x)

根据 (->) 的 Applicative 实例的定义。

因此(,) <$> length <*> head的类型是liftA2 (,) length head的类型是\ x -> (length x , head x)的类型。那是“显然”“只是”[a] -> (Int , a).

GHCi 同意：

> :t \ x -> (length x , head x)
\ x -> (length x , head x) :: [t] -> (Int, t)

> :t (,) <$> length <*> head
(,) <$> length <*> head    :: [a] -> (Int, a)

length :: Foldable t => t a -> Int 是为任何 Foldable 定义的，但 head :: [a] -> a 专门用于列表，因此 length 的类型专门化为 [a] -> Int.

并且 head 产生与输入列表的元素相同的类型：

            (Int,a)        ~     (,) Int   a
             /   \                    |    |
            /     \                   |    |
       length      \       :: [a] -> Int   |
           \      head     :: [a] ->       a
            \     /            |
             \   /             |
              [a]          ~  [a]

所以没有“转换”。一切都在流动。

理解 (,) <$> length <*> head 的类型

Understanding the type of (,) <$> length <*> head

haskell

types

type-inference

applicative

type-signature