PolyML功能和种类

Question

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

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

Answer 1

什么这个所要求的是：

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

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

例如，id "cat" = "cat"和id() =()。后面的值是单位类型，它是只有1个值的类型。请注意，从unit到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] 

而且正如约翰所说，这些功能必须是不纯的。我也会去例外。