「集合」を明示的に値とするアプローチ [1] [2] だと、「同順の要素の並びはどちらでもいい」ソートアルゴリズムは、 全ての可能なソート順の集合を返すことになると思います。
-- msort_one xs = one_of (msort xs)
msort [] = {[]}
msort xs = let (ys,zs) = split xs in {merge xs' ys' | xs'∈msort xs, ys'∈msort ys}
where merge ys [] = {ys}
merge [] zs = {zs}
merge (y::ys) (z::zs) = if y<z then {y::ws | ws ∈ merge ys (z::zs)}
else if z<y then {z::ws | ws ∈ merge (y::ys) zs}
else {y::ws | ws ∈ merge ys (z::zs)} ∪ {z::ws | ws ∈ merge (y::ys) zs}
split xs = 略
これ、本当に非決定性が気になる最後の分岐以外でも全ての場面で集合を気にしなくてはいけなくて、 書くの面倒じゃないでしょうか。自分は、せめてこう書きたい：
x |?| y = if cointoss then x else y
msort [] = []
msort xs = let (ys,zs) = split xs in merge (msort xs) (msort ys)
where merge ys [] = ys
merge [] zs = zs
merge (y::ys) (z::zs) = if y<z then y :: merge ys (z::zs)
else if z<y then z :: merge (y::ys) zs
else (y :: merge ys (z::zs)) |?| (z :: merge (y::ys) zs)
split xs = 略
いや、これにも全く満足はできていないのですが。シングルトン集合 {e} はそのまま e、 内包表記による集合に一般化した関数適用もそのままただの関数適用、合併 ∪ は |?| になります。 一つだけを選び出す際の one_of は不要です。
空集合や、その他の集合演算（共通部分 ∩、可能な答え全部を取り出す all_of などなど…） を許すとバックトラック等が必要なヘビーウェイトな非決定性になってしまうので、 それは"この文脈では"おそらく考えるべきではないと思う。 （…というのが、もしかしたら私の主張の最大のポイント、ということになるのかもしれない。）
別の言い方をすると「++ と >>= と return だけを許す リストモナド にプログラム全体を閉じ込めてしまえ」という主張になります、たぶん。 扱う対象は、常に "複数の値を束ねた「集合」" です。 あまりにも当たり前に集合過ぎるのでソースコード上では見えないだけ。 Haskell で IO モナドから逃げられないのと同じで、このリストモナドからは逃げられません。 main :: List a に最後に one_of が（プログラムの世界の外から）適用されて実行が終わります。 「++ と >>= と return と one_of だけを許す」と制限することで、 (1) まず、仕様にあう処理系実装をゼロコストで実現するのは現時点でも非常に簡単 (2) さらに、何か画期的にわかりやすい構文で非決定性が表現できる気がしてならないのですが、 cointoss も |?| もなにか違うような、違和感がある、というのが現状です。
カジュアルのんでたーみにずむ。
配列の最大要素のインデックスを返す関数が欲しくなりました。
function where_is_the_max_element( arr ) { // 簡単のため arr.length > 0 と仮定
var max_i = 0
for(var i=1; i<arr.length; ++i)
if( arr[max_i] < arr[i] )
max_i = i
return max_i
}
普通の実装ですね。左から右に要素を見ていって、そこまでの最大値よりも大きい要素があったら更新。 結果としては、「最大要素のインデックスの内最左のもの」を返す関数の実装になっています。 さて今回はこれに疑義を呈したい。
今ある普通の言語の場合、「別に最左である必要はなくて、最大要素のインデックスならどれでもよかった」 という実装をすることができません。そういう実装ができる言語を考えるとどうだろう。たとえばこんなの
function where_is_the_max_element( arr ) {
var max_i = 0
for(var i=1; i<arr.length; ++i)
if( arr[max_i] < arr[i] || (arr[max_i]==arr[i] && cointoss) )
max_i = i
return max_i
}
cointoss （…という名前はちょっと誤解招きまくりですが）は、評価されるたび、 true か false かどっちでもいいけどどっちかになるプリミティブ。 処理系は、cointossを常にtrueとして実装してもいいし、常にfalseとして実装してもいいし、 乱数を使って確率1/2でtrueかfalseになる式として実装してもよい。 仕様では true か false のどちらかになることだけを保証。
メリットとしては、「最左でなくてどっちでもよかった」という意図をコードで語ることができる。
あとでコード読んだりリファクタリングしたりする人が、そこを変えていいのかよくないのかわかりやすくて便利です。
コメントでもいいんですけど、コメントじゃなくてコードで書けるならその方がベターだよね。
あと、もう一つのメリットとして、遠い将来ものすごく賢いコンパイラができたときに最適化の役に立つ。
たとえば、すごい解析の結果常にソート済み配列にだけ適用されることがわかっていれば、
後者の場合は print( where_is_the_max_element(sorted_arr) );
を処理系が全自動で print( sorted_arr.length-1 ); に最適化してしまっていい。
でも、前者ではどんなに賢いコンパイラでもそれは許されない。
別の例を出してみると、順番が同じ要素の並べ方はどの順でもいい時に stable sort
を書いてしまったら、どんな夢の超絶最適化コンパイラでもソートが unstable になる最適化はできなくなってしまう。
どの順番でもいいところは「どの順番でもいい」とコードで書いておけば、
100年後の凄いコンパイラはきっとそれをなんとかしてくれる、はず。
で、さて、問題なんですが、こういうことを実現する構文として cointoss
というプリミティブは我ながらちょっとわかりにくすぎる気がします。
他に、x か y のどっちでもいいけどどっちかを返す
x |?| yeither {...} or {...} という文を入れれば…などなど考えているんですが、
どれも、やっていることに比べて構文がややこしすぎるんですよね。なんというか、
上の「どれでもいいから最大値の場所」の例がまったくわかりやすくならない。
これが綺麗にわかりやすく書けるようなシンタックスは何かないだろうか…というのが今考えていることです。
どうなんでしょうね。
でした。
まず、ごめんなさい！録画してあとでupしようと思ってたんですが、 さっきたぶん操作間違えて録画したファイル全部消してしまいました。 もうだめだ…。 最初の方ずっと存在を忘れてて途中で開始したustreamのサーバ上録画はこちら： keigoiさんのの途中から途中まで / ちょっと飛んでその続きから最後の発表者まで。 水島さんとアキラさんの勇姿が失われてしまった…すみません。
発表資料リンク集：
自分の感想は…。 Scala の特殊化無いので型レベルVistorパターン（？）という解決の仕方は上手いなー、というのと、 やっと Functional Dependency 使うときの TypeCast の存在理由がわかったー！っていうのと、 いけがみさんのスライド素晴らしかったのと、 全体として似てる部分も似てない部分もあるけれど それぞれの言語で「型からその型を持つ値を無理矢理作る」ところは皆何か似通ってて面白かった （と同時に、なんか言語レベルでどうにか解決する方法があるんじゃないかなーという思いがよぎった）のと、 ある意味関連するのだけど、型レベルの構文で型レベル計算を書くのがわりとしんどいので、 式は実行時レベルの式で書いて、その式の裏で型レベル計算を走らせつつ最後に型だけいただく、 という書き方の工夫も面白いなーとか。
型レベルプログラミングの会：懇親会 のページ作りました。 人数確認しておきたいので、こっちも参加登録よろしくお願いします。＞各位
アスカをクリアした気分になったので、他のローグライク、ということで なんとなく 変愚蛮怒 をはじめてみました。 「このくらいレベルあれば大丈夫だろー」と未知のところに突撃してゲームオーバー、を繰り返しています。