PolyML函数和类型

Question

..。一对函数tofun : int -> ('a -> 'a)和fromfun : ('a -> 'a) -> int，使得(fromfun o tofun) n为每个n : int计算为n。

有谁能向我解释这到底是想要什么吗？我正在寻找更多的解释，而不是一个实际的解决方案。

Answer 1

这里要求的是：

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

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

例如，id "cat" = "cat"和id () = ()。后一个值是类型单位，它是一个只有一个值的类型。请注意，从unit到unit只有一个总计函数(即id或类似的东西)。这突出了定义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]

正如约翰所建议的那样，这些功能一定是不纯的。我也会例外地去。