如何确定Haskell函数的类型？

Question

我偶然发现了很多练习,它们会给你一个功能,并要求你推断出每个练习的类型.

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

功能:

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

假设的类型:

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

谢谢!

---

我加了27次演习在这里 没有解决方案.

其中一些有解决方案包括在这里.但是,可以使用GHCi命令知道类型:t

Answer 1

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

所以,从左到右获取参数列表:

• f是一个应用于两个参数的函数:第一个是结果,(g x y)第二个是x
  • 我们不知道第一个参数是什么类型,所以我们称之为 a
  • 我们也不知道第二种类型,所以我们称之为 b
  • 我们也不知道结果类型(所以我们称之为c),但我们不知道这一定是通过类型返回h1
    • 现在f是一个函数映射a -> b -> c
• g是一个应用于两个参数的函数:第一个是x第二个y
  • 我们知道第一个参数g与第二个参数相同f,所以它必须是相同的类型:我们已经标记过了b
  • 第二个参数g是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)的f和g是在两个参数两个功能,即g第一个参数是相同f的第二等在Haskell ,编译器为我们做了这个; 如果我们g使用错误数量的参数调用,Python将在运行时抱怨,或者返回f不能用作第一个参数的东西.

Answer 2

如果你没有任何东西,你可以逐步从使用的方式中推断出类型,统一推导出的部分.我们有定义

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

所以f应用于两个参数,第二个参数是第三个参数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

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

Answer 3

如果您想以正式方式执行此操作,则可以遵循类型系统的推理规则.如果你只有应用程序,那么简单输入的lambda演算的规则就可以了(参见关于lambda演算的这些讲义的第2.3节).

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