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

Question

以下等式是用 Miranda 语法编写的，但由于 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 -> a？）

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

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

抱歉忘了加上 hd 是列表的标准头函数，定义为：

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 [] 是 RHS 上hd 的参数，所以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的第一个参数的头部并将它的cons到第二个，因此

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

Answer 2

我将使用haskell语法来编写类型。

rc v g i = g (v:i)

这里rc 接受三个参数，所以它的类型类似于a -> b -> c -> d。 v:i 必须是与v 和i 相同类型的元素的列表，所以v :: a 和i :: [a]。 g 应用于该列表，因此 g :: [a] -> d。 如果你把所有东西放在一起，你会得到rc :: a -> ([a] -> d) -> [a] -> d。

正如你已经知道rn :: a -> a，因为它只是身份。

我不知道你在rh 中使用的hd 函数的类型，所以我会跳过。

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

这里f 有两个参数，所以它的类型类似于a -> b -> c。 从第一种情况我们可以推断出b == c，因为我们返回y，并且第一个参数是一个列表。 现在我们知道f :: [a'] -> b -> b。 在第二种情况下，注意x 和y 是如何在rc 的输入中给出的：y 必须是函数[a'] -> d 和rc x y :: a' -> d（这也必须是y 的类型，因为它作为f 的第二个参数传递）。 最后，我们可以说f :: [a'] -> ([a'] -> d) -> ([a'] -> d)。由于-> 是右关联的，这相当于[a'] -> ([a'] -> d) -> [a'] -> d。

你可以用同样的方式推理其余的。