function - PolyML 函数和类型

Question

[...] 一对函数tofun : int -> ('a -> 'a)和fromfun : ('a -> 'a) -> int这样的(fromfun o tofun) n函数，n每个n : int.

谁能向我解释这实际上要求什么？我正在寻找对此的更多解释，而不是对此的实际解决方案。

Answer 1

这要求的是：

1) 一个高阶函数tofun，当给定一个整数时，它返回一个多态函数，它具有 type 'a->'a，这意味着它可以应用于任何类型的值，返回相同类型的值。这种函数的一个例子是：

- fun id x = x;
val id = fn : 'a -> 'a

例如，id "cat" = "cat"和id () = ()。后面的值是 unit 类型，是一个只有 1 个值的类型。unit请注意，从to unit（即，id或等效的东西）只有 1 个总功能。这强调了定义的困难tofun：它返回一个类型的函数，'a -> 'a除了标识函数之外，很难想到其他函数。另一方面 - 此类函数可能无法终止或可能引发错误但仍然有类型'a -> 'a。

2)fromfun应该接受一个类型的函数'a ->'a并返回一个整数。所以例如fromfun id可能评估为0（或者如果你想变得棘手，它可能永远不会终止或者它可能会引发错误）

3）这些应该是彼此的倒数，因此例如fromfun (tofun 5)需要评估为5。

直观地说，这在足够纯的函数式语言中应该是不可能的。如果在 SML 中是可能的，我的猜测是通过使用 SML 的一些不纯特性（允许副作用）来违反引用透明性。或者，技巧可能涉及引发和处理错误（这也是 SML 的一个不纯特性）。如果您找到了在 SML 中有效的答案，那么看看它是否可以翻译成令人讨厌的纯函数式语言 Haskell 会很有趣。我的猜测是它不会翻译。

Answer 2

您可以设计以下属性：

fun prop_inverse f g n = (f o g) n = n

以及 和的定义tofun，fromfun

fun tofun n = ...
fun fromfun f = ...

您可以测试他们是否支持该属性：

val prop_test_1 =
    List.all
      (fn i => prop_inverse fromfun tofun i handle _ => false)
      [0, ~1, 1, valOf Int.maxInt, valOf Int.minInt]

正如约翰所说，这些功能一定是不纯的。我也会有例外。