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 значением. Обратите внимание, что существует только 1 общая функция от 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] 

И как предлагает Джон, эти функции должны быть нечистыми. Я бы тоже пошел с исключениями.