3

OCaml が署名の中間のパラメータ化された型を展開できない理由はありますか?

例えば：

(* foo.ml *)
type 'a internal = Foo of 'a
type t = string internal

と：

(* foo.mli *)
type t = Foo of string

エラーを出します。

これは、メモリ表現が時々異なる可能性があるという事実に関連していると思いますが、OCaml バグトラッカーにバグレポートを提出する前に、もっと深い理由があるのではないかと思っていました...

4

2 に答える 2

4

これはメモリ表現の問題ではありません。型宣言を型シグネチャと照合する場合、またはより一般的には、宣言t1が宣言より一般的でないかどうかをチェックする場合t2、型チェッカーは現在、次の 3 つのケースのみを考慮します。

  • t2抽象型または型の省略形です
  • t1両方ともt2和型
  • t1t2両方のレコード

他のケースはエラーで失敗します。あなたの場合、t1（チェックされるタイプ）はタイプの略語であり、t2（仕様）は合計タイプです。これは型エラーで失敗します。

ソース コードを参照しtype_declarationsてください。

foo.mlこれは、これでも失敗するため、メモリ表現の考慮事項ではありません。

type u = Foo of string
type t = u

おそらく、このチェックは洗練される可能性があります。バグトラッカーで質問する必要があります。

編集: このチェックをどこまで改善する必要があるかを判断するのは簡単ではありません。一般に、署名の一致をチェックするときに署名側で略語を展開することは正しくありません。たとえば、次のようなものは受け入れられません。

module Test : sig
  type t = Foo
  type u = t (* to the outside, t and u would be equal *)
end = struct
  type t = Foo (* while internally they are different *)
  type u = Foo (* sum/records are generative/nominative *)
end

逆の方法 (内部の平等が外部から隠されている) は正しく、すでに可能です。

module Test : sig
  type t = Foo
  type u = Foo
end = struct
  type t = Foo
  type u = t = Foo
end;;

fun (x : Test.t) -> (x : Test.u);;
(* Error: This expression has type Test.t but an expression
   was expected of type Test.u *)

現在、型システムの動的セマンティクス (メモリ表現の選択) はそのような展開によって保持されないため、略語展開を検討するときにメモリ表現も考慮されます。

module Test : sig
  type r = { x : float; y : float; z : float } (* boxed float record *)
end = struct
  type 'a t = { x : 'a; y : 'a; z : 'a } (* polymorphic record *)
  type r = float t
end
于 2012-05-08T07:15:31.270 に答える