SML/NJのvalue restrictionが怪しい気がする

SML

SML/NJに怪しげな振る舞いを見つけました。
コードとエラーメッセージから推察するに value restriction(値多相性制約) 絡みだと思います。

value restriction
多相型が推論されては困る計算*1を弾くために、SMLが型推論に掛ける縛り。


それを踏まえて問題のコード。

structure S :> sig
  val reset      : unit -> unit
  val register_reset : (unit -> unit) -> unit
end = struct
  fun id x = x

  val reset_fun = ref id
  fun register_reset f = reset_fun := (f o !reset_fun)
  fun reset() = !reset_fun ()
end

これをnjに渡すと…

Standard ML of New Jersey v110.76 [built: Thu Nov 20 22:50:17 2014]
[opening test.sml]
test.sml:8.7-8.25 Warning: type vars not generalized because of
   value restriction are instantiated to dummy types (X1,X2,...)
test.sml:10.17-10.30 Error: operator and operand don't agree [tycon mismatch]
  operator domain: ?.X1
  operand:         unit
  in expression:
    (! reset_fun) ()
test.sml:2.1-11.4 Error: value type in structure doesn't match signature spec
    name: register_reset
  spec:   (unit -> unit) -> unit
  actual: (?.X1 -> ?.X1) -> unit
/home/eldesh/lcl/bin/sml: Fatal error -- Uncaught exception Error with 0
 raised at ../compiler/TopLevel/interact/evalloop.sml:66.19-66.27

S.reset_fun で出ている警告に value restriction という単語が含まれていますね :)


どうやら S.register_reset で、型 unit と処理系が導入した型 ?.X1 がマッチしないと言っているようです。


この ?.X1 とはnjが導入した型変数の表示で、「具体的には分からないけども多相でない型」を表します。
これと同じ型の付く式に具体型が出てくれば、その型に決まります。

処理系毎の振る舞い

このコードは mlton,mlkit,sml#,polyml は受け付けますが、sml/njのみが弾いてしまいます。

処理系 MLton MLKit SML# Poly/ML SML/NJ
accept? pass pass pass pass fail

よってnjがあやしいです*2

ただ恐らく、作った人たちはこの手の動作は把握してる気がするので報告しても直る気がしない…。

work around

上のコードでは関数 reset_fun が多相である必要は無いので、それをアノテーションしてあげればエラーは回避できます。

(* 修正前 *)
val reset_fun = ref id

(* 修正後 *)
val reset_fun : (unit -> unit) ref = ref id

参考

*1:ポインタ(ref)絡みで実行時に型エラーになってしまう

*2:酷い理屈だ