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)

Intially我们假设所有的四个参数(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作为输入类型和t输出类型,这意味着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