PolyML 函数和类型

Question

[...] a pair of functions tofun : int -> ('a -> 'a) and fromfun : ('a -> 'a) -> int such that (fromfun o tofun) n evaluates to n for every n : int.

任何人都可以向我解释这实际上要求的是什么？我正在寻找更多的解释，而不是实际的解决方案。

Answer 1

求的是：

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

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

例如，id "cat" = "cat" 和 id () = ()。后面的值是 unit 类型，这是一个只有 1 个值的类型。请注意，从 unit 到 unit（即 id 或等效的东西）只有 1 个总函数。这强调了定义 tofun 的难度：它 return 是类型 'a -> 'a 的函数，除了恒等函数，很难想到其他函数。另一方面——这样的函数可能无法终止或可能引发错误并且仍然具有类型 'a -> 'a.

2) fromfun 应该采用 'a ->'a 类型的函数和 return 整数。所以例如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]

正如 John 所说，这些函数一定是不纯的。我也会有例外。

PolyML 函数和类型

PolyML Functions and Types

types

function

sml

polyml