1

私が定義する場合

fun id x = x

それから自然idにタイプを持っています'a -> 'a

もちろん、は にid 0評価されますが0、これは完全に理にかなっています。

これは完全に理にかなっているので、関数でカプセル化できるはずです。

fun applyToZero (f: 'a -> 'a) = f 0

applyToZeroタイプが('a -> 'a) -> intあり、applyToZero id評価されることを願って0

しかし、applyToZero上記のように定義しようとすると、SML/NJ は次のような奇妙なエラー メッセージを表示します。

unexpected exception (bug?) in SML/NJ: Match [nonexhaustive match failure]
  raised at: ../compiler/Elaborator/types/unify.sml:84.37

これは、コンパイラ自体のバグのように見えます。奇妙ですが、可能です。

しかし、PolyML も気に入りません (ただし、エラー メッセージはそれほど奇妙ではありません)。

> fun applyToZero (f: 'a -> 'a) = f 0;
poly: : error: Type error in function application.
   Function: f : 'a -> 'a
   Argument: 0 : int
   Reason: Can't unify int to 'a (Cannot unify with explicit type variable)
Found near f 0

以下は機能します：

fun ignoreF (f: 'a -> 'a) = 1

推論されたタイプで('a -> 'a) -> int。これは、このタイプの高階関数を作成することが不可能ではないことを示しています。

SML が の私の定義を受け入れないのはなぜapplyToZeroですか? タイプが になるように定義できる回避策はあります('a -> 'a) -> intか?

動機:この質問のパズルを解こうとする試みでtofun、タイプの関数と、すべての整数に対して望ましいプロパティを持つint -> 'a -> 'a別の関数を定義することができました。ただし、私の作業の推定タイプは. SML がそれを受け入れるように型注釈を追加しようとする私の試みはすべて失敗しました。その質問をした人がまだそのパズルに取り組んでいる可能性があるため、 の定義を示したくありませんが、 の定義はまったく同じエラーメッセージを引き起こします。fromfunfromfun (tofun n) = nnfromfun('int -> 'int) -> 'int)('a -> 'a) -> intfromfunapplyToZero

4

2 に答える 2

4

これは、SML で使用されているような普通の Hindley-Milner では実行できません。これは、いわゆる高ランクまたはファースト クラスのポリモーフィズムをサポートしていないためです。型注釈'a -> 'aと型('a -> 'a) -> intは、あなたが考えていることを意味するものではありません。

型変数のバインダーを明示的にすると、それがより明確になります。

fun ignoreF (f: 'a -> 'a) = 1

実際に意味する

fun 'a ignoreF (f: 'a -> 'a) = 1

つまり、引数ではなく、'a関数全体のパラメーターです。したがって、関数の型はignoreFf

ignoreF : ∀ 'a. (('a -> 'a) -> int)

'aここでは、全称量指定子としての型で明示的なバインダーを作成します。SML ではすべての量指定子をその構文で暗黙的に保持しているのに対し、型理論ではそのような型をこのように記述します。今、あなたが思っていたタイプが書かれるでしょう

ignoreF : (∀ 'a. ('a -> 'a)) -> int

違いに注意してください: 最初のバージョンでは、 get の呼び出し元ignoreFが をインスタンス化する方法を選択できる'aため、何でもかまいません。関数はそれを想定できませんint(これがapplyToZero型チェックを行わない理由です)。2 番目のタイプでは、引数の呼び出し元が選択しますignoreF。

しかし、そのような型は Hindley-Milner ではサポートされていません。すべての ∀ が最も外側のレベルにある、いわゆるプレネックス ポリモーフィズム(またはランク 0 ポリモーフィズム) のみをサポートします。これが、この制限の下であいまいさがないため、それらを暗黙的に保持できる理由です。上位ポリモーフィズムの問題は、その型推論が決定できないことです。

したがってapplyToZero、SML で必要な型を持つことはできません。このようなことを実現する唯一の方法は、モジュール システムとそのファンクターを使用することです。

functor ApplyToZero (val f : 'a -> 'a) = struct val it = f 0 end

ところで、SML/NJ から引用したエラー メッセージは、表示されたコードが原因である可能性はありません。あなたは何か他のことをしたに違いありません。

于 2016-11-26T09:08:31.097 に答える