推理 Haskell 中的类型答案

【问题标题】：Reasoning about types in Haskell推理 Haskell 中的类型
【发布时间】：2021-08-06 12:57:50
【问题描述】：

第 995 页上的“Haskell Programming from First Principles”的第 16 章有一个练习来手动计算 (fmap . fmap) 如何进行类型检查。它建议将每个fmap 的类型替换为组合运算符类型中的函数类型：

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

T2fmap :: Functor f => (m -> n) -> f m -> f n

T3fmap :: 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可以帮助我开始，或者提供类似练习的例子来展示如何手工计算类型？

【问题讨论】：

我在this answer的末尾给出了一个缩短的推导，看看是否有帮助。
您在某些地方替换了 a 和 c，但在其他地方没有替换。您必须在任何地方都这样做才能获得正确的类型。

标签： haskell types type-inference function-composition hindley-milner

【解决方案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 的等价/统一下以及它所包含的所有内容。

【讨论】：