关于 Haskell 中类型的推理

Question

第 995 页的“Haskell 从第一原则编程”的第 16 章有一个练习，用于手动计算 (fmap . fmap) 如何进行类型检查。它建议将每个 fmap 的类型替换为组合运算符类型中的函数类型：

T1 (.) :: (b -> c) -> (a -> b) -> a -> c

T2 fmap :: Functor f => (m -> n) -> f m -> f n

T3 fmap :: Functor g => (x -> y) -> g x -> g y

通过（尝试）将 T2 和 T3 替换为 T1，我得出以下结果：

T4：((m -> n) -> f m -> f n) -> ((x -> y) -> g x -> g y) -> a -> c

此外，它建议检查 (fmap . fmap) 的类型以查看最终类型应该是什么样子。

T5：(fmap . fmap) :: (Functor f1, Functor f2) => (a -> b) -> f1 (f2 a) -> f1 (f2 b)

我无法理解我应该在这里做什么。任何知识渊博的 haskellers 都可以帮助我入门，或者提供类似练习的示例来展示如何手动计算类型吗？

Answer 1

我们循序渐进：

--- fmap . fmap  =  (.) fmap fmap
--- Functor f, g, ... => ..... 

(.)      :: (   b     ->      c    ) -> (a ->  b ) -> a ->     c
    fmap ::  (d -> e) -> f d -> f e
             --------    ----------
(.) fmap ::                             (a ->d->e) -> a -> f d -> f e
                                             ----          ----------
-- then,

(.) fmap      :: (   a     ->  d  ->  e ) -> a   -> f   d   -> f   e
         fmap ::  (b -> c) -> g b -> g c
                  --------    ---    ---
(.) fmap fmap ::                          (b->c) -> f (g b) -> f (g c)
                                          ------      -----      -----

重要的是在每次单独使用类型时一致地重命名所有类型变量，以避免混淆。

我们利用箭头关联在右边的事实，

 A -> B -> C   ~   A -> (B -> C)

类型推断规则是

   f   :: A -> B
     x :: C
   --------------
   f x ::      B    ,  A ~ C

(f :: A -> B) (x :: C) :: B 在类型的等价/统一下 A ~ C 及其包含的所有内容。

关于 Haskell 中类型的推理

Reasoning about types in Haskell

haskell

types

type-inference

function-composition

hindley-milner