function - PolyML の関数と型

Question

[...] for everyに評価される関数tofun : int -> ('a -> 'a)などのペア。fromfun : ('a -> 'a) -> int(fromfun o tofun) nnn : int

これが実際に何を求めているのか、私に説明できる人はいますか? これに対する実際の解決策よりも、その説明を探しています。

Answer 1

これが求めているのは次のとおりです。

tofun1)整数が与えられると多相関数を返す高階関数。 type を持ちます。これは'a->'a、任意の型の値に適用でき、同じ型の値を返すことを意味します。このような関数の例は次のとおりです。

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

たとえば、id "cat" = "cat"とid () = (). 後者の値は unit 型で、値が 1 つしかない型です。unitfrom to unit(つまり、idまたは同等のもの)の合計関数は 1 つだけであることに注意してください。これは、 を定義することの難しさを浮き彫りにしてtofunいます。それは type の関数を返し'a -> 'a、恒等関数以外に他の関数を考えるのは難しいです。一方、そのような関数は終了に失敗したり、エラーを発生させたりしても型が残っている可能性があります'a -> 'a。

2)fromfun型の関数を取り'a ->'a、整数を返すことになっています。したがって、たとえばfromfun id0 に評価される可能性があります (または、トリッキーにしたい場合は、終了しないか、エラーが発生する可能性があります)。

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]

John が示唆するように、これらの関数は不純でなければなりません。私も例外で行きます。