function - 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，当给定一个整数时，它返回一个多态函数，其类型为 'a->'a，这意味着它可以适用于任何类型的值，返回相同类型的值。此类函数的示例是:

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

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

2) fromfun 应该采用 'a ->'a 类型的函数并返回一个整数。所以例如fromfun id 的计算结果可能为 0(或者如果您想变得棘手，它可能永远不会终止或可能引发错误)

3) 这些应该是彼此相反的，因此，例如fromfun (tofun 5) 需要计算为 5。

直观上，这在足够纯粹的函数式语言中应该是不可能的。如果在 SML 中可行，我的猜测是，这将是通过使用 SML 的一些不纯粹的功能(允许副作用)来违反引用透明度。或者，这个技巧可能涉及引发和处理错误(这也是 SML 的一个不纯粹的功能)。如果你找到一个在 SML 中有效的答案，那么看看它是否可以被翻译成烦人的纯函数语言 Haskell 将会很有趣。我的猜测是它不会翻译。