Функции и типы 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 () = (), Последнее значение имеет тип unit, который имеет тип только с 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]

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