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] 

而且正如約翰所說，這些功能必須是不純的。我也會去例外。