Note

サイト
最近のコメント
 | 

2009-04-22

[] オーバーロードが解決されるルール

どうもこんばんは。G'Camlの路上販売を試みたものの巨大資本の前に敗れ去り、港*1で海を眺めているYTです。

型レの発表内容について、id:camlspotterさんに補足いただきました。ありがたや。

Obj.magic(またはassert false)を使わないで済む構造など、非常に参考になります。

で、型レでlimitationsとして、次のようなis_same_typeの各引数に同じ型を与えた場合、int -> intは'b -> 'cにもマッチするためオーバーロードが解決されずtrue_tが得られないみたいな話をしたのでした。

val is_same_type: [| 'a -> 'a -> true_t | 'b -> 'c -> false_t |]

それに対して、このような反論?がなされてます。

さて、型が同じかどうか判定できないのではないかという話があったけれども、これは、マァ出来る、という主張をしておきたい

(中略)

これは GCaml の変態的 overload resolution priority のおかげ。Overload resolution しなくちゃいけないけど、複数のケースがマッチするときは、先に宣言された方を勝手に GCaml が選んでくれる。正直キモいが、便利な時もある。とういう訳で、型が同じかどうか、というか、 unifiable かどうかは、GCaml では expansive let による auto overload resolution を使えば可能、ということです:

確かに上が優先というのはk.inabaさんの資料の内容とも一致します。

しかし現実にis_same_typeはオーバーロードが解決されない。例示されたTComp.compareと、is_same_typeの何が違うのかイマイチわからなかったので、色々実験してみました。

# module TypeLevel:
    sig
      type ('a, 'b) cons
      type nil
    end =
  struct
    type ('a, 'b) cons = unit
    type nil = unit
  end;;
module TypeLevel : sig type ('a, 'b) cons type nil end
# open TypeLevel;;
# type true_t = (nil, nil) cons;;
type true_t = (TypeLevel.nil, TypeLevel.nil) TypeLevel.cons
# type false_t = nil;;
type false_t = TypeLevel.nil
(* 型レで上手くいかないと言った形 *)
# let is_same_type = generic
                     | : 'a -> 'a -> true_t => fun _ _ -> assert false
                     | : 'b -> 'c -> false_t => fun _ _ -> assert false;;
val is_same_type : [| 'a -> 'a -> true_t | 'b -> 'c -> false_t |] = <generic>
# lazy (is_same_type 1 2);;
- : { int -> int -> 'd < [| 'a -> 'a -> true_t | 'b -> 'c -> false_t |] } =>
      'd lazy_t
= <generic>
(* refを付けてみた *)
# let is_same_type2 = generic
                    | : 'a -> 'a -> true_t ref => fun _ _ -> assert false
                    | : 'b -> 'c -> false_t ref => fun _ _ -> assert false;;
val is_same_type2 : [| 'a -> 'a -> true_t ref | 'b -> 'c -> false_t ref |] =
  <generic>
# lazy (is_same_type2 1 2);;
- : true_t ref lazy_t = <lazy>
(* listを付けてみた *)
# let is_same_type3 = generic
                    | : 'a -> 'a -> true_t list => fun _ _ -> assert false
                    | : 'b -> 'c -> false_t list => fun _ _ -> assert false;;
val is_same_type3 : [| 'a -> 'a -> true_t list | 'b -> 'c -> false_t list |] =
  <generic>
# lazy (is_same_type3 1 2);;
- : { int -> int -> 'd list < [| 'a -> 'a -> true_t list
                               | 'b -> 'c -> false_t list |] } =>
      'd list lazy_t
= <generic>
(* 抽象型を付けてみた *)
# module T: sig type 'a t end = struct type 'a t = unit end;;
module T : sig type 'a t end
# let is_same_type4 = generic
                    | : 'a -> 'a -> true_t T.t => fun _ _ -> assert false
                    | : 'b -> 'c -> false_t T.t => fun _ _ -> assert false;;
val is_same_type4 : [| 'a -> 'a -> true_t T.t | 'b -> 'c -> false_t T.t |] =
  <generic>
# lazy (is_same_type4 1 2);;
- : true_t T.t lazy_t = <lazy>

結果、生の型とlistはオーバーロードが解決されない。ref(レコード)と抽象型はオーバーロードが解決される。

例示されたTComp.compareは、全体を抽象型tでラップ(と言うのでしょうか。抽象型tの型パラメータとしている)しているためオーバーロードが解決されるようです。

……なんだこれはああああ。

結論、よくわかりませんが抽象型の型パラメータにすることで上優先ルールが働き型の同値判定は可能。Lokiに追いつく道が開けましたバンザイ

*1:G'CamlMacPorts用野良Portfile書きましたのでよろしければご利用ください。

camlspottercamlspotter 2009/04/22 22:22 id:ytqwerty さんのお蔭で昔の事を大分思い出してきました、ありがとうございます。
えーっと、お悩みの件は relaxed value polymorphism で説明できます。恐らく。はてなのエントリでは http://d.hatena.ne.jp/osiire/20090215#1234630188 とそっから辿れるリンクが良い感じ。
OCaml/GCaml では 'a list、'a lazy_t はプリミティブな型で、定義が無いんだけど、実はパラメタ 'a が covariant なのです。一方、'a ref は covariant ではない。だから、
>|ocaml|
# let id x = x;;
val id : 'a -> 'a = <fun>
# id id;;
- : '_a -> '_a = <fun>
# id (lazy None);;
- : 'a option lazy_t = lazy None
# id [];;
- : 'a list = []
# id (ref None);;
- : '_a option ref = {contents = None}
||<
こうなる。これがややこしくなったのが上の例だす。

ytqwertyytqwerty 2009/04/22 23:29 ありがとうございます。URLからたどれる論文を読んでいる途中です。抽象型は、
# let a = (Obj.magic 0: 'a T.t);;
val a : '_a T.t = <abstr>
で'_aとアンダーバーが付くので、式全体で多相が回復できずに、型がひとつに絞られるという解釈でよろしいでしょうか。
ということは使い分ければ好きなタイミングまで型計算を遅らせることもできますね。

camlspottercamlspotter 2009/04/23 09:24 回復、という言葉はなんかなくなってた物が復活したみたいで、気になりますけど、
そういうことです。

 | 
カレンダー
2004 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2005 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2006 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2007 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2008 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2009 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2010 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2011 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2012 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 |
2013 | 01 | 02 | 03 |