関数型言語ML(SML, OCaml, etc.), Part 5

関数型言語ML(SML, OC ..

79:デフォルトの名無しさん
07/11/23 15:10:04
今後のハード技術は
スレッドが使いづらい方向に行くと思うぞ

80:デフォルトの名無しさん
07/11/23 15:10:48
有益でないから残らない。
関数型言語はErlangなど残っている方。

81:デフォルトの名無しさん
07/11/23 15:14:30
>>79
どちらかというとスレッドが無いとやってられない方向へ向かってる

82:デフォルトの名無しさん
07/11/23 15:18:45
有益でない言語は残らない。

83:デフォルトの名無しさん
07/11/23 15:24:09
つまりMSにとって有益な言語が残るってことだな

84:デフォルトの名無しさん
07/11/23 15:33:41
Haskell は STM とか頑張っているんだがのう
SML はダメッポス

85:デフォルトの名無しさん
07/11/23 16:14:00
STM?

86:デフォルトの名無しさん
07/11/23 16:18:31
>>84
URLﾘﾝｸ(haskell.g.hatena.ne.jp)

元の処理系に並列化の基盤が無いと、
こういう実験にも使えないのよね

87:デフォルトの名無しさん
07/11/23 16:46:40
間違えた。>>86 は >>85 向け。

88:85
07/11/23 16:59:39
さんきゅう

89:79
07/11/23 18:29:22
スレッドが使いづらい方向に行くっていう意見は、たぶん俺がハード屋で
性能/消費電力/発熱に苦しんでるからかも。

SMPコアには既に限界を感じてる。

ASMPコアで無駄な回路を減らせば、まだまだ上を狙える。
遅延評価・非同期実行（イベント同期）をナチュラルに行なえる言語だと
ハード・ソフトの両面からグッと最適化が効く。

スレッドはSMPと相性がいいかもしれんが、
でもASMPにはマッチしないと思う。

90:デフォルトの名無しさん
07/11/23 18:32:00
スレッド←→遅延評価・非同期実行（イベント同期）
って反対概念でもないよね?

91:デフォルトの名無しさん
07/11/23 18:39:20
>>89
ASMP でも汎用コアが複数あったり、SMP と言っても特殊用途の
コプロ積んでたりするもんじゃないの?

どう転んでもスレッドの重要性は当分は覆らないと思うけどなあ。

92:デフォルトの名無しさん
07/11/23 22:38:05
>>90
確かに。お互いに実現可能なものを持ってるしね。

スレッドはハード層にCPUとしての機能と性能を要求してくるけど、
本当にそんなに大げさな物が必要なのかなーって思ってる。

OS層にはマルチタスク要求があるからスレッドは有益だけどさ。

アプリ層でスレッドを使うときって、
　・CPU複数使って速く処理する
　・ブロッキング処理を非ブロッキング処理にする

こういうのを言語がサポートしてないからじゃない？
（ライブラリじゃなくて言語仕様ね）

それにスレッドっていうキーワードを使って作られたものって、
DSP,SIMD,コプロ等々の存在を無視する気がする。
┌───────┐
│　関数　　　　　　　　　　　　　　　｜
├──┐　　　　　　　　　　　　　｜
｜　ｽﾚｯﾄﾞ　｜　　　　　　　　　　　　　｜
├──┴─┬────┤
｜　CPU　　　　｜DSP,SIMD,コプロ｜
└───┴────┘

言語にはネイティブスレッドを要求するより
こんなものの→（Scatter/Gather、Map/Reduce、遅延評価、イベント同期）
シームレスでポータビリティな仕様と、実装の最適化を要求して欲しい。

93:デフォルトの名無しさん
07/11/23 23:05:28
>>92
結局 CPU 複数使って速く処理するにはスレッドが必要なんだぜ。
何でそんなにスレッドを嫌がるのかは知らんけど、現実には
コプロや SIMD があってもスレッドは必須だよ。

94:デフォルトの名無しさん
07/11/23 23:27:35
話がかみ合ってないな

95:デフォルトの名無しさん
07/11/23 23:38:17
はぐらかしてるだけに見えるけど

96:デフォルトの名無しさん
07/11/24 00:04:53
＞CPU　複数使って速く処理するにはスレッドが必要
違う。
手続き言語andスレッド　によって速い処理を行おうとするから
複数のCPUを要求されている。

でもスレッドじゃ
　　DSP,SIMD,コプロ
この辺をうまく使っていけない。

極論だけど、関数言語がソフトウェアの主流なら
クロックを使わない論理回路で作ったチップにも需要が出るから
そういうのも作るもん。

97:デフォルトの名無しさん
07/11/24 00:15:20
>>96
違うっていうけどさ、元々違う話をしてるんだから当たり前だよ。
俺は現実世界にある CPU をどう有効に使えるかにしか興味無いよ。
そしてその為にはスレッドを使うのが一番の近道。

それにスレッドと SIMD やコプロは排他的な存在じゃないから。

98:デフォルトの名無しさん
07/11/24 00:35:01
>>96
>手続き言語andスレッド�によって速い処理を行おうとするから
>複数のCPUを要求されている。

これは違うよな。プログラマはスレッドなんて別に使いたくない。
シングルコアで高性能の CPU が作れないっていうから、仕方なく
ソフトウェアを並列化してるだけ。DSP も一緒。

99:デフォルトの名無しさん
07/11/24 00:47:23
各CPUにコードをロードさせておいてから、
データばらまいて、関数に突っ込んで、出力を集計すればいいじゃん。

ってこれはMap/Reduceだよな。

100:デフォルトの名無しさん
07/11/24 01:04:45
何だよ、素人か。

101:デフォルトの名無しさん
07/11/24 23:28:42
言語はマルチスレッドをサポートすべき?
│
├CPUシングルスレッド性能は打ち止めだからこれからはマルチスレッドスレッドだよ
│├マルチスレッドをどうにかするのは言語の仕事だよ
││├とりあえずスレッドとロックサポートすればいいよね (古典派)
││├ロックしないよ (モダン派)
││├プロセスは言語の基本だよ (並列言語派)
│││└おっぱいおっぱい (ぱい計算ってうまいの?)
││└マルチスレッドは実装屋の仕事だよ
││
│├マルチスレッドをどうにかするのはOSの仕事だよ
││├1つのプロセス中では並列度上がらないよ
││└小さいプロセスいっぱい作るよ (forkできればそれでいい派)
││
│├CPUごとに仮想マシン割り当てるから問題無いよ
││
│└コプロの命令もメインプロセッサの命令に見せかけるからやっぱスレッドだよ (Intel)
│
├マルチスレッドよりも大切なものがあるよ
│├SMPは限界。処理ごとに回路作るよ
│├高性能処理はベクタマシンだろ。常考 (ベクタ派)
││└GPUを計算に利用しようぜ (新ベクタ派)
│├他マシンとの通信こそ重要だよ (クラスタ派)
│└機械語レベルでなんとかなるよ (スーパースカラ派・コードモーフィング派)
│
└並列こそ計算の本質だよ。データフローマシン最高 (逐次処理は諸悪の根源だよ派)

102:デフォルトの名無しさん
07/11/25 00:13:28
っあらゆるテクニックを使って速く動くように裏で最適化してよ（何も考えたくない派）

103:デフォルトの名無しさん
07/11/25 14:48:34
クラスタ以外は、下へ行けば行くほど現実解から遠ざかっているなw

104:デフォルトの名無しさん
07/11/25 20:21:12
ていうかアプリによってどれがいい違ってくるよね

105:デフォルトの名無しさん
07/11/25 20:24:02
アプリレベルじゃない話も混ざっているみたいだけど
例えば fork を使うと良いアプリってどんなの?

106:デフォルトの名無しさん
07/11/25 20:28:36
ネットワークサービス系はforkがいいと思う。
セキュリティを考えると、
同じプロセスで走らせたくない処理が多い。

107:デフォルトの名無しさん
07/11/25 20:45:54
ネットワークサービス系って一般的にはスレッドプールを作るイメージだけど、
具体的にはどんなアプリを想定してるの?

108:デフォルトの名無しさん
07/11/26 11:28:12
>>84
manticoreがあるでしょ > SML

>>101
> 言語はマルチスレッドをサポートすべき?

関数型言語の場合は、semanticsをどうするかが一番の論点で、
(関数型言語でなくていいことは、他の言語でやればいいし、実際行なわれている)
言語に並列処理能力を持たせるべきかどうかってのは、設問としておかしい。
持たせるとしたらどういう風なものがいいか、研究が行なわれ続けている。

109:デフォルトの名無しさん
07/11/26 12:02:18
>>108
＞関数型言語の場合は、semanticsをどうするかが一番の論点
そーそー、それそれ。
関数型言語にはそういう力があるんだから。

>>92の一番最後に書いたここの部分ね。
＞シームレスでポータビリティな仕様

CがUNIXの力になって
LLがWebアプリの力になったように
関数型言語が並列処理分野の力になると思うんだけど。

今のスレの流れって
なんだかWebアプリの話をしてるときに
C実装レイヤーのことを話してるみたいな気がする。

110:デフォルトの名無しさん
07/11/26 12:04:09
>>108
>関数型言語でなくていいことは、他の言語でやればいい
それはおかしいだろ。
例えばすごく関数型向きなアプリケーションを作ろうとしていて、
たまたま一ヶ所並列計算が必要だと分かったら、それだけで
関数型言語が選択肢から外れるってのは問題だと思わないか？
同じ論法で、汎用言語なら、良く使われる機構は一通りカバーしておくべき。

111:デフォルトの名無しさん
07/11/26 15:39:16
あなたが知らないだけです。

112:デフォルトの名無しさん
07/11/26 20:41:03
>>111
そういうのは例え 2ch でもどうかと思うよ。

manticore ってこれか。まだ実装は公開されてないのね。

URLﾘﾝｸ(manticore.cs.uchicago.edu)

113:デフォルトの名無しさん
07/11/26 22:17:20
>>86
それ、最初の方でoperaionalにSTMの意味を説明しているけど、
それはSTMの実装の一つを紹介している(ことになっている)だけで、
STMは必ずしもそういう実装になる必要はないので読む時には気をつけて。
TMはdatabaseやdistributed computingでよく使われるモデル。

並列処理抽象化のために、実装がいくつも考えられて、
モナド親和性の高いモデルを採用している。

114:デフォルトの名無しさん
07/11/27 14:11:41
CML(URLﾘﾝｸ(cml.cs.uchicago.edu))とOCamlのThreadsライブラリの事もたまには思い出してあげてください。

115:デフォルトの名無しさん
07/11/27 20:54:51
CML って所謂 Green Thread だと思ってた
ちゃんと "Concurrent" に動くの?

116:デフォルトの名無しさん
07/11/28 08:03:00
スケジューラがユーザ空間に(も)ないと、
関数型言語っぽい面白いことができない。

CML→manticoreって人がいるね。

117:デフォルトの名無しさん
07/11/28 23:15:14
せっかく新生した JoCaml のことも思い出してあげてください

118:デフォルトの名無しさん
07/11/28 23:20:30
OCaml はもう良いじゃん...

119:デフォルトの名無しさん
07/11/28 23:29:28
>>114
coThreadライブラリ(URLﾘﾝｸ(cothreads.sourceforge.net))は無視ですか、そうですか。

120:デフォルトの名無しさん
07/11/30 01:25:15
プログラミング in OCaml ~関数型プログラミングの基礎からGUI構築まで~
と
入門OCaml ~プログラミング基礎と実践理解~
どっちがいい？

121:デフォルトの名無しさん
07/11/30 11:09:15
立ち読みして決めろ

122:デフォルトの名無しさん
07/12/01 00:27:53
お前らの感想を言え

123:デフォルトの名無しさん
07/12/01 13:42:43
>>122
昨日発売される本の即日レビューなんて無茶いうな。

　　　入門OCaml
必要なことは大体書いてあるので、基礎的なことは十分できるようになった。
　短所としては、よくあることだけど、ちょっと複雑な機能を説明するときに
複雑な例で解説してる場所がある、とか。そのぶん実用例の確認にはいいんかな。
そういう部分は自分で簡単なもの作ってみて理解するしかない。
　まだ勉強中だけどスレッドやらパーサやらCGIやらの使用例とかあるし
本格的に使うつもりなら買っといていいんじゃないっかな。

あとこの本が無ければSML#とか知らなかった。

124:デフォルトの名無しさん
07/12/01 16:26:55
SML#の本、欲しい

125:デフォルトの名無しさん
07/12/01 17:36:49
>>116
>CML→manticoreって人がいるね。

manticoreってもう使えるの?

126:デフォルトの名無しさん
07/12/01 20:45:42
>>120
どちらかといえば、前者。

127:デフォルトの名無しさん
07/12/02 00:09:43
>>125
>>116は研究者/開発者

128:デフォルトの名無しさん
07/12/02 01:04:45
>>119
正直無駄にHaskell-STM風にモナド前提なのを何とかして欲しい。

129:デフォルトの名無しさん
07/12/02 08:05:45
無駄に？

130:デフォルトの名無しさん
07/12/02 12:32:54
Poly/ML が 5.1 でネイティブスレッドを使える様になっているね
polyml.5.1/libpolyml/processes.cpp 内で pthread 関連の関数を
呼び出しているみたい

Poly/ML を使っている人はこのスレには居ないかな...

131:デフォルトの名無しさん
07/12/02 21:46:29
使ってるよ。
自作のコードはStandard ML系の処理系のほとんどでひととおり動作チェックする。

132:130
07/12/02 22:23:23
今日久々に Poly/ML 見てみたんだけど、結構進化してるよね。
イメージベースの環境から、オブジェクトファイルを吐いて
実行ファイルを生成出来る様に変わっているし、スレッドは
カーネルスレッドをサポートしているし、FFI は C の構造体
を扱えるし、Intel Mac も Solaris もサポートしているし、
あと欲しいのは UNICODE のサポートくらい。

Standard ML 処理系では最強なんじゃないかな。

133:デフォルトの名無しさん
07/12/03 09:37:00
誰かocaml-ssl ってのビルドできた人いますか（0.4.2）

URLﾘﾝｸ(sourceforge.net)

134:デフォルトの名無しさん
07/12/06 00:06:44
SML のソースコードを沢山読んでみたいのですが、
Perl でいう CPAN みたいなのはありませんか?

135:デフォルトの名無しさん
07/12/06 08:34:33
つ URLﾘﾝｸ(www.cs.princeton.edu)

136:デフォルトの名無しさん
07/12/06 09:02:46
ありがとうございます！

137:デフォルトの名無しさん
07/12/07 12:11:14
>>2
>URLﾘﾝｸ(yk.i.hosei.ac.jp)

だいぶ今更かもしれないけど、これ無くなってしまっているね。
欲しい人は今のうちに Web Archive から頂いておいた方が良いかも。

138:デフォルトの名無しさん
07/12/08 02:59:37
>133
Cygwin 上で特に patch なしでビルドできてるけど。何ぞ問題が？

139:デフォルトの名無しさん
07/12/08 16:52:38
過疎っているので、Python スレにあったお題でコードを書いてみました。
"行頭の空白文字列を nbsp に変更するプログラム"

fun replaceWhite file =
　　let fun repLn lst =
　　　　　　　　case hd lst of
　　　　　　　　　　#" " => [#"&", #"n", #"b", #"s", #"p", #";"] @ repLn(tl lst)
　　　　　　　　| #"¥t" => [#"&", #"n", #"b", #"s", #"p", #";",
　　　　　　　　　　　　　　　　　　　　　#"&", #"n", #"b", #"s", #"p", #";",
　　　　　　　　　　　　　　　　　　　　　#"&", #"n", #"b", #"s", #"p", #";",
　　　　　　　　　　　　　　　　　　　　　#"&", #"n", #"b", #"s", #"p", #";"] @ repLn(tl lst)
　　　　　　　　| _ => lst
　　　　　　fun replace out =
　　　　　　　　case TextIO.inputLine out of
　　　　　　　　　　NONE => ()
　　　　　　　　| SOME ln => ((print o String.implode o repLn o String.explode) ln;
　　　　　　　　　　　　　　　　　　　　　　replace out)
　　in (replace o TextIO.openIn) file
　　end;

140:デフォルトの名無しさん
07/12/08 16:56:47
もういっちょ。
"フィボナッチ数を 0 から 35 まで表示するプログラム"

fun fibloop () =
　　let fun fib n = if n < 2 then n else fib(n-1) + fib(n-2)
　　　　　　fun loop 36 = ()
　　　　　　　　| loop cnt = (print(Int.toString(fib(cnt)) ^ "¥n");
　　　　　　　　　　　　　　　　　　　　　　loop (cnt + 1))
　　in loop 0
　　end;

141:デフォルトの名無しさん
07/12/08 21:30:26
次スレを立てる時は >>2 の SML の所にこれを追加して欲しいな
SML を勉強していて一番参考になった

URLﾘﾝｸ(www.geocities.jp)
URLﾘﾝｸ(sml.sourceforge.net)

142:デフォルトの名無しさん
07/12/08 23:42:59
>>137
旧研究室サーバにあった。
URLﾘﾝｸ(133.25.16.150)

143:デフォルトの名無しさん
07/12/10 00:42:45
>>139
...正規表現のライブラリって無いのですか？
いくら静的型付けとはいえ、スクリプト系の言語に比べてかなり冗長で、
いまいちSMLを勉強する気にならないのですが...。

144:デフォルトの名無しさん
07/12/10 03:21:09
取り敢えず Moscow ML には正規表現ライブラリがバンドルされている
みたいだけど、他もあるんじゃないかな。正規表現を使わなくとも
Vector で書いたらコード量は大分少なくなると思う。

まあそんな事は誰でも簡単に調べられる事だし、勉強する気にならない
のであれば他の事をした方が良いと思うよ。自由ってそういう事でしょ。
面白いと思ってすぐに手を動かせる人間が自分で色々探求して行く一方で、
そうじゃない人がいても別に誰も強制したりなんかしない。

そもそも >>139 は SML を勉強し始めて一日目の人間が書いたコード
だから参考にしない方が良いでしょう…

145:デフォルトの名無しさん
07/12/10 09:43:10
>>144
3行でおｋ

146:デフォルトの名無しさん
07/12/10 18:12:49
>>145
俺の
コードに
文句言うな

147:デフォルトの名無しさん
07/12/10 21:34:29
>>144
一日目でそれだけ書ければすごいよ。

148:デフォルトの名無しさん
07/12/10 22:13:04
>>145
3 行 x 80 桁ではこれが限界ですた…

fun r () = let open TextIO String Char val c = (valOf o input1) stdIn; in case c
of #" " => print "＆nbsp;" | #"¥t" => print "＆nbsp;＆nbsp;＆nbsp;＆nbsp;" | #"¥n" =>
print "¥n" | _ =>((print o toString)c;(print o valOf o inputLine)stdIn);r() end;

149:デフォルトの名無しさん
07/12/12 20:07:08
OCamlで
('a -> 'a) -> 'a
という型のY-combinatorを定義することは出来るのでしょうか。
let fix = fun f -> (fun x -> f (fun y -> x x y)) (fun x -> f (fun y -> x x y))
や
let rec fix f = f(fun x -> fix f x)
はどうしても、
(('a -> 'b) -> 'a -> 'b) -> 'a -> 'b
という型になってしまいます。(遅延評価をするHaskellでは問題なく書けるのですが)
これだと,TAPLのP144にある,以下の相互再帰が型エラーで書けません。
let ff ieio =
{iseven =
(fun x ->
if x=0 then true
else ieio.isodd (x-1));
isodd =
(fun x ->
if x=0 then false
else ieio.iseven (x-1))}

let r = fix ff

150:デフォルトの名無しさん
07/12/13 02:27:16
パターンマッチのある言語で正規表現って必要なんだろうか。
メタランゲージなんだから、そのまま書き下した方がスッキリする。

151:デフォルトの名無しさん
07/12/13 08:08:58
関数型言語のパターンマッチでまだ A.*B 相当とか書けないよね。

152:デフォルトの名無しさん
07/12/13 08:45:20
>>150
正規表現並にconciseな表現ができればね

153:デフォルトの名無しさん
07/12/13 08:58:43
正規表現そのものだと、バックトラックが必要になるからまずいです。

154:デフォルトの名無しさん
07/12/13 17:18:34
中置文字について何かまとめた。トリビア的なものだけど。（OCaml 3.09.2）

頭文字
　　=<>@^&+-*/$%　　どこでも大丈夫
　　|　　二文字以上なら頭文字可
後続文字
　　~　　二文字以上なら頭文字にできるが、頭に使うと前置しかできなくなる。
　　!　　頭文字にすると前置のみに。
　　.:?　　後続文字のみ使用可

155:デフォルトの名無しさん
07/12/15 00:37:16
(* ^ o ^ *)

156:デフォルトの名無しさん
07/12/15 00:39:32
神経を逆撫でするコメントだな

157:デフォルトの名無しさん
07/12/17 12:32:42
with-open-file (fun ch -> fprintf ch "aaa")

みたいなのって標準ライブラリにある？

158:デフォルトの名無しさん
07/12/17 21:14:55
俺も欲しいけど、エラーの扱いとかどうなるんだろ

159:デフォルトの名無しさん
07/12/18 20:20:46
中でfinallyつかえばいいんじゃないかな。

160:デフォルトの名無しさん
07/12/22 10:35:14
ocamlにfinallyなんてないだろ

161:デフォルトの名無しさん
07/12/22 16:22:00
Javaプログラマは夢見るSuccubus
finally かなり例外に依存して生きているの

162:デフォルトの名無しさん
07/12/22 17:32:45
何だ OCaml には finally があるのかと思った
また OCaml 限定の話かよとスルーしてたのに

163:デフォルトの名無しさん
07/12/27 23:00:37
>>149
OCamlでは
('a -> 'a) -> 'a
という型のY-combinatorは定義出来ません。
HaskeiiはLazy evaluationなので、例で書いているように出来るのですが、
OCamlはEager evaluationなので、argumentをすぐに評価しようとするので、それをお書きになったような形で避けるとにコンビネータではなくなってしまいます。
これを避けるにはLazy モジュールを使用してﾅﾝﾁｬｯﾃ遅延評価で解決します。そうすればコンビネータとして扱うことが出来ます。

同様のことはモナドにも言えて、ﾅﾝﾁｬｯﾃ・モジュールを使用すると解決することがあります。

MLのＹコンビネータの書き方はLittle MLerの巻末に書いてあるのでご覧下さい。

164:デフォルトの名無しさん
07/12/28 17:21:19
>>149 >>163

factの実装方法を２通り紹介しておく。

チューリングの賢人鳥
let rec turing's_sage f x = f (turing f) x;;
turing's_sage (fun f x -> if x = 0 then 1 else x * (f (x-1))) 5;;

カリーの雲雀
let lark x (`M y) = x (fun z -> y (`M y) z);;
let curry's_sage f x = lark f (`M (lark f)) x;;
curry's_sage (fun f n -> if n = 0 then 1 else n * (f (n-1))) 5;;

どっちの方法も
- : int = 120
と返ってくる。

165:デフォルトの名無しさん
07/12/28 19:10:27
>>164
スマリヤンの「ものまね鳥」だね。SKIコンビネータ入門にいいよね。
ほかにもJAYとかOWLとか出てきた希ガス。

166:デフォルトの名無しさん
07/12/28 21:22:48
論理学の問題ならCoqを使ってコードを作ればいいんじゃねえか？

URLﾘﾝｸ(coq.inria.fr)

167:デフォルトの名無しさん
07/12/28 21:39:17
(つд⊂)ｺﾞｼｺﾞｼ(;ﾟдﾟ) 論理学の問題

168:デフォルトの名無しさん
07/12/29 00:08:29
Coq is the specification language.

Interactive Theorem Proving And Program Development
by Coq'art: The Calculus Of Inductive Constructions

これ系統の参考文献にこれもいいかも。

TAPL : Types and Programming Languages

169:デフォルトの名無しさん
07/12/29 00:24:27
>>167
数理論理学とコンピュータ・プログラムの間には深い関連性がある。

Ａ．近代論理学の開祖であるフレーゲの概念記法を出発点とするゲンツェンの自然演繹
Ｂ．チャーチの型付きラムダ計算

２つのモデルはカリー・ハワード対応によって同型として対応付けられる。
つまり、論理学の問題と言っているのは、実はコンピュータ・プログラムの問題と言っているのと同じなのだ。
QED.

170:デフォルトの名無しさん
07/12/29 00:51:12
Coq見てみたけどﾜｶﾗﾝｗ

OCaml-Nagoyaの次の本はCoqだな。決定。

171:デフォルトの名無しさん
07/12/29 19:25:22
WindowsのCoqIDEが動かないな。固まったよｗ

172:デフォルトの名無しさん
07/12/30 00:47:12
>>171
うごくよ。
てかProofGeneralが亡くなってる。

173:デフォルトの名無しさん
08/01/01 02:06:59
>>169
その同型になるのは、１階の述語論理のこと？

174:デフォルトの名無しさん
08/01/01 13:37:59
カテゴリカル・コンビネータ理論

175:デフォルトの名無しさん
08/01/01 13:45:05
一階述語論理にカリー・ハワード同型対応で対応するのは、一般の関数型言語で使われている型理論とはだいぶ異なる型理論です。

176:デフォルトの名無しさん
08/01/01 14:36:17
高階述語論理をカリー・ハワード対応させるとどうなるんですか？

177:デフォルトの名無しさん
08/01/01 15:55:45
>>176
どうしたいん？

178:デフォルトの名無しさん
08/01/01 16:07:39
Curry-Howardの対応の依存型（dependent type）があると、高階述語論理を表現することができる。
高階述語論理があれば、「∀f. --- 任意の関数 f について…」という扱いが可能になったり、「関数や述語に関する量化（∀∃）が可能な論理」を構成できる。

179:デフォルトの名無しさん
08/01/01 16:19:56
型付きλ計算の世界では、「値の世界」と「型の世界」の間に明確な分離があり、型の定義中に値が出現するといったことはありません。
しかし、依存型(dependent type)を導入するとこの制限が取り払われて、型が値を持てるようになります。
依存型は単純な型付きλ計算よりもはるかに強力で、うまく使えばリストの長さや配列の境界チェックなどさまざまに応用できます。
しかし強力さの一方で型チェックは複雑になり、一般の依存型では型チェックが停止しない場合もあります。
例えば、基本的には型の部分で計算ができるので、そこに無限ループするような項を入れておけば止まらなくなります。
Curry-Howard Isomorphism により、依存型は述語論理と等価な記述力を持つことになります。
したがって、依存型をつけたλ計算の体系を考えることで、論理式の証明を記述したり、その正しさを検査することが可能になるわけです。

OCAMLのCoq では、単純なλ計算ではなく帰納的に定義された型(Inductive types)を使えるように拡張した
Calculus of Inductive Construction というものに依存型を導入し、システムの根幹としています。

180:デフォルトの名無しさん
08/01/01 16:26:17
最低でも、一階述語論理系を構成できる程度は理解し、その上で、

直観主義論理，Matin-Loefの型理論、依存型算譜言語

の3つをプログラムの基礎として最低限おさえておけ。

181:デフォルトの名無しさん
08/01/01 17:11:13
Curry-Howard Isomorphism をトポスの言葉で表現するとどうなるんですか？

182:デフォルトの名無しさん
08/01/01 17:37:52
>>181
おとなしくシミロン嫁

183:デフォルトの名無しさん
08/01/01 17:40:00
グロタンのEGA/SGA嫁

184:デフォルトの名無しさん
08/01/01 17:41:40
知ってどしたいん？ん？

185:デフォルトの名無しさん
08/01/01 17:47:24
シミロンとは・・・

圏論による論理学―高階論理とトポス
清水義夫

URLﾘﾝｸ(www.amazon.co.jp)

186:デフォルトの名無しさん
08/01/01 18:09:02
>>182
シミロン読んでるんですが、高階論理をトポスに対応させて
いるところを Curry-Howard 同型と考えていいわけですか？

187:デフォルトの名無しさん
08/01/01 18:26:11
>>186
まあそうなんだけど、関数に対応するものがトポスの射になってる。

普通の集合論では、「はじめに一者あり」である。存在論的な形になっていて、その一者（実は、空）から、すべての存在が生成される。
では、Mac Lane が指摘した、論理学ではどうなるか。

ところが関数型の場合、「はじめに働きあり」である。なんじゃそりゃ、と思うかもしれない。
普通の集合論では、関数は、集合の一種（つまり、グラフ）として定義される。
でもこちらは、逆に、関数から集合を定義しようということなのだ。

この関数概念を一般化したのがシミロンのトポスの射。

188:デフォルトの名無しさん
08/01/01 18:31:40
Grothendieckは位相空間 X より X 上の層全体のなす圏(トポスになる) がより本質的だと考えた。
彼はこの考えを、エタールコホモロジーのアイデアとともに得た。

189:デフォルトの名無しさん
08/01/01 18:34:39
>>187
解説ありがとうございます。
ちょっと外出してきますのでまたのちほど。
すみませんです。

190:デフォルトの名無しさん
08/01/01 18:36:07
シミロンでやってるのはGrothendieckのオリジナルとは違って、
Kripke-Joyalの意味論での手続きによって集合論的論理式をトポスの対象と射についての言明として解釈したもの。

191:デフォルトの名無しさん
08/01/01 18:47:05
実数の体系の持つ超越的な性格は集合論の初期から様々な数学者の嫌悪の的となった。
実数を定めるのに便利な集合論的定式化はやがて多くの数学者に受け入れられるようになったが、
20世紀初めに論理学者のブラウワーは直観主義とよばれる、具体的に構成できるようなものだけを認める論理の体系をつくった。
彼はそこで実数について通常の数学におけるものとは著しく異なった結論を導きだせることを示した。
これにはKripke-Joyalの層の意味論によって現代的な解釈が与えられる。

シミロンのやってることを実行するとこんな風に実数の扱いなどがもっとブラウワー的に出来るようになります。

192:デフォルトの名無しさん
08/01/01 18:49:58
ただしCoqではKripke-Joyalの意味論は扱えないのでこのスレの趣旨からは外れますね。
つづきは数学板で質問してください。

193:デフォルトの名無しさん
08/01/01 19:10:59
λ式は、どのプログラマにとっても役立つ新たなツールです。最近ではVisual Basic 2008にも実装されました。

元々、Visual Basic 2008 (以前のコード名は "Orcas") にλ式が追加されたのは、LINQ (Language Integrated Queries) をサポートするためです。
これは、Visual Basic でのデータプログラミングを可能にするものです。

λ式を使用すると、プログラムの柔軟性が向上することがわかります。
λ式は、関数内で定義される呼び出し可能なエンティティであり、何の制約もなく利用でき、
したがって、λ式を関数から返したり他の関数に渡したりできるからです。

λ計算（lambda calculus）は、理論計算機科学や数理論理学における、関数の定義と実行を抽象化した計算体系であるλ算法とも言う。
関数を文字λ)を使った式によって表記する。アロンゾ・チャーチとスティーヴン・コール・クリーネによって1930年代に考案されたものです。
1936年にチャーチはλ計算を用いて一階述語論理の決定可能性問題を否定的に解いた。
λ計算は「計算可能な関数」とはなにかを定義するために用いられることもある。

λ計算は1つの変換規則（変数置換）と1つの関数定義規則のみを持つ、最小の（ユニバーサルな）プログラミング言語であるということもできる。
ここでいう「ユニバーサルな」とは、全ての計算可能な関数が表現でき正しく評価されるという意味である。
これは、λ計算がチューリングマシンと等価な数理モデルであることを意味している。
チューリングマシンがハードウェア的なモデル化であるのに対し、λ計算はよりソフトウェア的なアプローチをとっている。

λ計算は計算の意味論や型理論など、計算機科学のいろいろなところで使われており、特にLisp、ML、Haskellといった関数型プログラミング言語の理論的基盤として、
その誕生に大きな役割を果たしたが、とうとうVisual Basicにまで搭載されたことで、今後、その重要性は益々増大するだろう。

194:デフォルトの名無しさん
08/01/01 20:43:42
いま帰りました。
つまり、空集合から始まる現代集合論はもう
終わりの時代を迎えた、ということですか？
シミロンを読んでいて、ラムダ項もある種の
射に対応するのを知り目から鱗が落ちました。

195:デフォルトの名無しさん
08/01/01 21:53:13
>>192
そうですね。数学板にいきます。

196:デフォルトの名無しさん
08/01/02 22:55:53
Lisp ⇒ Common Lisp
Lisp ⇒ Scheme
Lisp ⇒ ML
┌――┘
↓
ML ⇒ Miranda ⇒ Haskell ⇒ Erlang
ML ⇒ Miranda ⇒ Clean ⇒ Concurrent Clean
ML ⇒ SML
ML ⇒ CAML ⇒ OCAML ⇒ （そろそろこないかなぁ？）

197:デフォルトの名無しさん
08/01/02 23:38:37
Erlangは違くない？

198:デフォルトの名無しさん
08/01/03 04:13:52
ついついOCamlという字面を見ると『岡村』って読んじゃう。
SMLをSmileって読んじゃうみたいに。でも頭の中はSMのことでいっぱい。
EclipseやElispをエロリスプとか。

199:デフォルトの名無しさん
08/01/03 14:03:05
>>196
Haskell→Erlangはおかしいでしょ

200:デフォルトの名無しさん
08/01/03 14:18:11
Clean ⇒ Concurrent Clean ⇒ Clean

201:デフォルトの名無しさん
08/01/03 23:11:56
OCamler ⇒ 岡村さん
SMLer ⇒ 須村さん
Schemer ⇒ 隙間さん

202:デフォルトの名無しさん
08/01/03 23:27:49
数学わかる人がいなくなると急にレベル下がっちゃうね。

203:デフォルトの名無しさん
08/01/04 01:21:28
Visual Basicやりたい放題なんだな。
VB.NET化であれだけ振り回した後だともう既存のユーザの移行コストとか考えないでいい空気なんだろうか。

204:デフォルトの名無しさん
08/01/04 10:14:36
別にラムダ式を入れるのに後方互換を犠牲にする必要はないだろ

205:デフォルトの名無しさん
08/01/04 17:31:47
COMつかい放題なのに文法が残念だからカオスでOK

206:デフォルトの名無しさん
08/01/04 22:50:49
VBはスレチだから置いとくとして、F#は何度かアップデートされたら化ける可能性はある。
OCAMLが完全に止まってるだけにちょっと気になる。

207:デフォルトの名無しさん
08/01/05 00:06:15
URLﾘﾝｸ(q-lang.sourceforge.net)
これなんか面白そう

208:デフォルトの名無しさん
08/01/05 00:25:51
>>207
Q言語って音響・映像に特化してるのかな？
これで作られた "Q+Faust+Pd" はかなり大規模な感じ。
関数型の特性を生かしてフィルターとかが多いみたいですね。

209:デフォルトの名無しさん
08/01/05 22:59:09
>>206
言語そのものの出来より、MSが力入れるかどうかだな。

210:デフォルトの名無しさん
08/01/06 01:19:39
>>209
現在のF#はfunctorが使えないからちょっとね。
でも今後のアップデートで何を追加するのかロードマップを示してくれると興味も湧くんだけどなぁ。
ＭＳが力を入れてくれると期待したい。

211:デフォルトの名無しさん
08/01/06 23:46:06
URLﾘﾝｸ(www.infoq.com)
ここ見た感じだと結構ちがう言語に見える
yield とかあるんだね

212:デフォルトの名無しさん
08/01/06 23:58:10
>>211
F#の記事ですね。
記者は手続き型でしか考えられない人かな？
forループ連発が意図的なのかよくわからなけど、あまり良い例じゃないなぁ。

213:デフォルトの名無しさん
08/01/07 00:15:51
この記事のforは全部F#独自のシーケンス内包表記でしょ。
書いた人もFoundations of F#の人だし。

214:デフォルトの名無しさん
08/01/07 00:26:33
>>213
for使うと再帰より速度が出るとか？

215:デフォルトの名無しさん
08/01/12 10:03:20
3.10.1でたね。プレステ3でビルドできるみたい？

216:デフォルトの名無しさん
08/01/12 18:38:12
>>215
何の？

217:デフォルトの名無しさん
08/01/13 02:37:14
URLﾘﾝｸ(caml.inria.fr)

The most recent version of Objective Caml is 3.10.1. It was released on 2008-01-11.

Some of the highlights in release 3.10 are:
* Instance variables in classes can be declared virtual and
implemented in subclasses. Syntax is val virtual v : t.
* Printing of stack backtraces on uncaught exceptions,
previously available only for bytecode-compiled programs,
is now supported for native-code programs as well.
(Supported on Intel/AMD and PPC, in 32 and 64 bits).
* New ports: MacOS X, PowerPC, 64 bits; Microsoft Windows 64 bits (x64)
using the Microsoft PSDK toolchain; Microsoft Windows 32 bits using the Visual Studio 2005 toolchain.
* The Camlp4 preprocessor was partially reimplemented and offers a new,
more modular API for syntax extensions.
(Users of third-party syntax extensions may wish to stay with OCaml 3.09 until these extensions are ported to the new API.)
* A new experimental tool, ocamlbuild:
a compilation manager that automates the building of OCaml applications and libraries. See the draft documentation.

218:デフォルトの名無しさん
08/01/13 21:53:45
流れをぶったぎっちゃうけれど、質問させてください
SML#のページにあるSMLFormatってcamlp4みたいなものなの？
説明見てもちょっと理解できなかったので…
サンプルも何か追加で入れないと動かないのもあるみたいなので使ったことある方とか居たら、どんなものか聞かせてください

219:デフォルトの名無しさん
08/01/13 22:32:40
使ったこと無いけど解説読むと普通のフォーマッタ／プリティプリンタじゃないかな。

220:デフォルトの名無しさん
08/01/16 21:14:36
F#版Parsec
URLﾘﾝｸ(www.quanttec.com)

F#版STM
URLﾘﾝｸ(cs.hubfs.net)

221:デフォルトの名無しさん
08/01/16 22:41:00
schemeのiotaみたいなのってocamlにないですかね

222:デフォルトの名無しさん
08/01/17 08:21:32
Arrayにはある。ListにはExtlibにある。

223:デフォルトの名無しさん
08/01/17 23:14:49
トン。

224:デフォルトの名無しさん
08/01/18 00:08:30
できたー。ライブラリインストールに手間取った；；
ExtList.List.init 100 ((+)1)；；
結構タイプ量おおいな；；

225:デフォルトの名無しさん
08/01/18 00:27:11
Extlibは基本open ExtListとかして使うものだよ。
ListまでをopenしないのはOCaml流だと思ってあきらめるしかないけど。

226:218
08/01/18 22:06:57
>219
遅くなってごめんなさい

ありがとう

227:デフォルトの名無しさん
08/01/21 20:16:22
>>225
遅くなったけど、ありがとう
ばっちり使わせてもらいます。

228:デフォルトの名無しさん
08/01/22 17:31:49
windows用のexeファイルを作りたいのですがどうすればいいですか？
VC++ expressインストールすればできますか？

229:デフォルトの名無しさん
08/01/23 08:10:53
同梱のドキュメントに書いてあるよ。

230:デフォルトの名無しさん
08/01/23 23:43:03
同じint -> int = <fun>なのに、RandomではException: Invalid_argument "Random.int"がでます
○ExtLib.List.init 10 ((+)1);;
×ExtLib.List.init 10 Random.int;;
説明では、Invalid_argが出るのは初期値(↑だと10)が負の時とあるけど、これってもしかしてバグ?

231:デフォルトの名無しさん
08/01/23 23:46:44
↑無視してくださいRandom.int 0がエラーでした。

232:デフォルトの名無しさん
08/01/24 23:02:51
次ｽﾚのタイトルを「関数型言語ML(SML, OCaml, F#, etc.), Part 6」として「【.NET】F#について語れ【OCAML】」ｽﾚを合流させれば過疎らなくて済むかねぇ。
ML系過疎り杉ｗ

233:デフォルトの名無しさん
08/01/24 23:03:20
たった今ハマりかけたのでちょっと書いとく。
Array.copyで新規作成されるのは一次元目の配列だけで、
二次元、三次元とかの値は前の値を差し続けてる。
まるごとコピーしたいときはその次元専用のcopyを作った方がいいみたい。

234:デフォルトの名無しさん
08/01/25 03:01:51
228じゃないけどうまくいかないや。
masm32もVC++も入れたしmasmのINCLUDE、LIB、PATHも通したのに。

一応Visual StudioのVCのPATH入れたり
masm32のbinにcl.exeやmspdb80.dll入れてみたりしたけど駄目だった。
う～ん、masmとVC++アンインストしようかしらw

235:デフォルトの名無しさん
08/01/26 00:34:24
エスパー能力を期待しないでくれよ

236:デフォルトの名無しさん
08/01/30 12:53:22
すみません，勉強し始めたばかりで，わからないことがあります．
指定した数だけランダムな数字を出力したいです．
やってみたところ再帰が止まらないです...
どうして＞．＜ｂ

# let rec print_random n =
if n = 0 then 2 else
begin
print_int (Random.int 2);
print_random n-1;
end;;

237:デフォルトの名無しさん
08/01/30 12:59:31
>print_random n-1;
これが(print_random n)-1;と解釈されるからだな
print_random (n-1);とすればよろし

238:sage
08/01/30 14:49:02
ocamlbuild はゴミ

あれで便利便利って言って喜んでる奴はまだロクなもん書いてない

さらなるゴミ p4 のビルドで必要なのがさらにゴミ
ゴミのおかげで make world の時間がもったいない

239:デフォルトの名無しさん
08/01/30 17:18:38
>>237
ありがとうございます～～～
少しずつ型チェックってなんのかわかってきました．いろいろ書いてみます！

let rec cntRandom n zeroCnt oneCnt=
if n = 0 then zeroCnt else
(
if ((Random.int 2) = 0) then
cntRandom (n-1) (zeroCnt+1) oneCnt else cntRandom (n-1) zeroCnt (oneCnt+1)
);;

240:デフォルトの名無しさん
08/02/02 21:00:52
token listを受け取って整形式XMLなら(string,string) xmlを返すxml_of_tokensを作れ、という問題に
3日ぐらい挑んでいるのですが、わかりません。誰か助けて。

type token = PCDATA of string | Open of string | Close of string;;
type ('a,'b) xml = XLf of 'b option | XBr of 'a * ('a,'b) xml list;;

入力：　[Open "a"; Open "b"; Close "b"; Open "c"; PCDATA "Hello"; Close "c"; Close "a"]
出力：　XBr ("a", [XBr ("b", []); XBr ("c", [XBr ("Hello", [])])])

入力の型と出力の型が違うのでわけわかりません
閉じタグとか考えてると、スコープが足りないです。
スコップをください。

241:デフォルトの名無しさん
08/02/03 00:21:39
>>240
全然深く考えてないけど，スタック使えばいいんじゃないの？

242:デフォルトの名無しさん
08/02/03 10:32:25
>>240
PCDATAはXLfでなくて良いのか？

exception ParseException of string
let rec parse (xs : token list) (context : string list) (ks : ('a,'b) xml list list) : ('a,'b) xml =
　let add_child ks x =
　　match ks with
　　| [] -> raise (ParseException "internal error: add_child")
　　| (k::ks1) -> (x::k)::ks1
　in
　match xs with
　| [] ->
　　if context <> [] then
　　　raise (ParseException ("some tags are not closed:" ^ (String.concat "," context)))
　　else
　　　hd (hd ks)
　| (PCDATA str)::xs1 ->
　　if context = [] then
　　　raise (ParseException ("toplevel PCDATA:" ^ str))
　　else
　　　parse xs1 context (add_child ks (XBr (str, [])))
　| (Open tag)::xs1 ->
　　parse xs1 (tag::context) ([]::ks)
　| (Close tag)::xs1 ->
　　if (hd context) <> tag then
　　　raise (ParseException ("close tag mismatch:" ^ tag ^ " appeared where " ^ (hd context) ^ " expected"))
　　else
　　　parse xs1 (tl context) (add_child (tl ks) (XBr (tag, (rev (hd ks)))))
let run_parse xs = parse xs [] [[]]

243:デフォルトの名無しさん
08/02/03 22:14:54
うおーありがとうございます！
(Open tag)::xs1の箇所で、ひとつ先読みする再帰になるのかと思って
ずっと考えてたけど、全然違った・・
あと、ご指摘のとおりPCDATAはXLfのほうが良さそうですね

上のadd_childみたいな関数が必要になるかどうかの判断って
自分には職人技の世界に思えるんですが
一般的なやり方みたいなのあるんですかね。

とりあえず、上記を参考に自分でも書けるよう頑張ってみます。

244:デフォルトの名無しさん
08/02/05 23:51:48
ねぇねぇ、OCamlでオブジェクトを使わないって人いる？
そういう人ってレコードを拡張したい時どうしているの？

245:デフォルトの名無しさん
08/02/06 00:19:05
OCamlのクラスって副作用ありますか？

246:デフォルトの名無しさん
08/02/06 00:54:00
副作用ありのオブジェクトも作れますし、なしのも作れますよ。

副作用あり
# class point = object
val mutable x : int = 0
method set_x v = x <- v
end;;
class point : object val mutable x : int method set_x : int -> unit end

副作用なし
# class point' = object
val x : int = 0
method set_x v = {< x = v >}
end;;
class point' : object ('a) val x : int method set_x : int -> 'a end

247:デフォルトの名無しさん
08/02/06 02:49:12
OCamlでlet _ = ... とlet () = ... 構文の違いがよくわかりません。
使い分けがあるのでしょうか？

248:デフォルトの名無しさん
08/02/06 21:32:35
let _ =... と let () =... とでは、使える状況が違う。
前者は名前の束縛を省略しただけで右式がどんな型になっても構わないけど、
後者は右式がunit型にならないとダメ。
どちらも print_string のような副作用が目的の式によく使うけど、
私は戻り値が要らないという意味で、let _ =...で統一している。
これだと let _ = Thread.create f () とかでも対応できる。

249:247
08/02/06 23:43:09
>>248
ありがとうございます。

# let () = true;;
Characters 9-13:
let () = true;;
^^^^
This expression has type bool but is here used with type unit

やってみたら確かにそうです。
悩んでいたのでとても参考になります。

250:デフォルトの名無しさん
08/02/07 10:23:25
俺は戻り値がunit じゃない状況を区別するために let () = を使ってる
let _ = は、 ignore @@ Unix.system "rm -rf hoge" とか

251:デフォルトの名無しさん
08/02/07 10:40:36
labelglutを使っていて
GluMat.gluPerspective ~fovy:(45.0) ~aspect:(1.0) ~zNear:(0.1) ~zFar:(100.0)
って書いてもUnbound value GluMat.gluPerspectiveって言われてちゃう

URLﾘﾝｸ(wwwfun.kurims.kyoto-u.ac.jp)
URLﾘﾝｸ(www.opengl.org)
を見て書いたのですがどこがいけないかわかりません＞．＜ｂ

252:デフォルトの名無しさん
08/02/07 23:12:43
>>251
まさかライブラリの指定を忘れてるなんて落ちはないよな。
ocamlc -I +lablGL lablgl.cma lablglut.cma ...
という感じでコンパイルしなきゃいけないはずだけど？

253:247
08/02/08 02:21:31
>>250
統一するか区別するかOCaml内のコードを調べてみます。
多いほうにしてみます。

254:デフォルトの名無しさん
08/02/08 09:33:48
>>252
大体原因がわかった
exampleにあった
GlMat.ortho ~x:(-1.0, 1.0) ~y:(-1.0, 1.0) ~z:(-1.0,1.0);
を調べてみたら
void glOrtho( GLdouble left,
GLdouble right,
GLdouble bottom,
GLdouble top,
GLdouble nearVal,
GLdouble farVal);
でなっていてGLの引数と違う名前になっていたのね

GluMat.perspective ~fovy:(45.0) ~aspect:(1.0) ~zNear:(0.1) ~zFar(100.0);
GluMat.perspective ~fovy:(45.0) ~aspect:(1.0) ~z(0.1, 100.0);
見たく試してみてもダメだったｗ

どっかに引数に関してマニュアルないわけ？

255:デフォルトの名無しさん
08/02/09 21:25:54
>> 254
.mli 見ろや:

val perspective : fovy:float -> aspect:float -> z:float * float -> unit

256:デフォルトの名無しさん
08/02/14 01:59:10
cygwin 3.10で実行しています。

while true do
　　print_string "debug1\n";
　　ignore (Unix.recv sock buf 0 (String.length buf) []);
　　print_string buf;
　　print_string "debug2\n";
done;;
を実行したのですが、
print_string "debug1\n";
が実行されず、プログラムが停止して、動きません。
コンパイル時にエラーはありませんでした。
何がいけないのでしょうか？

257:デフォルトの名無しさん
08/02/14 06:49:29
>>256
システムに関係なく print_string は buffering されているので
flush stdout が必要。

デバッグには stderr に出力 + flush の prerr_endline をおすすめする。
次の pervasives.mli のコメントをよく読んでくれ:

val print_string : string -> unit
(** Print a string on standard output. *)
val print_endline : string -> unit
(** Print a string, followed by a newline character, on
standard output and flush standard output. *)
val prerr_endline : string -> unit
(** Print a string, followed by a newline character on standard error
and flush standard error. *)

こういう細かいことって日本語の O'Caml の本には書いてないのかな?

258:デフォルトの名無しさん
08/02/14 20:34:46
>257
ありがとうございます。
prerr_endlineを使用したところ、うまく動作するようになりました。

次ページ