型…きゅん??
http://twitter.com/ranha/status/3598749459
http://twitter.com/asm__/status/3598819573
http://twitter.com/m0h1can/status/3598890839
http://twitter.com/ranha/status/3599046158
http://twitter.com/ikegami__/status/3598831349
http://twitter.com/ranha/status/3599115276
http://twitter.com/ranha/status/3599164655
http://twitter.com/m0h1can/status/3599115357
http://twitter.com/m0h1can/status/3599238569
http://twitter.com/m0h1can/status/3599286928
http://twitter.com/m0h1can/status/3599297298
http://twitter.com/ranha/status/3599244158
http://twitter.com/ranha/status/3599258696
http://twitter.com/ranha/status/3599348816
http://twitter.com/ranha/status/3599373755
http://twitter.com/ranha/status/3599396533
http://twitter.com/ranha/status/3599457002
http://twitter.com/ikegami__/status/3598877012
http://twitter.com/alohakun/status/3600138039
http://twitter.com/alohakun/status/3600156447
http://twitter.com/alohakun/status/3600185237
http://twitter.com/ikegami__/status/3600201641
http://twitter.com/ikegami__/status/3600214738
uezato yuya
@ranha 初期の頃の、静的型付け言語っていうのは、何か理由があってそうなってたんだろうか。型チェックに基づく安全性とか、最適化とか、そういう事は考えられてなくて、自然と型っていう発想がただそこにあったんじゃないかなぁみたいな。うーん。50,60年前・・・?(2009-08-28 17:02:31) linkasm
@asm__ @ranha 型付けというより何バイト割り当てるか だったんじゃないかな C++からやたら厳しくなった理由は…なんかあった気がする(2009-08-28 17:09:45) linkIkegami Daisuke
@ikegami__ 確かに、型理論と論理学や圏論が合流したのは最近である(2009-08-28 17:10:53) link
@ikegami__ でも、型付き Lisp は 50 年前くらいからあるのかな?(2009-08-28 17:15:25) linkモヒカンではない
@m0h1can 最初ってビット幅が型で、まぁとりあえずデータ壊さない為の目印だった、とか勝手に思ってるんだけど、こんなテキトーな嘘かけば賢人が教えてくれるかなー(2009-08-28 17:16:51) link
@ranha 1958年、ALGOL 58とか想像しにくいぐらい昔で何が起こっていたんだろう。むしろ単に、区別を無くす、っていうような発想が無かったんじゃないだろうか。(2009-08-28 17:33:19) link
@ranha そういう事考えると、1960ぐらいのLispとかおめがヤバい感じが・・・。(2009-08-28 17:40:42) link
@m0h1can FORTRAN I(1954)の時点で型あったんじゃない？整数や小数点を区別したり、コンパイラだからか？(2009-08-28 17:40:43) link
@ranha FORTRANに型があるのは、なんか単純にアセンブリのインストラクションにあるのをそのまま持って来た感じかなーみたいな。浮動小数点命令セットとか、数値命令セットとか・・・。その区別を持ち上げると自然とああはならないのか。お分かりだろうか?分かりません。(2009-08-28 17:45:51) link
@m0h1can まともにデータ型区別するのは66以降ですね(2009-08-28 17:53:39) link
@ranha 「機械語とのセマンティクスギャップが少ない」「一般的には機械語やアセンブリ言語を指す。」絶望があった http://bit.ly/EFD6x(2009-08-28 17:54:16) link
@ranha ランタイムエラーとか起こされると資源的な意味で多分暴動が起きるので、そういう事を許さない為にチェックとかなって、チェックするのには型が使えるから型チェックみたいな・・・。(2009-08-28 17:55:48) link
@m0h1can ただ少くともラッセルの型みたいな抽象的な何かを導入する発想はコンピュータ以前に広まってたと思ったりしますね(2009-08-28 17:58:55) link
@m0h1can 型を明確に意識した最初の実装は何で誰だろ？(2009-08-28 18:00:01) link
@ranha 少なくとも、LCF MLの頃は、今で言う 型 をそれだと言っても問題は無い気がしていて、でもそれは70年最後、80年頭ですしその間になんか。simply typed λcalculusとか普通にどうなのかなぁ・・・。(2009-08-28 18:05:10) link
@ranha Simulaとかあの辺はジャストミートなのでは無いかとか思ったけど分かりません。型とかいうよりは、オブジェクトと、その関係とかなのかなぁ。でもそういうのは多分それだと思う。(2009-08-28 18:07:48) link
@ranha untyped λ-calculusから、typed λ-calculusにresearchが移ったなんかみたいなのは、全然知りませんけど、そうなのかなぁ。結局そこに在ったけど、見ていた/考えていたものが違えばそれは別なので、そういう事で見ると…?(2009-08-28 18:10:14) link
@ranha そもそも研究と、実用では、要請が違うんだろう。でも今は、それらが結びついているのだとすると、それは良い世界なのでは無いかとちょっと思います。元々意図していなくても、結局同じ事をやってればいつか繋がる時が来るんだろうか。(2009-08-28 18:16:38) linkザイロリック錠
@alohakun 型の発想って、群論とかそこらへんなんじゃないですかね。集合に対して許される演算の集合が規定される。(2009-08-28 19:28:09) link
@alohakun 望ましい性質を備えたプログラムの集合を定義しようと思うと、自然と型理論の発想に行き着く気がするけど。昔は、プログラムを動かすだけで精一杯だったから、プログラムの性質についての議論が深まるのは、少し時代が進んでからだと思う。(2009-08-28 19:30:04) link
@alohakun 計算機械や初期の言語にも、「型」そのものの概念はあったのだろうけど、まだ「理論」は無かったんだろうね。(2009-08-28 19:32:48) link
@ikegami__ 型付けされた言語の型は、群ほどきれいな構造を持ってないですよ。もっとしょうもない性質しかない。だから、圏論とか論理学に近い(2009-08-28 19:34:28) link
@ikegami__ 圏論や論理学がしょうもない、とは言ってません。圏論や論理学のしょうもない部分を型の理論の裏付けとして使ってる(2009-08-28 19:35:46) link
