Haskell 中的手动类型推断

Question

考虑函数

f g h x y = g (g x) (h y)

它的类型是什么？显然我可以使用:t f 来查找，但是如果我需要手动推断，那么最好的方法是什么？

我展示的方法是将类型分配给参数并从那里推断 - 例如x :: a, y :: b 给了我们g :: a -> c 和h :: b -> d 对于一些c,d（来自g x，h y）然后我们继续从那里进行扣除（c = a来自g (g x) (h y) 等）。

但是，这有时会变成一团糟，而且我经常不知道如何进行进一步的扣除或在完成后如何解决。有时会发生其他问题 - 例如，在这种情况下，x 将变成一个函数，但这对我来说在作弊和查找类型之前并不明显。

是否有一种特定的算法始终有效（并且对于人类快速执行而言是合理的）？否则，我是否缺少一些启发式或提示？

Answer 1

让我们检查顶层的函数：

f g h x y = g (g x) (h y)

我们将从为类型分配名称开始，然后随着我们对函数的更多了解，对它们进行专门化。

首先，让我们为顶部表达式分配一个类型。我们就叫它a：

g (g x) (h y) :: a

让我们取出第一个参数并分别分配类型：

-- 'expanding'  (g (g x)) (h y) :: a
h y :: b
g (g x) :: b -> a

再来一次

-- 'expanding' g (g x) :: b -> a
g x :: c
g :: c -> b -> a

再来一次

-- 'expanding' g x :: c
x :: d
g :: d -> c

但请稍等：我们现在有了g :: c -> b -> a 和g :: d -> c。所以通过检查，我们知道c 和d 是等价的（写成c ~ d），还有c ~ b -> a。

这可以通过简单地比较我们推断的g 的两种类型来推断。请注意，这不是类型矛盾，因为类型变量足够通用以适应它们的等价物。如果我们推断出，例如，Int ~ Bool 某处，这将是矛盾的。

所以我们现在总共有以下信息：（省略了一些工作）

y :: e
h :: e -> b
x :: b -> a             -- Originally d, applied d ~ b -> a.
g :: (b -> a) -> b -> a -- Originally c -> b -> a, applied c ~ b -> a

这是通过替换每个类型变量的最具体形式来完成的，即将c 和d 替换为更具体的b -> a。

因此，只需检查哪些参数去了哪里，我们就会看到

f :: ((b -> a) -> b -> a) -> (e -> b) -> (b -> a) -> e -> a

GHC 证实了这一点。

Answer 2

函数是：

f g h x y = g (g x) (h y)

或更详细：

f g h x y = (g (g x)) (h y)

最初我们假设所有四个参数（g、h、x 和 y）都有不同的类型。我们还为我们的函数引入了一个输出类型（这里是t）：

g :: a
h :: b
x :: c
y :: d
f g h x y :: t

但是现在我们要进行一些推理。我们看到例如g x，所以这意味着有一个函数应用程序带有g 函数和x 参数。这意味着g是一个函数，输入类型为c，所以我们将g的类型重新定义为：

g :: a ~ (c -> e)
h :: b
x :: c
y :: d
f g h x y :: t

（这里的波浪号~表示两种类型相同，所以a与c -> e相同）。

由于g 的类型为g :: c -> e，x 的类型为c，这意味着函数应用g x 的结果为g x :: e 的类型。

我们看到另一个函数应用程序，g 作为函数，g x 作为参数。所以这意味着g（即c）的输入类型应该等于g x（即e）的类型，因此我们知道c ~ e，所以现在的类型是：

     c ~ e
g :: a ~ (c -> c)
h :: b
x :: c
y :: d
f g h x y :: t

现在我们看到一个带有h 函数和y 参数的函数应用程序。那么就是说h是一个函数，输入的类型和y :: d的类型一样，所以h的类型是d -> f，也就是说：

     c ~ e
g :: a ~ (c -> c)
h :: b ~ (d -> f)
x :: c
y :: d
f g h x y :: t

最后我们看到一个函数应用程序，其中g (g x) 为函数，h y 为参数，这意味着g (g x) :: c 的输出类型应该是一个函数，f 为输入类型，@987654364 @ 作为输出类型，所以这意味着c ~ (f -> t)，因此：

     c ~ e
     c ~ (f -> t)
g :: a ~ (c -> c) ~ ((f -> t) -> (f -> t))
h :: b ~ (d -> f)
x :: (f -> t)
y :: d
f g h x y :: t

也就是说，由于f 具有g、h、x 和y 的这些参数，所以f 的类型是：

f :: ((f -> t) -> (f -> t)) -> (d -> f) -> (f -> t) -> d -> t
--   \_________ __________/    \__ ___/    \__ ___/    |
--             v                  v           v        |
--             g                  h           x        y

Answer 3

您已经描述了如何做到这一点，但也许您错过了统一步骤。也就是说，有时我们知道两个变量是相同的：

x :: a
y :: b
g :: a -> b    -- from g x
h :: c -> d    -- from h y
a ~ b          -- from g (g x)

我们知道a 和b 是相同的，因为我们将g x（一个b）传递给g，它需要一个a。所以现在我们将所有的bs 替换为a，并继续直到我们考虑了所有的子表达式...

关于你的“一团糟”的评论，我有几件事要说：

1. 这是执行此操作的方法。如果它太难，你只需要练习，它会变得更容易。您将开始培养一种直觉，而且会更容易实现。
2. 这个特殊的功能不是一个简单的功能。我已经为 Haskell 编程了 12 年，但我仍然需要在纸上完成这个统一算法。它是如此抽象的事实并没有帮助 - 如果我知道这个函数的目的是什么，它会容易得多。

Answer 4

简单地写下它们下面的所有实体的类型：

f g h x y = g (g x)   (h y) 
                 x :: x  y :: y
                       h :: y -> a            , h y :: a
               g :: x -> b                    , g x :: b
            g    :: b -> (a -> t)             , x ~ b , b ~ (a -> t)
f :: (x -> b) -> (y -> a) -> x -> y -> t      , x ~ b , b ~ (a -> t)
f :: (b -> b) -> (y -> a) -> b -> y -> t      , b ~ (a -> t)
--       g           h       x    y

因此f :: ((a -> t) -> (a -> t)) -> (y -> a) -> (a -> t) -> y -> t。就是这样。

确实，

~> :t let f g h x y = g (g x) (h y) in f
    :: ((t1 -> t) -> t1 -> t) -> (t2 -> t1) -> (t1 -> t) -> t2 -> t

---

事情是这样的：

1. x 必须有某种类型，我们称之为x：x :: x。
2. y 必须有某种类型，我们称之为y：y :: y。
3. h y 必须有某种类型，我们称之为a：h y :: a。因此h :: y -> a。
4. g x 必须有某种类型，我们称之为b：g x :: b。因此g :: x -> b。
5. g _ _ 必须有某种类型，我们称之为t。因此g :: b -> a -> t.
   与g :: b -> (a -> t) 相同。
6. g 的两个类型签名必须统一，即在涉及的一些类型变量替换下是相同的，因为这两个签名描述了同一个实体，@ 987654343@.
   因此我们必须有x ~ b, b ~ (a -> t)。这是替代品。
7. 拥有f 的所有参数类型，我们知道它产生g 产生的东西，即t。所以我们可以写下它的类型，(x -> b) -> (y -> a) -> x -> y -> t。
8. 最后，我们根据替换来替换类型，以减少涉及的类型变量的数量。因此，我们首先将b 替换为x，然后将a -> t 替换为b，每次都从替换中删除已消除的类型变量。
9. 当替换为空时，我们就完成了。

当然，我们最初可以选择用x 替换b，最后替换为x ~ (a -> t)，然后我们最终会得到相同的类型，如果我们总是用更复杂的类型替换更简单的类型（例如，用(a -> t) 替换b，反之亦然不）。

简单的步骤，有保证的结果。

---

这是另一种更短/更清晰推导的尝试。我们关注g x 充当g 的论点这一事实，因此g x :: x （而琐碎的部分仍然存在，h y :: a）：

f g h x y = g (g x)   (h y)      {- g :: g , h :: h , x :: x , y :: y
  g h x y        x       y                 , g x   :: x   -- !
                  x       a      t         , g x a :: t
                                               x a :: t  ... x ~ a->t
f :: g             ->h     ->x     ->y->t
f :: (x     ->x   )->(y->a)->x     ->y->t 
f :: ((a->t)->a->t)->(y->a)->(a->t)->y->t      -}

毕竟很简单。

定义中的最后一个参数可以省略，如f g h x = (g . g) x . h。