ML & HOL

[Shinji KONO]

河野真治 @ 琉球大学情報工学です。

ML は、コンピュータ理論研究者御用達のプログラミング言語です。
最初に知ったのは、東大の大形計算機センタで入ったのと、それ
をゼミで説明した先輩がいたから。

型宣言をプログラムコードから推論する型推論と言うのが売りで
す。ということは、型がないのと同じ。自分で矛盾しない限りエ
ラーにならない。型推論は実は、Prolog のun ification と同じ
だから、型のないPrologと、型推論のMLとは、実は、ほとんど同
じ。

この言語が(理論研究者の間で)有名なのは、HOL という会話型定
理証明システムが、かなり早いうちから、この上で実装されてい
たから。自己矛盾的なんだけど、MLの自由な型付けが、定理証明
システムの実装を容易にしているわけ。

-1 :: [2,3,4,5];
> val it = [1, 2, 3, 4, 5] : int list

上が自分で入力したもので、ML (ここではMoscow MLという処理系)
が推論した型がint l ist として表示されている。この言語もポ
インタがない言語です。ということは、GCがある言語ってことだ
な。

- fun zip(l1,l2) =
if null l1 orelse null l2 then []
else (hd l1,hd l2) :: zip(tl l1,tl l2);
> val zip = fn : 'a list * 'b list -> ('a * 'b) list

- zip([1,2,3],["a","b","c"]);
> val it = [(1, "a"), (2, "b"), (3, "c")] : (int * string) list

とかになると、ほとんど意味不明だけど、orelse みたな便利な構
文が多いのも特徴です。hd が carで、tl が cdr 。:: が cons
というと、LISPを知っている人はわかるはず。

ちょっと面白いのは、curry 化が入っている。f(a,b) という複数
の引数の関数を、g = f'(a) という関数が返す関数g を使って、(
f'(a)) (g) みたいに書ける。つまり、特殊化した関数を返すこと
が出来ます。どんな風に実装しているかは、あまり考えたくない
が...

- fun curried_zip l1 l2 = zip(l1,l2);
> val curried_zip = fn : 'a list -> 'b list -> ('a * 'b) list

- fun zip_num l2 = curried_zip [0,1,2] l2;
> val zip_num = fn : 'a list -> (int * 'a) list

- zip_num ["a","b","c"];
> val it = [(0, "a"), (1, "b"), (2, "c")] : (int * string) list

ってな感じ。

個人的には、あまり好きな言語ではないです。HOLも難しすぎると
いうのが印象。でも、論理を勉強するなら、やっておけば? って
なところですね。ML使うぐらいなら、僕は、P rolog 使うだろう
な。上の例だと、こんな感じ。

SICStus 4.0.0 (i386-darwin-8.8.1): Thu Mar 1 22:07:26 CET 2007
Licensed to SP4ie.u-ryukyu.ac.jp temp
| ?- [user].
% compiling user...
| zip([],_,[]).
| zip(_,[],[]).
| zip([H1|T1],[H2|T2],[(H1,H2)|T3]) :- zip(T1,T2,T3).
|
| zip_num(I,O) :- zip([0,1,2],I,O).
| ^D
% compiled user in module user, 0 msec 632 bytes
yes
| ?- zip([1,2,3],[a,b,c],X).
X = [(1,a),(2,b),(3,c)] ?
yes
| ?- zip_num([a,b,c],X).
X = [(0,a),(1,b),(2,c)] ?
yes
| ?- zip(X,Y,[(1,a),(2,b),(3,c)]).
X = [1,2,3],
Y = [a,b,c|_A] ? ;
X = [1,2,3|_A],
Y = [a,b,c] ? ;
no
| ?-

ソフトウェア工学では、(他で教えないから仕方なく) 論理も教え
ているんだけど、その一環で使う気だったんだが、install めん
どくさすぎ～ epkg にいれるか。

MLの処理系は、Standard ML, ocaml, NewJersey ML とかあるが、
HOLは、Moscow MLがお勧めらしい。OS X でも動くようですが、HOL
の muddy.o のDynamic loading で、stat_a lloc がないとか言っ
てくる。install 時に mosml のbinaryからsymbolを落してしまっ
ているらしいが... 一応、動いているみたいな気もするが、もう
少し調べないとだめだな。

http://www.dina.kvl.dk/~sestoft/mosml.html

http://sourceforge.net/projects/hol/

---
Shinji KONO @ Information Engineering, University of the Ryukyus
河野真治 @ 琉球大学工学部情報工学科

[ku...@gssm.otsuka.tsukuba.ac.jp]

久野です。

ko...@ie.u-ryukyu.ac.jpさん:
> 型宣言をプログラムコードから推論する型推論と言うのが売りで
> す。ということは、型がないのと同じ。

何書いてるんですか。違うでしょ。

> 自分で矛盾しない限りエラーにならない。

矛盾があればコンパイル時に解る。大切じゃないですか。

> 型推論は実は、Prolog のunification と同じだから、型のない
> Prologと、型推論のMLとは、実は、ほとんど同じ。

型のない言語では矛盾があってもそれにぶちあたる経路を実行しない
と間違いが発現しない。テストで全部の経路を通ることは不可能。発現
したときに「何がわるかったか」も探求しないといけない。コンパイラ
の出す型エラーの方が洩れもないし解りやすいしずっといいでしょ。

型推論は型がないのと同じなんて教えないでくださいよ～(泣) 久野

[Shinji KONO]

河野真治 @ 琉球大学情報工学です。

In article <0705160847...@utogw.gssm.otsuka.tsukuba.ac.jp>, ku...@gssm.otsuka.tsukuba.ac.jp writes
> 型推論は型がないのと同じなんて教えないでくださいよ～(泣) 久野

同じってのは言いすぎか...

> 型のない言語では矛盾があってもそれにぶちあたる経路を実行しない
> と間違いが発現しない。テストで全部の経路を通ることは不可能。発現
> したときに「何がわるかったか」も探求しないといけない。コンパイラ
> の出す型エラーの方が洩れもないし解りやすいしずっといいでしょ。

一方で、世の中を複雑にしているものの一つでもありますね。

「プログラム書くときに最適化を考えるな」と言いつつ、double
にするか float にするか悩むのを強制されるのも、実はうっとうしい。

Open/GLみたいに、引数の型毎に違う関数が用意されているのを
見たりすると「なんだかなぁ」と思います。

Cだとポインタで渡せば、型なんてないも同然だしな。

ML の「別に、型宣言なんて要らないんだよ」ってのは、それなりに
説得力はありますね。

[ku...@gssm.otsuka.tsukuba.ac.jp]

久野です。

ko...@ie.u-ryukyu.ac.jpさん:
> 一方で、世の中を複雑にしているものの一つでもありますね。

まあそれはあるんだけど、2つの側面から記述するから突き合わせて
エラーが解るという面もあるんで。

> 「プログラム書くときに最適化を考えるな」と言いつつ、double
> にするか float にするか悩むのを強制されるのも、実はうっとうしい。

え、Prologみたいに1つの型だけで行くと決めるのならfloatなんて捨
ててdoubleだけにすりゃいいでしょ。

> Open/GLみたいに、引数の型毎に違う関数が用意されているのを
> 見たりすると「なんだかなぁ」と思います。
> Cだとポインタで渡せば、型なんてないも同然だしな。

そりゃ言語が古いから。

> ML の「別に、型宣言なんて要らないんだよ」ってのは、それなりに
> 説得力はありますね。

結局何が言いたかったんだ～ 久野