澄清Haskell函数类型参数

Question

在最近的工作表中,我被要求解释为什么函数f在:f g x = g (g x) x没有类型.

我对Haskell很新,我很困惑,如何在不知道任何有关函数的细节的情况下计算出左右表达式的关联顺序.似乎g应将其定义为:

g :: a -> b,假设类型x是a-不过,这似乎带来麻烦立即为在RHS,g (g x) x似乎暗示g需要两个参数,类型之一b和类型之一a.此外,我也坚持如何阅读LHS,即确实f接受2个参数:一个函数g和一个变量,x或者只接受1个参数,(g x)？

我想知道是否有人可以告诉我应该如何阅读这些表达方式？

Answer 1

为了能够回答这样的问题,你需要像Haskell编译器一样思考.我们有一个功能.

f g x = g (g x) x

为了使这是很好类型的,我们需要找到的类型f,g和x.现在,f有两个参数,所以

f :: a -> b -> c
g :: a
x :: b

我们也知道g x作为一个表达式必须有意义(我们会说它g x是"格式良好的"),所以g必须是一个x可以应用的函数.所以情况也是如此

g :: b -> t0

t0现在,类型变量在哪里.我们不知道结果g x; 我们只知道它"有道理".现在,外在g (g x) x也必须有意义.所以g必须是一个我们可以应用的类型g x(它有类型t0,如前所述)和x(有类型b)能够得到类型的结果c(函数的返回类型).所以

g :: t0 -> b -> c

现在,这就是问题发生的地方.我们看到,g有三个声明:a,b -> t0,和t0 -> b -> c.为了g拥有所有这三种类型,它们必须统一起来.也就是说,通过插入某些变量的值,它们必须能够变得相同.该a是没有问题的,看到这是一个自由变量和不依赖于其他任何东西,所以我们可以在"设置"它任何我们想做的.因此,b -> t0与t0 -> b -> c必须是相同的.在Haskell中,我们将其写为

(b -> t0) ~ (t0 -> b -> c)

括号(在类型中)是右关联的,所以这相当于

(b -> t0) ~ (t0 -> (b -> c))

为了使两个函数类型相同,它们的参数必须相同,所以

b ~ t0
t0 ~ (b -> c)

通过传递属性,这意味着

b ~ (b -> c)

所以b是一种将自己作为一种论证的类型.这就是Haskell所说的无限类型,并且当前标准不允许这样做.因此,为了使您编写的函数可以接受,b必须是Haskell中不存在的类型.因此,f不是有效的Haskell函数.

Answer 2

相关规则是:

1. 申请书写为并列,即f x适用f于x.

2. 括号用于分隔表达式,而不是用于函数应用程序,即f (g x)适用f于g x.(g x它本身适用g于哪里x.)

3. 应用程序关联到左侧,即f x y = (f x) y.

把这些在一起,我们可以看到g (g x) x = (g (g x)) x,即应用g (g x)到x,这里g (g x)是自身的应用g来g x.

我还应该提到Haskell中的所有函数只需要一个参数.在一个函数看起来有多个参数的地方,确实存在这样的问题:

f x y z = ((f x) y) z

换句话说,f是一个函数,它接受一个参数并返回一个接受参数的函数,并返回一个接受参数并返回一个值的函数.你可能会看到为什么我们有时候更喜欢撒谎并说一个函数需要多个参数,但从技术上讲它并不正确."接受多个参数"的函数实际上是一个返回函数的函数,它可以返回一个函数,依此类推.

Answer 3

1. 函数应用程序是左关联的:a b c解析为(a b) c
2. 函数定义是lambda表达式的语法糖:f x y = ...意思f = \x y -> ...
3. 具有多个参数的Lambda会自动计算:\x y -> ...均值\x -> (\y -> ...)

从而

f g x = g (g x) x

手段

f = \g -> (\x -> (g (g x)) x)

现在让我们尝试推导出类型f.我们给它一个名字:

f :: ta

但到底是ta什么？f被定义为lambda,因此它的类型涉及->(它是一个函数):

\g -> (\x -> (g (g x)) x) :: tb -> tc
g :: tb
\x -> (g (g x)) x :: tc

即类型\g -> ...是tb -> tc对某些类型的tb和tc,和类型g(参数)是tb,并且将结果的类型(功能体)是tc.

因为整个事情是必然的f,我们有

ta = tb -> tc

但是,我们还没有完成tc:

\x -> (g (g x)) x :: td -> te
x :: td
(g (g x)) x :: te

同

tc = td -> te

函数体(我们称之为的类型te)包含一个函数(必须是)对变量的应用x.由此得出:

g (g x) :: td -> te

因为

x :: td
(g (g x)) x :: te

再次向下钻,我们有

g :: tf -> (td -> te)
g x :: tf

因为应用g到g x必须有类型td -> te.最后,

g :: td -> tf

因为

x :: td
g x :: tf

现在我们有两个方程式g:

g :: tf -> (td -> te)
g :: td -> tf

因此

tf       = td
td -> te = tf

tf -> te = tf

在这里我们遇到一个问题:tf根据自身定义,给出类似的东西

tf = (((((... -> te) -> te) -> te) -> te) -> te) -> te

即无限大型.这是不允许的,这就是f没有有效类型的原因.