函数式编程中的签名/类型(OCaml)

10

我开始学习函数式编程(OCaml),但是我不理解一个关于fp的重要话题:签名(我不确定它是否是一个合适的名称)。当我输入一些内容并使用ocaml编译时,例如:

# let inc x = x + 1 ;;
val inc : int -> int = <fun>

这很简单,但我不知道为什么会这样:
let something f g a b = f a (g a b)

输出:

val something : (’a -> ’b -> ’c) -> (’a -> ’d -> ’b) -> ’a -> ’d -> ’c = <fun>

我想对于你们中的许多人来说,这个话题绝对是函数式编程的基础,但我在这里寻求帮助,因为我在互联网上没有找到有关OCaml签名的任何信息(虽然有些关于Haskell签名的文章,但没有解释)。

如果这个话题在某种程度上能够生存下来,我会在这里发布几个函数,它们的签名使我感到困惑:

# let nie f a b = f b a ;; (* flip *)
val nie : (’a -> ’b -> ’c) -> ’b -> ’a -> ’c = <fun>

# let i f g a b = f (g a b) b ;;
val i : (’a -> ’b -> ’c) -> (’d -> ’b -> ’a) -> ’d -> ’b -> ’c = <fun>


# let s x y z = x z (y z) ;;
val s : (’a -> ’b -> ’c) -> (’a -> ’b) -> ’a -> ’c = <fun>

# let callCC f k = f (fun c d -> k c) k ;;
val callCC : ((’a -> ’b -> ’c) -> (’a -> ’c) -> ’d) -> (’a -> ’c) -> ’d = <fun>

感谢您的帮助和解释。

术语说明(可帮助您的文献搜索):在Ocaml中,“签名”通常意味着其他东西,即模块的类型类似于基本表达式和值。您所询问的有时称为“类型签名”,但通常只称为“类型”,或者当存在变量时称为“类型方案”。 - Gilles 'SO- stop being evil'
2个回答

19

为了理解这个类型签名,有几个概念你需要掌握,我不知道你已经掌握了哪些,所以我会尽力解释每个重要的概念:

柯里化

你知道,如果你有类型 foo -> bar,它描述了一个函数接受类型为 foo 的参数并返回类型为 bar 的结果。由于 -> 是右结合的,类型 foo -> bar -> bazfoo -> (bar -> baz) 相同,因此它描述了一个接受类型为 foo 的参数并返回类型为 bar -> baz 的值的函数,这意味着返回值是一个接受类型为 bar 的值并返回类型为 baz 的函数。

这样的函数可以像这样调用:my_function my_foo my_bar,因为函数应用是左结合的,所以它等价于 (my_function my_foo) my_bar,即它将 my_function 应用于参数 my_foo,然后将作为结果返回的函数应用于参数 my_bar

因为它可以这样调用,类型为 foo -> bar -> baz 的函数通常被称为“接受两个参数的函数”,我在本答案的其余部分也会这样称呼它。

类型变量

如果你定义一个函数像这样:let f x = x,它将拥有类型 'a -> 'a。但是,'a 在 OCaml 标准库中实际上并不是一个定义过的类型,那它是什么?

' 开头的任何类型都是所谓的 类型变量。类型变量可以代表任何可能的类型。因此,在上面的例子中,f 可以使用 intstringlist 或者任何其他类型调用——没有关系。

此外,如果同一个类型变量在类型签名中出现超过一次,它将表示相同的类型。因此,在上面的例子中,这意味着 f 的返回类型与参数类型相同。因此,如果使用 int 调用 f,它将返回一个 int。如果使用 string 调用它,则返回一个 string,依此类推。

因此,类型为 'a -> 'b -> 'a 的函数可以接受两个任意类型的参数(第一个和第二个参数的类型可能不同),并返回与第一个参数相同类型的值,而类型为 'a -> 'a -> 'a 的函数将接受两个相同类型的参数。

关于类型推断的一个说明:除非你显式给一个函数指定类型签名,否则 OCaml 总是会为你推导出最通用的类型。因此,除非函数使用仅适用于特定类型的操作(例如 +),否则推导出的类型将包含类型变量。

现在来解释这个类型...

val something : ('a -> 'b -> 'c) -> ('a -> 'd -> 'b) -> 'a -> 'd -> 'c = <fun>

这个类型签名告诉你something是一个接受四个参数的函数。

第一个参数的类型是'a -> 'b -> 'c。也就是说,这是一个接受两个任意、可能不同类型的参数并返回任意类型值的函数。

第二个参数的类型是'a -> 'd -> 'b。这同样是一个带有两个参数的函数。需要注意的重要事项是该函数的第一个参数必须与第一个函数的第一个参数具有相同的类型,而函数的返回值必须与第一个函数的第二个参数具有相同的类型。

第三个参数的类型是'a,这也是两个函数的第一个参数的类型。

最后,第四个参数的类型是'd,这是第二个函数的第二个参数的类型。

返回值的类型将是'c,即第一个函数的返回类型。


1
不错的写作。看到你的版本后,我放弃了我的版本。在柯里化和类型变量之后,我还会将类型推断融入解释中。正如你所知,他的第一个函数说int -> int是因为它能够从使用+运算符中推断出来。他的其他函数没有提供这种信息,所以他最终得到了类型变量。 - xscott
@xscott:谢谢。那是一个很好的观点。我已经在类型变量部分的最后一段添加了一条注释。我认为添加一个完整的关于类型推断的部分超出了这个问题的范围。我认为这里重要的是理解类型的含义,而不是ocaml如何得出它们。 - sepp2k
哇,现在我知道了更多!谢谢!但是我对这个笔记有一个问题:“这里需要注意的重要事情是,函数的第一个参数必须与第一个函数的第一个参数具有相同的类型,并且函数的返回值必须与第一个函数的第二个参数的类型相同。”为什么必须这样做?为什么不是其他方式呢? - lever7
@lever7:因为第一个函数的第一个参数是'a,第二个函数的第一个参数也是'a。如果它是'e'f或其他我们以前没见过的东西,它可以是任何类型。但是正如我所说,如果同一类型变量在同一签名中出现多次,则每次都必须表示相同的类型。 - sepp2k
@lever:或者,如果您的问题是为什么该类型遵循定义:函数“f”和函数“g”都以相同的值(“a”)作为它们的第一个参数。因此,它们必须采用相同的第一个参数类型。进一步地,调用“g”的结果被用作“f”的第二个参数。因此,“f”的第二个参数的类型必须与“g”返回的类型相同。 - sepp2k
谢谢,我想我现在明白了 ;) - lever7

6
如果你真的对这个主题感兴趣(并且可以访问大学图书馆),那么读一下Wadler的优秀著作(尽管有些过时)“函数式编程入门”吧。它以非常好的方式解释了类型签名和类型推断。
另外两个提示:请注意,箭头->是右结合的,因此您可以从右边括起来,这有时有助于理解事情,即a -> b -> ca -> (b -> c)相同。这与第二个提示相关:高阶函数。您可以做以下操作:
let add x y = x + y
let inc = add 1

在函数式编程中,把“add”看作是一个必须接收两个数字参数并返回数字值的函数通常是不正确的。它也可以是一个接收一个数字参数并返回类型为num -> num的函数。
理解这一点将有助于您理解类型签名,但您也可以在没有此知识的情况下进行操作。以下是简单明了的解释:
# let s x y z = x z (y z) ;;
val s : (’a -> ’b -> ’c) -> (’a -> ’b) -> ’a -> ’c = <fun>

看右边。给y一个参数,所以它的类型是a -> b,其中a是z的类型。x给了两个参数,第一个参数是z,所以第一个参数的类型也必须是a(y z)的类型是b,因此x的类型是(a -> b -> c)。这使您可以立即推断出s的类型。


网页内容由stack overflow 提供, 点击上面的
可以查看英文原文,
原文链接