17

我偶然发现了许多给你一个功能的练习，并要求你推断出每个练习的类型。

我有以下示例。请注意，这不是我需要完成的作业。我有这个具体例子的答案，并在下面提供。也许有人可以帮助我学习如何推理这种练习。

功能：

h1 f g x y = f (g x y) x

假定的类型：

h1 :: (a -> b -> c) -> (b -> d -> a) -> b -> d -> c

谢谢！

我在这里添加了 27 个 没有解决方案的练习。

其中一些解决方案包含在此处。但是，可以通过使用 GHCi 命令知道类型:t

4

4 回答 4

23 
h1 f g x y = f (g x y) x

因此，从左到右获取参数列表：

  • f是一个应用于两个参数的函数：第一个是结果，(g x y)第二个是x
    • 我们还不知道第一个参数是什么类型，所以我们称之为a
    • 我们也不知道第二种类型，所以我们称之为b
    • 我们也不知道结果类型（所以我们称之为c），但我们知道这一定是返回的类型h1
      • nowf是一个函数映射a -> b -> c
  • g是应用于两个参数的函数：第一个是x，第二个y
    • 我们知道 的第一个参数g与 的第二个参数相同f，所以它必须是相同的类型：我们已经标记了b
    • gis的第二个参数y，我们还没有分配占位符类型，所以它会依次获得下一个，d
    • g的结果是 的第一个参数f，我们已经将其标记为a
      • 所以现在g是一个函数映射b -> d -> a
  • 第三个参数是x，因为这是 的第二个参数f，我们已经标记了它的类型b
  • 第四个参数是y，这是 的第二个参数g，所以我们已经标记了它的类型d
  • 的结果h1是应用f到的结果(g x y) x，正如我们之前所说，所以它具有相同的类型，已经标记c

尽管我们按顺序处理了参数列表，但为每个参数标记、推断和统一类型的实际过程是通过查看.h1

因此，我的第一个项目符号可以详细说明为：

  • f是要考虑的第一个参数，所以让我们看看h1（之后的所有内容=）的主体，看看它是如何使用的
    • f (g x y) x表示f应用于(g x y) x，因此f必须是函数
    • (g x y)在括号中，这意味着正在评估这些括号内的任何内容，并且该评估的结果是f
    • x只是一个简单的参数f，直接从h1自己的参数列表传递
    • 所以，f是一个有两个参数的函数

如果它有助于阅读f (g x y) x，您可以考虑使用类 C 表示法的等效表达式是f(g(x,y), x). 在这里，您可以立即看到f和g是带有两个参数的函数，f第一个参数是g返回的值，等等。

请注意，表达式的左侧h1 f g x y仅给出了一条类型信息：它h1是一个有四个参数的函数。参数名称本身只是表达式右侧（的主体h1）中使用的占位符。这里参数的相对顺序只是告诉我们如何调用h1，但没有告诉我们如何h1在内部使用参数。

同样，这是一个程序样式的等价物（我将使用 Python，因此不必填写任何类型）：

def h1(f, g, x, y):
    return f(g(x,y),x)

这意味着与

h1 f g x y = f (g x y) x

（有一个警告 - 部分应用 - 我怀疑只会在这里进一步混淆问题）。

在这两种情况下，声明（=在 Haskell 中的左侧，:在 Python 中的之前）只告诉我们函数名称和它需要多少个参数。

在这两种情况下，我们可以从定义（Haskell 中的右侧，Python 中的缩进块）推断出和都是两个参数的函数，第一个参数与第二个参数相同，等等。在 Haskell ，编译器为我们做这件事；如果我们使用错误数量的参数调用，Python 只会在运行时抱怨，或者它返回的东西不能用作第一个参数。:fggfgf

于 2012-07-24T20:06:58.327 回答
10

如果你没有什么可做的，你就从事物的使用方式上一步一步推导出类型，把推导出来的部分统一起来。我们有定义

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

所以我们看到它h需要四个迄今为止完全未知类型的参数，让我们调用它们a, b, c, d，结果类型将被调用r。所以 h 的类型必须与

a -> b -> c -> d -> r

现在我们必须看看我们可以对参数类型说些什么。为此，我们查看定义的右侧。

f (g x y) x

sof应用于两个参数，其中第二个是 的第三个参数h，因此我们知道它的类型是c。f我们对的第一个参数的类型一无所知。应用的f结果就是应用的结果h，所以f的结果类型是r。

f :: u -> c -> r
a = u -> c -> r

f右边的第一个参数是g x y。因此我们可以推断

g :: c -> d -> u
b = c -> d -> u

因为g的参数是 的第三个和第四个参数h，因此它们的类型是已知的，结果是 的第一个参数f。

包起来，

f :: u -> c -> r
g :: c -> d -> u
x :: c
y :: d
h :: (u -> c -> r) -> (c -> d -> u) -> c -> d -> r

根据需要重命名类型变量。

于 2012-07-24T20:06:54.880 回答
6

如果你想以正式的方式来做，你可以遵循类型系统的推理规则。如果您只有应用程序，那么简单类型的 lambda 演算的规则就可以了（请参阅这些关于 lambda 演算的讲义的第 2.3 节）。

该算法包括使用类型系统的类型规则构建演绎树，然后通过统一计算术语的最终类型。

于 2012-07-24T20:14:22.847 回答
1

确定函数的类型取决于使用的类型系统。大多数函数式编程语言都基于Hindley-Milner 类型系统，其中有一种类型推断算法（也称为 Hindley-Milner）。对于给定的表达式，该算法派生出所谓的主体类型，这基本上是函数可以具有的最通用类型，如果表达式不可类型化，则该类型会失败。这是 GHCi 在您输入时使用的:t expression。

Hindley-Milner 类型系统允许多态函数，但所有通用量词都必须在类型之外。（通常在使用类型时您看不到量词；量词被省略，它们只是假定的。）例如，consthas type a -> (b -> a)，可以用量词写成(∀a)(∀b)(a -> (b -> a)). 但是，HM 不允许像这样的类型(∀a)(a -> (((∀b)b) -> a))

还有更多表达性的类型系统，例如System F，它允许在任何地方对类型变量使用通用量词，但它的类型推断是不可判定的，并且没有正确的主类型概念。GHC 中有各种语言扩展允许你使用这些类型，但是你失去了类型推断，你必须用类型显式地注释你的函数。

例如：在 HM 中，该函数xx = \f -> f f是不可类型化的（在 GHCi 中尝试）。但是在一个允许通用类型量词无处不在的类型系统中，它有一个类型。在具有适当 GHC 扩展的 Haskell 中，您可以编写： 

{-# LANGUAGE RankNTypes #-}

xx :: (forall a. a -> a) -> (forall b. b -> b)
xx = \f -> f f

（请注意，RankNTypes允许您编写此类量化类型，但不能为此类函数提供类型推断 - 您必须自己声明类型。）

Hindley-Milner 类型系统是一个很好的折衷方案：它允许多态函数与类型推断一起使用。

如果你有兴趣，你可以阅读原论文。但是，它包含一些拼写错误，因此您在阅读时必须保持警惕。

于 2012-08-12T08:13:17.823 回答