4 
type t = MyInt of int | MyFloat of float | MyString of string
let foo printerf = function
  | MyInt i -> printerf string_of_int i
  | MyFloat x -> printerf string_of_float x
  | MyString s -> printerf (fun x -> x) s

それは報告します：

Error: This expression has type float -> string
       but an expression was expected of type int -> string
4

2 に答える 2

8

この正確なコード スニペット (この Web ページから来ていると思います) を移植する正しい方法は、次の FAQ エントリで説明されているように、ファースト クラスのポリモーフィズムを使用することです。. FAQ エントリを読んでください。クイック リファレンスとして、動作するコードの一例を以下に示します。

type t = MyInt of int | MyFloat of float | MyString of string

type 'b printer = { print : 'a . ('a -> string) -> 'a -> 'b }
let foo erf = function
  | MyInt i -> erf.print string_of_int i
  | MyFloat x -> erf.print string_of_float x
  | MyString s -> erf.print (fun x -> x) s

let () = foo
  { print = fun printer data -> print_endline (printer data) }
  (MyString "Hello World!")

ただし、ここでは、このファーストクラスのポリモーフィズムは実際には必要ないことに注意してください。パラメトリック性により、printerが type のデータでできる唯一のことは'a、それを印刷関数に渡すこと 'a -> stringです。したがって、プリンターの動作は、結果のstringデータに対して何を行うかによって完全に決定されます。別の言い方をすれば、 type'b printerは type と同形であり、string -> 'b他の情報をもたらしません。したがって、次のように書くことができます。

let foo erf = function
  | MyInt i -> erf (string_of_int i)
  | MyFloat x -> erf (string_of_float x)
  | MyString s -> erf s

let () = foo print_endline (MyString "Hello World!")

のタイプfooは現在(string -> 'a) -> t -> 'aです。これは、 継続渡しスタイルとして知られています。この型から取得する唯一の方法'aは、文字列で引数関数を呼び出すことです。したがって、実際には、文字列を返し、関数を呼び出すだけです (継続)。その上で。これは次のように書き換えることができます。

let foo = function
  | MyInt i -> string_of_int i
  | MyFloat x -> string_of_float x
  | MyString s -> s

let () = print_endline (foo (MyString "Hello World!"))

簡単に言えば、あなたが示したコードは非常に複雑であり、それがもたらすと思われる問題は誇張されています。ここでは複雑な型システムは必要ありません。(しかし、FAQ で示されているファーストクラスのポリモーフィズムが実際に役立つ、より良い例を見つけることができます。たまたま、この例は...最悪です。)

歴史的および科学的背景

質問によって要求された、ファーストクラスのポリモーフィズムに関する歴史的な余談。

'a . ('a -> string) -> 'a -> 'bは「すべてのため'aに」を意味し('a -> string) -> 'a -> 'bます。これは、型変数(ビット'aによって「定義」される) が多態的であり、自由変数(型のパラメーターとして定義される) を持つ型です。'a .'bprinter

foo上記のコードの最初のバージョンのの型は です'b printer -> t -> 'b。System F型をエンコードしていると理解できる

forall 'b . (forall 'a . ('a -> string) -> 'a -> 'b) -> t -> 'b

ML 型推論アルゴリズムは、「プレフィックス ポリモーフィズム」に制限された型を推論します。これは、すべての型変数が先頭で量化される型です。これは'b上記の型の場合ですが、(多態的な) 引数内'aで数量化されている場合はそうではありません。ML (Hindley-Damas-Milner) 推論システムのこの制限を正確に尊重する型システムは、この型を推論しないため、それを必要とするプログラムを型が正しくないとして拒否します (つまり、「間違っている」のではなく、「正しいことを証明できない」ことを意味します)。 ）。

この制限により、推論システムは決定可能 (完全なシステム F の型推論は決定不可能 (Joe B. Wells)) であり、「プリンシパル」 (プリンシパル型が何であるかがわからない場合は、この SO の議論を参照してください。つまり、推論エンジンは常に最も一般的な型を選択します) が、安全な型システムの通常の悩みの種である適切に型付けされたプログラムも拒否します。

ほとんどの ML 言語 (OCaml、Haskell...) は、ある時点で、本当に書きたいコードに対してこの制限に遭遇しました。90 年代に登場した OCaml については、オブジェクト指向プログラミング パターンを言語でエンコードする作業を行っていました (マニュアルの例を参照)。

これが、ファーストクラスのポリモーフィズムが最初にメソッド型に導入され、後にレコードに拡張された理由です (ファーストクラスのモジュールは、これを可能にする独立した、はるかに最近の追加です)。これが何らかの意味で「フィールド」を持つ「もの」に多かれ少なかれ制限されるのには十分な理由があります。これにより、(必要な) ポリモーフィズム アノテーションを配置する自然な方法が得られ、フィールド プロジェクションはポリモーフィックな値をインスタンス化する必要性をテストするための型チェッカー - 必要に応じて、これにより理論がより単純になります。

この時期の OCaml コミュニティでの研究活動については、たとえば、Extended ML with Semi-Explicit Higher-Order Polymorphism、Jacques Garrigue および Didier Rémy、1997 を参照してください。ファースト クラス ポリモーフィズムへの他のアプローチが開発されました (セクション 5 (関連作品を参照) )、文献の概要については、Dider Le Botlan のRecasting MLFSTを参照してください)、その他のユース ケース、特にHaskell のモナドが見つかりました( Lazy Functional State Threads、Simon Peyton Jones and John Launchbury、1994)。

于 2013-02-05T16:34:57.327 に答える
1

この行から

| MyInt i -> printerf string_of_int i

コンパイラは、 の最初の引数printerfが type を持つべきであると推測しますint -> stringが、次の行から

| MyFloat x -> printerf string_of_float x

の 1 番目の引数printerfはfloat -> string. OCaml には整数と実数で異なる型があることをご存知だと思います... したがって、この型の衝突printerfはコンパイラを病気にします。

printerfこのコードの型として期待していた型は何ですか? 高階関数を避けて、文字列への変換をより簡単に実装する必要があるのではないでしょうか?

于 2013-02-05T12:42:11.260 に答える