types - 在函数式编程中确定函数的类型

Question

以下等式是用 Miranda Syntax 编写的，但由于 Miranda 和 Haskell 之间的相似性，我希望 Haskell 程序员应该理解它!

如果定义以下函数:

rc v g i = g (v:i)
rn x = x
rh g = hd (g [])


f [] y = y 
f (x:xs) y = f xs (rc x y)

g [] y = y
g (x:xs) y = g xs (x:y)

你如何计算函数的类型？我想我知道如何为 f、g 和 rn 解决这个问题，但我对部分应用程序部分感到困惑。

rn 将是 * -> * (或任何 -> 任何东西，我认为它是 Haskell 中的 -> a？)

对于 f 和 g，函数类型都是 [*] -> * -> * ?

我不确定如何找到 rc 和 rh 的类型。在 rc 中，g 被部分应用于变量 i - 所以我猜这将 i 的类型限制为 [*]。 rc 和 g 在 rc 的定义中应用什么顺序？是否将 g 应用于 i，然后将结果函数用作 rc 的参数？或者 rc 是否采用 v、g 和 i 的 3 个单独参数？我真的很困惑..任何帮助将不胜感激!谢谢你们。

抱歉忘了补充，hd 是列表的标准 head 函数，定义为:

hd :: [*] -> *
hd (a:x) = a
hd [] = error "hd []"

Answer 1

类型是从已知的类型以及在定义中如何使用表达式推断出来的。

让我们从顶部开始，

rc v g i = g (v : i)

所以 rc :: a -> b -> c -> d我们必须看看可以发现什么关于 a, b, c和 d .在右侧，出现 (v : i) ，所以 v :: a ，我们看到 i :: [a] , c = [a] .然后 g适用于 v : i , 所以 g :: [a] -> d ，总而言之，

rc :: a -> ([a] -> d) -> [a] -> d

rn x = x意味着对 rn 的参数类型没有限制和它的返回类型是一样的， rn :: a -> a .

rh g = hd (g [])

自 rh的论点 g应用于 RHS 上的空列表，它必须具有类型 [a] -> b , 可能有关 a 的更多信息或 b如下。确实， g []是 hd 的参数在 RHS，所以 g [] :: [c]和 g :: [a] -> [c] ， 因此

rh :: ([a] -> [c]) -> c

下一个

f [] y = y 
f (x:xs) y = f xs (rc x y)

第一个参数是一个列表，如果它是空的，结果是第二个参数，所以 f :: [a] -> b -> b由第一个方程得出。现在，在第二个方程中，在 RHS 上， f 的第二个参数是 rc x y ，因此 rc x y必须与 y 具有相同的类型，我们称之为 b .但

rc :: a -> ([a] -> d) -> [a] -> d

, 所以 b = [a] -> d .因此

f :: [a] -> ([a] -> d) -> [a] -> d

最后

g [] y = y
g (x:xs) y = g xs (x:y)

从第一个方程我们推导出 g :: [a] -> b -> b .从第二个，我们推导出 b = [a] ，因为我们取了 g 的头部的第一个参数并将其限制为第二个，因此

g :: [a] -> [a] -> [a]