また恥を省みず妄想を垂れ流してみる
えーと、すっかりtwitterの手軽さにやられてこっちの更新がさらにおろそかになっていますが、私のTL上で数週間前に流れていた話題から派生して悶々と妄想していたことを書き出してみます。そうするとまたkinabaさんとかが面白く解釈してくれるかもしれないので。箇条書きモード。
- なんかすでに誰かが言っているかもしれませんが、
- もし型が仕様ならば型のない言語というかプログラミングは実質的に存在しない*1
- だったら*2、型付言語と形無し言語という言い方はおかしくて、分類は以下のとおりになる
- そういうことはすでにkinabaさんがtweetしているような気がするが忘れたことにする
- プログラミングをほとんどしない、CSの知識もろくにない人間がこれを言う意味が少しはあるんじゃないかと思うのは、私が研究生活を送っている世界が(ZFC)集合論というほぼ究極に型がない世界であるということから。
- 型がないことの利点は確かにあって、例えばforcingをこれだけ縦横無尽に使いまくるときに、下手な型システムがあることは多分マイナスにしかならないだろう。多分だけど。
- でも、実際にはAとBが自然数からなる集合の時に、
なんて定義を平気でやる。Von Neumannの順序数を使っているならば、自然数そのものも自然数からなる集合なのだから、曖昧さが入るにもかかわらず。
- これが問題とされない理由は、読み手が人間型推論機としてそこそこの性能をもっていることを仮定しているからではないか。
- そこから考えるに、仕様を規定するための型が不必要だというのは、むしろそれを補充できるだけの型システムが人間の側にあるのだということになるんじゃないか
- えと、もちろんこの型というのがもともとの型という言葉からえらく離れているので違う言葉を当てるべきという意見には一理あると思う
- ただ、もともとの型の意味から始まった型チェッカなどが、新しい意味での型に関しても使えるのはすごいということは覚えておきたいわけで
- でもそのあたりで窮屈になるのは良くないから、やはりコンパイルは通すけどwarningは出すみたいな型チェックから行くのがベストのような気がする。
というところから始まって。
- いつだかのWhat/Howという言い方をするならば、Whatが型、Howがその要素になる
- だから、型推論はHowからWhatを導き出すこと、型から要素を作るのをなんというのかは知らないけれども、それはWhatからHowを導き出すことになる
- んで、いつぞやのカジュアル非決定性の話というのは、Howを書くときに対応するWhatの範囲を増やせるようにしようということになるのではないかと。
- これを一般化するとこうなるのではないか。
- この言語を使うならHowを書かないといけませんとか、この言語を使うならWhatを記述しないといけませんとか窮屈じゃないかと
- 「窮屈も何も、そうしないときちんとアルゴリズムを規定できないじゃないか」というかもしれませんが、どうせバグのないプログラムなんか実質的に存在していないんだから、厳密に規定しなくてもいいじゃん。
- 適当なWhatと適当なHowを書いて、食い違うところは適当にすり合わせて、なんとなく一人前になるとかいうプログラミングパラダイムが作れないかとか妄想。
- アスペルガー気味で指示をありのままに受け取ることが多い私が、臨機応変と状況判断を基本とする妻との共同作業で戸惑うことが多いのは、上にあるようなプログラミングパラダイムが私にないからなのだと思う
- そして、プログラミングができない人が数多くいるのならば、上にあるようなむしろ現実では普通な指示の出し方をプログラム言語上ではできないからだと思う
- 料理のレシピでは、例えば「5-6分または十分に煮えるまで」とか言うし。
- 家具の組み立てとかも、順番が変えられそうなところは変えるじゃん
- とか思った
- アウトプットしたので気が楽。もうこれ忘れる
- 発表の準備します。ごめんなさい。
