私の発表が、私にも理解出来なかったので文章にしてみる
今回の私の発表は、
思考の道具としてのプログラミング
という観点から見ての
が未来に向かって持つべき何かを探る
というような事でした。あの発表からそんな事が考えられていたという事は、分かる筈もないです。私にも分からない。
発表では、問題をプログラミングによって解決する、という2フェイズに分けて考える所からはじめました。
フェイズ1
問題(コンテストのようなものを想像していただけると良いのですが、それに限った話では無い事に注意してください)が与えられた時に、
まず問題を理解する事からはじまります。
問題 - 何か1を経て → 問題の理解
何か1というのは、そもそも「読む」ような行為と、「読み手の持つ背景知識」など経験によるものから来る有効手の数の多さという武器「柔軟さ」というこれまた有効手を思いつく力強さ、などがあると思います。
余談ですが、私には少なくともこれら3つは欠損しています。
フェイズ2
問題の理解 - 何か2を経て → 実行者の分かる形に落とし込む。
自分の問題の理解に従って、どうすれば解を求める事が出来るかを「何らかのルール、手段、その2」によって書き落とします。
何か2というのは、プログラミングで、その手段としてのプログラミング言語だと思います。
通常プログラミングする、という時は、このフェイズ2の事では無いでしょうか。
すると、上の図(?)を書き直すと
問題の理解 - プログラミング -> 実行者の分かる形に落とし込む
という事になります。
繫げてみる
フェイズ1とフェイズ2を繫げてみると
問題 - 何か1を経て → 問題の理解 - プログラミングを経て → 実行者の分かる形に落とし込む (- コンパイル、インタプリトなど -> 実行結果)
という事になると思います。
しかしながら、通常こうは行かない筈です。
1.一発で問題を理解する事は出来ないので
2.考えを一歩一歩詰めて行く事で完全な理解を行う
ここで、理解の不十分さとしては「問題の意図の読み違い」「考えの浅さ」「複雑に考えすぎていた」があると思うのですが、私の経験上、それらがプログラミング言語に書き下す段階で判明することがあります。
そもそも、何故頭の中で考えていた事を実際に「書き下す。頭から抜き出して何かに落とし込む」ことで「自身でこれは正しいだろう」と思っていた事の誤りに気付けるのでしょうか。
まぁそれは知りません。
ただ、考えが及んでいなかった部分も「考えざるを得ない」という「不器用さ」がプログラミング言語にはあるからなのでは無いかと思います。
いわんや、あんまり人間ちゃんの考えているレベルではちゃんと考えられていないって事で、そうすると「ちゃんと書かなければならない」という不器用さは非常に重要だと思うのです。
この事は後半にも関わって来ます。
フェイズ図はどう書ける??
もう少し適当な形にフェイズ図を書くとすると
下のサイクル
ここで重要なのは「考えを明確にする」ステップで明確に出来る考えは１つである、という事だと思います。
プログラム が １つの考え/アルゴリズム に対応している必要は無くて、抽象の粒度は問いませんが、ともかくとして「明確に出来る考えは１つ」でしょう。
下のサイクルは、頭の中で考えたある発想をプログラミング言語として表現する過程で、
最初は頭の中でおぼろげで在った発想を、確実なものにしていく、
そしてその「確実なものにしていく」という過程で、発想の方向が徐々に固まってくるので、
その固まった部分を利用して自分の発想を見直す、見落としが無かったか考えるという事をやりつつ更に書き下して行く、そしてプログラミング言語として表される、という過程を表したものです。
簡単な問題というのは、最初から発想が朧げであるという事は無くて、具体的なキッチリした考えを即座に得る事が出来ます。
しかし簡単でない問題の場合は、どう攻め落とすかという考えは最初から明確にあるのではなく、「ある部分が幾つかある」のでは無いかと思います。
その部分たちを、取りあえずプログラミング言語として明確に表す。
するとそれがヒントになって、もう一歩先に進める事もあるのでは無いかなーと。
それと、頭の中で一度にごちゃごちゃと考えるのは大変なので、取りあえず分かっている部分でも書き出して上げる事で、その辺は棚上げして考えてあげる事が出来るので楽になるのでは無いでしょうか。
上のサイクル
ある１つの発想を得る事が出来れば、ソレを武器にして問題に立ち返る事で再び何かを得られる事があると思います。
このステップで新たに発想を勝ち得る事が出来れば、その新しい発想をプログラミング言語として表す事が出来るのでは無いかと思います。
残念なお知らせ
ここで「考えを明確にする」部分では「既存のプログラミング言語」を使う事が出来るのですが、
「何か1」は依然として「何か1」であって、より良い方法は無いのでしょうか・・・。
という事に関しては今回発表をしませんでした。
そもそも、この図はもうちょっと入り乱れた感じで、上のサイクルと下のサイクルはそこまでキッチリと区別はついていない気がします。が、モノを考える順番はあるんじゃないかなぁ・・・と。
考えを明確にする = プログラミング その手段としてのプログラミング言語
さて、「考えを明確にする」手段としてのプログラミング言語 であれば、頭の中でモノを考える時に持っているものになるべく「対応するモノ」を言語側が持っていると、「楽」で良いのでは無いかと思います。
そこで、実際の言語に欲しいものを考えてみると
構造を表すもの
これは、頭の中でモノを考える時に頼れるモノが、モノで、構造だと私は思っていて、そうすると構造を表すモノが欲しいです。
実際はどうなってる?
構造体、Class、代数的データ型(Algebraic Data Types,Variant)、抽象データ型(Abstract Data Types)
パターン、一括りんぐ、付随するパターンマッチ
何らかの意味で似たものは、何らかのものに纏められるべきなんじゃないかなーとか。あんまり区別を付けたくないケース。これは本当は居るかどうかは分かりません
構造それ自身をパターンとする、というよりは、構造を弄る側の操作から見てって感じですね。
頭の中に複数の構造がある時(あるかなぁ・・・)に、同じような事をやりたい時はまぁ多分なんか・・・。
実際はどうなってる?
Parametric Polymorphism
Subtyping Polymorphism(参照の何か)
Ad-hoc Polymorphism(Overloadingの何か)
これ型の話じゃんみたいな。
型はまぁ、在ります。私、型さんの事、好きです。
もじゅーる
これは会場でnihaさんが言ってくれたもので、
解決済みの問題はそれはそれで纏めておくもので、
関数とかも割とそうだと思うんですけど、そういう事も含めたニュアンスで、つまりパターンとしてもじゅーるに含めます
実際はどうなってる?
モジュール
一方欲しく無いものもあるでしょうよ
資源の管理とかあんまりしたくない
はあんまりやりたくないっていうか・・・。
勿論、問題そのものが資源管理系の問題ならばそれを考えないといけないのでそうですけど、
そういうケースじゃない時っていう感じですね。
実際はどうなってる?
Garbage Collectionとか
一回考えた事のあることは、考える事を省略したい。参照だけ付ければ良いじゃん
もじゅーるとはちょっと分けて考えて。
毎回0から必要な世界を構築するとかいうよりは、かつて自分がやった仕事を利用出来ると良いよねみたいな。
実際はどうなってる?
色々。まぁライブラリとか、パッケージとか。
仕事はやりたく無い
実際はどうなってる?
何も書かないでも勝手にプログラムが出て来たりはしないので、悲しい。
フォーマッティング
これも会場で出してもらったヤツです。
けどまぁ今考えると、うーん、構造を文字列っていうか、文字列じゃないですけど別なものに変える時って、
それは自明だから一々やらせてんじゃねーよタコみたいなそれはあるんじゃないかな。
割と文字列に限った話じゃなくて、同型の構造は勝手に変換出来るみたいな・・・。
実際はどうなってる?
頑張ってやるか、勝手によろしくやってくれる系なのはあんまり無いような・・・。
Haskellのshowとかはもしかしたらそうかも、で deriving Showを書くだけで基本は良いので。
ただまぁ、showした後にreadするのは自明じゃないらしくて、ガッデムってなる。
エラー処理
これはまぁ言う所があって、そもそも頭の中でエラーとかしたら死ぬんじゃないでしょうか?
実際はどうなってる?
エラーが出ると世界が死ぬ
素直にやるとすると、例外な気がしますけど、本当にそれで良いのかな。
欲しいもの達はどこで導入された?
割と情報が集まったものだけ
構造体は
本当のはじめの頃からは無かったけれども、少し経ってから出て来たんじゃ無いでしょうか。
まぁもうはじめ見たいなもんです。私生まれてないです。
型
http://ranha.tumblr.com/post/174924331
一番最初の頃は、「メモリ上のオブジェクトのサイズ」の為にあった気がして、それは今でいう所の「型」の意じゃないと思います。
そういう時の型っていうのは、「構造に意味付けする」「構造に名前を付けて区別する」とかそういう感じで、メモリ上のオブジェクトのサイズは・・・まぁ結局は言及する形になるんでしょうけど、考えてないですよ多分。
で、これはどの辺から入って来たのかは分からないんですけれども、ALGOLぐらいから何じゃないかなーと。
FORTRANの頃からあったかもしれませんけど、それはアセンブリのインストラクションに対応させるぐらいで思い切り機械に使われてる感じがします。
むしろ逆に、「型が無いってのはどれくらいからだ?」っていう話があって、それはLispからなんじゃないですかね。型無しλ計算は知りません。
「型モドキ」が在った頃に、そんな「型モドキ」は要らん的なLispさんは良いんじゃないかというのがあって、ただ何にせよ1950-59年ぐらいのLispはあまりにも型無しλ計算過ぎて意味分からないので、あんまりあてに成りません。
関係ある話としては、丁度スライドでこの辺の話をしている時(だったかなぁ)に、@todeskingさんから質問が在った気がして、
「人間が頭の中で考えている時は区別が付いていて、だったらプログラミングする時とか型書かなくて良いんじゃないでしょうか。」みたいな。
多分それは「構造の中身が分かってて、その操作が書ければおっけーおっけーみたいな」そしてそれは実際そうだと思います。けれども、それと型が無いっていうのは実は話が違うんじゃないでしょうかというのがあって。
むしろ、その役割を担ってくれるのが型ありきでの「型推論」なんじゃないかなーと思います。
まぁでもこれはちょっと分かりませんね。型が無くても良いんじゃないかってのは思います。
Structural SubtypingとかRecord Polymorphismとか多分それで良いんでしょうか皆さんとかいう時があって・・・。
ぽりもるふぃずむ
これはパターンの部分に関する話です。
多分型がある状況でのぽりもるふぃずむ的な話としては
ストレイチーの「Fundamental Concepts in Programming Languages http://www.springerlink.com/content/x878vn91l4763752/」ぐらいで、これが1966年ぐらいかも知れません。
Garbage Collection
http://www-formal.stanford.edu/jmc/recursive.html
とかは多分見た事ある人が居るかもしれないですけれども
Nothing happens until the program runs out of free storage. When a free register is wanted, and there is none left on the free-storage list, a reclamation cycle starts.
とかが書いています。
実装の中身は兎も角、この発想は驚異的で、こういう所を考えると、確かにLispは異常な気がします。
というのは半分で、脅威的なのはどちらかというと型無しλ計算です。
型無しλ計算のどこにも資源管理とか出て来ませんし、それ意外にも型無しλ計算は結構凄い。
まぁ余りにも計算の実行に注目したのでそういう所無く成ったんだと思いますけど、「注目したので無くなった」のであれば似た感じの話で大変面白いんじゃないかなーと。
欲しいもの達はどこで導入された? とか言って何がしたかったの?
頭の中でモノを考える時に色々やるソレが、言語側に登場したのは割と昔の話です。
実装に立ち入る事はしません。それはなんかやっちゃうとダメです。ダメ。それはさておく事にします。
上で挙げた欲しいものっていうのは「私」が「頭の中で考えている時はこんな感じ?」というのを列挙したもので、本当は「考えているけど」、「考えつく事が出来なくて」入っていないものがあるかもしれません。
ただそういうものがあるにせよ、多分そういう考えるという行為においてプリミティブそうな事は昔から入っているだろうし、「考えつく事が出来ない」ようなものはいつまで考えててもなんかどうしようも無いです。
とすると「既に欲しい機能は出揃っている?」という事になり、未来言語とかで人が集まってしまったんですけれども「(コンセプト的な意味では)もう未来未来したものは出てこない」んじゃないでしょうか?という問いをしました。
「出せて無いから未来が無いという事は言えない」という事は在りますけど、出せて無い事を出すなんていうのは悪魔の証明だと思いますし、ちょっと・・・。
そうするとやっぱり未来なんて・・・。未来なんて無いです。試合終了。
でももしかしたら・・・
未来があるとしたら、多分一々流れを書くんじゃなくて、性質、仕様、定義を書くだけであやふやーっと書くだけで「動いてくれる」ブツが出来ると良いとも思います。
動いてくれるブツっていうのは結局プログラムとか動かないとなんなんだって感じですので、動かないとダメです。
でも動くのを一々沢山書くのは辛い。そこで究極的に何も書きたく無い。
何も書きたく無いと言っても、問題提起とか、定義があります。そうしたらそれから勝手にプログラム作ってくれれば良いなーって事になるので、
そこで
とかが少しある気がして、現実はそんなに甘く無いです。
未来とか無くても良いじゃない
今は現実ですし、未来とか無くても、春香さんはかわいい。
これは本当に重要な話です。
落ち着いて考えれば春香さんはかわいいし、亜美さんはひぽぽたますぅ〜って言いますし、こういう現実を「もっと豊かに」楽しむ事が大事です。
現実を見ましょう。「既に面白いものが出揃っている」という仮定があるならば、それを利用すれば良くて、それで遊んであげれば良い。
未来言語はもう辞めて、良い言語っていうのを考える事にします。
良い言語っていうのは
- 堕落へ導く言語なんかじゃない
- 人間が成長する必要がある。人間が馬鹿だと言語が未来になるわけないでしょう。
- 豊かさは便利さじゃない。便利さはダメ。便利さは豊かさの代替には成らない。それは誤摩化しです。
- 便利さで卑屈なプログラムを書いて、まぁこれで良いかなーとなる。つまり、便利さで人間は死ぬ。
「本当にちゃんと考える」事としての定理証明
先にプログラミング言語は「不器用である」と述べました。
一々なんでも書かないと行けない。そこに苛々してしまう。
しかし、実はその苛々がダメ。徹底的にダメ。
中途半端に不器用なんじゃなくて、徹底的に「不器用な言語」で在って欲しい。
ここで次のようなプログラム(?)を考えます
add 0 b = b add (1 + a) = 1 + (add a b)
足し算を「こういう風に」定義したとしましょう。
次に
revCat : Array Nat length1 -> Array Nat length2 -> Array Nat (length1 + length2) revCat l1 l2 = concat l2 l1
revCatは、配列をひっくり返して結合するみたいな関数で、不器用な言語さんで書いていると仮定してください。
二つの配列を足した長さっていうのは Array Nat (length1 + length2)です。
ので、この関数は有効な気がするんですけど、ところがどっこい、そうじゃありません。うわーこの実例凄く貧相で面白く無い感じで申し訳無いです・・・。
なんでダメなのかって言われて、まぁその前にconcatがどうなってやがる！！って感じだと思うんですが
concat : Array Nat length1 -> Array Nat length2 -> Array Nat (length 1 + length2)
みたいな感じです。
更に具体的にどこが問題なのかというと、concatの定義により
revCat l1 l2 = concat l2 l1 -- Array Nat (length2 + length1)
て感じになります。すると何が起こるかというと、
Array Nat (length1 + length2)とArray Nat (length2 + length1)の単一化です。
更にいえば、length1 + length2 と length2 + length1の一致さが欲しい。で、ここまで長ったらしく書いててもう分かり分かりだと思うんですが、これは型チェックさんが死にます。
a + b が b + aであるという事は一言も言ってないんですけど、多くの言語さんだと、これはおっけーおっけーな感じに成ります。
それは何故か、簡単な話なんですけれども、値レベルの比較で言うと、というか、aとbの中身が決まっている時って、実際に計算出来るんですけれども、aとbの値が決まらないレベルではそれは無理です。
a + b = b + aという事は、全ての値に対して等しくなる事は全て調べれば分かるんですけれども、まず全て調べるとかがアレなので・・・まぁ。
じゃあどうすれば良いのかっていう話に関しては、a + b = b + aつまり_+_が可換である事を「証明」しなければ成りません。
「別に証明しなくても、実際に計算したら常に正しいっていう事が分かるから良いじゃん」
というそれは、それで正しいんですけれども、それは致命的な考えで計算が出来ると良いけれども計算している途中に宇宙が死ぬかもしれません。
それでその宇宙が死ぬのがその計算の所為だったりしたら、春香さんを見る事も出来ないので絶対に許せない。
従って、計算する前にそういう事を言えないといけません。
春香さんを見られなくなるという事もあるんですが、もう１つ問題点があります。
それは、上の_+_の定義を書いた時点では、a + b = b + aのような事が成り立つという「仮定」が在ります。
そしてその仮定は、ある意味では正しい(つまり実際に計算出来れば正しい)が、単純に「記号操作」という観点から見ると正しくは無い。
そして、今までのプログラミングの仕方では上のような問題は暗黙のうちに排除されていました。
だからまぁ、そういう、やってみれば分かる、みたいな事でやってるから彼女も出来ない。簡単です。もうちょっと考えて行動しよう。もうちょっと考えて行動出来てたら、まともなスライドが出来ました。まともなスライドが出来ないのは、今までのプログラミング言語の所為です。
単純に、明確な書き出しが、明確な理解を作る、という事だと思います。より正しい理解、深い理解に繋がる。
それは引いては使い手の成長に繋がると思いますし、今までの言語で中々出来なかった事だとすると、どうにもこうにも未来っぽくは見えませんが、良い言語だとは思います。
現状はでもそうでもない
簡単な問題の筈が、いざその証明を行うフェイズになると、意外にも困難で面倒臭くて長く成っちゃうって事はあると思います。
さすがにそこまではやりたく無くて、なんかこればっかり書いているんですけれども、QuickSortの停止性証明が凄く大変みたいな。
その辺は、皆さんがどんどん使って行くと定理証明系も良く成って行く(Agda2は多分ダメだと思っていて、私はCoqとIsabelle/*に移りたいです)と思うので、皆さんガンガン証明しましょう。
これわた
この発表は全体を通じて、プログラミングする事を2フェイズに分けて、そのフェイズ2における「何か2」、即ち「いわゆるプログラミングとその言語」として、定理証明系を使うということは全然悪い事では無い、という事を紹介しました。
面倒臭いので一文で書くと、今まであんまりやらなかった(ぼくも最近これで人生が楽しいです。定理証明をはじめて彼女が出来ません)ことが出来る系なので、楽しいと思います。
で、実は私はこういう発表がしたかったのでは在りません。
本当に発表したかったのは、未来の言語の話ですが、以下の話はいつかあたりに掘り下げて書けたら良いかなーと思います。
これわた1 人間の書く一切合切の情報を利用出来る言語/処理系
1.プログラムの構造を勝手に解析して、実は背後にはこんな事があるんじゃないかとか、他の所とこういう同型が見つかりましたとかそういう。
2.人間さんは名前を付ける時に、意味を付けて考えてると思う。ので、コード中に出現する名前を利用してもらう。ので、「名前」に意味さん何らかで付けられないかなーとか。
3.育成シミュレーション型 もしくは 恋愛アドベンチャー型で言語さんと処理系さんが成長していって、昔出来なかった事が出来たり、昔出来た事が出来なく成るとか。
これわた2 スタートゴール両方向からのプログラミング
1.割と多くの問題は、解決のスタートとゴールが見えてるので、その両方から埋めて行く事で真ん中も適当に埋まって行ってくれないかなーみたいな。
これわた3 「その1」で使える言語
1.実は今自分がどういう事を考えているか、とかいう事を何らかの方法で図示してくれたりする。
2.明らかにコンテスト系っぽい問題だけじゃなくて、単純に「ものを考える」という事を補助してくれるようなものが欲しい。
3.それがあると、未来の言語とかも考えるの楽に成ったりするんじゃないかなーとか。
