Hatena::ブログ(Diary)

::Eldesh a b = LEFT a | RIGHT b このページをアンテナに追加 RSSフィード Twitter

2014-11-21

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

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のみが弾いてしまいます。


処理系 MLtonMLKitSML#Poly/MLSML/NJ
accept?passpasspasspassfail

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

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

work around

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

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

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

参考

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

*2:酷い理屈だ

2014-10-16

SMLの空レコード型とunit型注釈を付けた時の処理系毎の振る舞い

SML#で使用出来る多相レコードは、SMLのレコード間のサブタイプ関係を推論すると考えると良さそうです。

例えば fn {x:int,...}=> hogehoge という関数は x という int 型のフィールドを持つ任意のレコードを引数に取りますが、これを {x:int} のサブタイプを何でも受け付けると考えます。

すると {x:int, y:string} や {z:'a, x:int, y:'a list} は {x:int} のサブタイプとなります。


ここで以下の関数 e を考えます。

fun e {...} = "unit";

({...} はどんなフィールドも含んでいる必要の無いレコードパターン。)


上の議論から考えれば、レコードに何も(特定のフィールドを)含んで無くてよい型を引数にとるので、e はあらゆるレコード型を受け付けるはずです。つまりあらゆるレコード型のスーパータイプですね。

各実装で評価すると以下のようになります。


型注釈無し

まずは SML# 。

(* SML# 2.0.0 *)
# fun e {...} = "unit";
val e = fn : ['a#{}. 'a -> string]
# e {x=3.14};
val it = "unit" : string
# e (42, "foo");
val it = "unit" : string

妥当な振る舞いに見えます。


次に SML/NJ 。

(* SML/NJ *)
- fun e {...} = "unit";
stdIn:1.2-1.22 Error: unresolved flex record (need to know the names of ALL the fields
 in this context)
  type: {'Z}

おなじみの(?) flex record エラー。何のフィールドにも触れてないけどダメっぽい。さもありなん。


更に MLton 。

(* MLton *)
$ cat e.sml
fun e {...} = "unit"
$ mlton e.sml
Error: e.sml 1.7.
  Unresolved ... in record pattern.
    in: {...}
compilation aborted: parseAndElaborate reported errors

こちらもそれっぽいエラー。


最後に Poly/ML

(* Poly/ML *)
$ poly --use e.sml
Poly/ML 5.5.1 Release
Error- in 'e.sml', line 1.
Can't find a fixed record type. Found near {...}
Error trying to use the file: 'e.sml'

これも妥当に見えます。


型注釈あり

ところでSMLのレコードは一般的に {f1=v1, f2=v2, ..., fn=vn} という形で書きます。

空の場合は {} と書き、これは ():unit と同じ値を指します。

- {}=();
val it = true : bool

{...} は任意のレコードを受け取り、{}は空のレコードであり、()と等しい。

では先ほどのレコードパターン {...} に unit 型の注釈を加えるとどうなるでしょうか?


SML# から。

(* SML# 2.0.0 *)
# fun e ({...}:unit) = "unit";
(interactive):2.8-2.17 Error:
  (type inference 048) type and type annotation don't agree
    inferred type: 'R#{}
  type annotation: unit

unit型はレコードではないのでエラーになっているようです。まぁ妥当に見えます。


で、SML/NJ。

(* SML/NJ *)
- fun e ({...}:unit) = "unit";
val e = fn : unit -> string

え? あれ…?


MLton では…

(* MLton *)
$ cat e.sml
fun e ({...}:unit) = "unit"
$ mlton e.sml
$ (* エラー無し *)

こっちも通ります…。


でも Poly/ML だと

$ poly --use s.sml
Poly/ML 5.5.1 Release
Exception- InternalError: mkArgTuple raised while compiling

Error trying to use the file: 's.sml'

通らない。


まとめ

まとめると以下のようになります。

(* 14/10/19 HaMLetでの結果を追記しました。やはりPoly/MLとSML#が怪しいようですね。 *)


型\処理系SML#SML/NJMLtonPoly/MLHaMLet
{...}passfailfailfailfail
({...}:unit)failpasspassfailpass
({...}:{x:int})passpasspasspasspass

最後の行のパターンも試してみました。適当なレコード型のアノテーションを付けるとどの処理系でも通ります。(推論されるはずの型の)サブタイプを指定していることになりますね。


注釈無しの場合については、そもそも多相レコードに対応してない処理系では {...} を書く(大抵の)場合は注釈が要るはずですし、どれも正しい動作に見えます。


注釈ありの場合は………どうなんですか(@_@)?

{...} が {} にマッチするのが自然だと考えられるので、どちらかと言うと SML# と Poly/ML が間違っているような気がしますが…。

2014-10-02

julia入門で多段階計算


名前だけ知っていた Julia 言語をなんとなく触ってみました。(グラフ(図の方ね)を書く手段を探してたというそれらしい理由もある)

#今回使用したのは Julia 0.3.1 mingw32版 です。


Juliaはそれ自身で項を操作でき、任意の式からその項を生成することが出来ます。

この機能を使えば、項を評価して段階的に項を生成していくような計算(多段階計算/MultiStageProgramming)が実現できそうです。


以下に多段階計算*1の(紹介で)よく在る例を書いてみました。(グラフどこ逝った

基本文法

必要な内容だけ導入しておきます。あとは勘でヨロシク…(^^;;

用語はJuliaとして正しくないかもしれないので注意。


x -> e
ラムダ式
eval(e)
式 e を評価
:e
式 e の項。 #例えば :(1+2) は :3 ではなく :(1+2) になる。
:->
ラムダ式のコンストラクタ
:call
関数適用のコンストラクタ
Expr(e, ...)
項を構成する関数 # 例えば eval(Expr(:->, :x, :x)) で恒等関数が出来る

今回重要なのは Expr関数 です。

:(コロン) は渡した式がそのまま項として(=未評価のまま)得られますが、Exprは普通の関数と同様に引数が評価されることに注意して下さい。

> :(1+(1+2))     # `>' 以降が入力
:(1 + (1 + 2))   # REPLが返す結果

# `#' 以降がコメント
> Expr(:call, :+, 1, 1+2)
:(1 + 3)

多段階計算でpowerを計算

この例では、一般的なpower関数から与える引数(指数)毎に特化した項を生成し、そこから関数を作ります。


#プロンプトには型が表示されないのでMLっぽい注釈がコメントに書いてあります。

まず xのy乗 を計算する(コードを生成する)関数を定義。

# (int code) * int -> int code
> function mult(x,y)
    y==0 ? (:(1)) : Expr(:call, :*, x, mult(x, y - 1))
  end
mult (generic function with 1 method)

cube は任意の式を3回掛けるようなコードを mult から生成します!!

# (int -> int) code
> cube = Expr(:->, :y, mult(:y, 3))
:(y->y * (y * (y * 1)))   # 3に特化した項が出来た

cube を評価すると、引数を3回掛けるような関数になるはず。2を渡すと(当然)8が得られる。

# eval : 'a code -> 'a
> eval(cube)
(anonymous function)  # int->int の関数のはず

> eval(cube)(2)
8                     # やった

もう少し一般化

cube を一般化し、任意の値(y)を任意の回数(n)展開する式を生成する関数を定義することも出来ます。

# int -> (int -> int) code
> exponent = n -> Expr(:->, :y, mult (:y, n))
(anonymous function)

3 を渡すと、任意の値(y)を3回掛けるような項を生成します。

> exponent(3)
:(y->y * (y * (y * 1)))

> eval(exponent(3))(2)
8

ダメな例

ついでに(私が初めに書いた(><)) mult のダメな定義の例を挙げておきます。

> function mult(x,y)
	y==0 ? (:(1)) : :($x * eval(($mult)($x,$y - 1)))
  end
mult (generic function with 1 method)

> mult(:x, 3)
:(x * eval((mult)(x,3 - 1)))

:(コロン) を使っているため、そこでevalの評価が止まってしまっています。

これだと遠回りに普通の関数のように実行されるだけですね :p


感想

型が無いので生成した項にエラーが無いかはプログラマが保障しないといけません。

特に今回のような項を手で組み上げるケースでは、コード生成までは問題無いのにevalするとエラーになる場合がやっかいです。


まともな多段階計算の処理系なら生成された項の型安全性まで検査できるし、同じことですが、ステージを混同してIntとExprを掛け算したりすることも無くなります(多分)。

やはり型が必要ですね。 (anonymous function)てなんやねんヽ(`Д´)ノ


参考

*1:MSP=MultiStageProgramming

2014-09-14

SML/NJのCygwin上でビルドに失敗するバグが修正された

私が以前パッチを書いて報告していた SML/NJのCygwin上でのインストールに失敗するバグ が 110.77(08/22/14) で修正されています。

Here is a list of tracked bugs fixed (or closed) with this release, please see the bug tracker for more details.

..

125 build script is broken on Cygwin-x86

..

http://www.smlnj.org/dist/working/110.77/110.77-README.html

実際のファイルには以下のように記述されてますので、*1

Older versions of Cygwin had a file /usr/include/exceptions.h, but this

file has disappeared in more recent versions. Here is the key bits

taken from ftp://ftp.com.univ-mrs.fr/pub/cygwin/usr/include/exceptions.h

やっぱり古いCygwinでは exceptions.h が存在したようなんですが、Cygwinはどれが本家のソースコードかよく分からないんですよねぇ(^^;;

とりあえずexceptions.hの内容は特にひねりも無く、でっち上げたパッチで正解だったことが分かって良かったです。

2014-09-12

ProofSummit2014とJSSST2014に参加

f:id:eldesh:20140910094313j:image:w300:right

遅めの夏休みを使ってProofSummit2014JSSST2014に行ってきました。

Coqチュートリアルとサマースクール(スパコンの話)に参加し、火曜日のPPLとその他セッションをふらふらしてた感じ。


Coqチュートリアルが主目的で参加したハズなんですが、謎の強烈な眠気であんまり覚えてません…。ひどい。

ssreflectのタクティックはかなりゴルフ的な方針で証明を短くしている感じを受けた気がします。

あとはかなり所謂工数を気にかけてCoq採用事例が解説されていたのが印象的でした。まだ開発で採用されるには時間がかかると思っているのですが、気づいたら証明も出来ない奴は人権が無い世界になるかも知れません。コワイ。


スパコンのサマースクールでは学部の授業を大急ぎでなぞった感じであまりテクニカル(に最新)な話は出ませんでした。

20年後でも使える言語じゃ無いとダメだそうですが、20年前に出来たソフトを使い続けてるんでしょうか。


他で印象に残ってるのは筑波の方のrefinement typeの拡張(?)とガリグ先生の型エイリアスでしょうか。PPL4

前者は自分で質問したのでやはり覚えてますね。

提案手法(述語を何回か展開して近似)では SMTソルバのfixpoint operatorより一般的なケースを扱えるようです。オフラインで教えて頂いたのですが、使ってるのはまさに質問で持ち出したZ3だったようで発表者の方にはその場で答えて欲しかった内容ですね(笑

それはともかくSMTソルバ流行ってますねぇ。


後者はOCamlモジュールの代入は通常定義をコピーするのに対して、名前を追跡するようになるものと理解しました。

アプリカティブファンクタに有用とのことですが、SMLにあっても嬉しいような気がします。どうなんでしょう?

あとNJ(というかCM)がさりげなく槍玉に上げられていたのでOCamlにだって仕様は無いじゃないか ( ー`дー´)と言っておきます(笑


FTDが初日のチュートリアルと被ってたので今回は会場で観られませんでした。

ちょっと残念でしたね。youtubeで公開してるので一応リンク貼っておきます。