みんなのオブザイヤーオブザイヤーを募集中!今年のツイート今年のうちにまとめよう!

matzにも解るよう、禅問答的に #ATS2 の型理論を説明してみたよ

禅問答的に #ATS2 の型理論 "Applied Type System" を説明してみたよ (参考文献: 静的な意味論 http://jats-ug.metasepi.org/doc/ATS2/INT2PROGINATS/x235.html )
やってみた
11448view 16コメント
15
Q @masterq_mogumog
彼は型理論をまったく理解しようとしていないからな。。。 #matz
Yukihiro Matsumoto @yukihiro_matz
@masterq_mogumog 理解しようとはしたんですよ。型システム入門も読んだし。
Q @masterq_mogumog
@yukihiro_matz どうでした?あと最新の論文がります。是非一度で良いので目を通していただきたく。。。 Applied Type System / ats-lang.org/Papers.html#Ap…
Q @masterq_mogumog
@yukihiro_matz がんばって日本語訳もしてみました。。。 / github.com/jats-ug/transl…
Q @masterq_mogumog
@yukihiro_matz 型システム入門はあまりにも詳細すぎて、エッセンスが抽出されていないんじゃないかと思うんです。。。
Q @masterq_mogumog
@yukihiro_matz 是非この文書も一読していただけると、、、たいへん高階で哲学的な表現ですが、型とはなんなのかを短かく説明しています / 静的な意味論 jats-ug.metasepi.org/doc/ATS2/INT2P…
Q @masterq_mogumog
@yukihiro_matz 僕は未読なのですが、より詳細でわかりやすいそうです Dependent ML: An approach to practical programming with dependent types ats-lang.org/MYDATA/DML-jfp…
Q @masterq_mogumog
そうだね。 #ATS2 の型について聞かれたら、禅問答ができるように、うまい説明を準備しておいた方がいいんだろうな。そのためにもDependent ML=>ATSの詳細な型理論をちゃんと理解する必要がある。その上でエッセンスだけを比喩表現で説明できるようにならなきゃいけない
Q @masterq_mogumog
#ATS2 ではじめてプログラミングしたときの、わけがわからなさを軽減する方法は比喩表現による教育しかない。。。たぶん。
Q @masterq_mogumog
#意味 という単語が #ATS2 の型を理解する上で大変重要。 #意味 とはなんなのかを考えることが #ATS2 プログラミング
Q @masterq_mogumog
実世界には #意味 は存在しない。 #値 は存在する。 #意味 はその #値 を解釈する観測者の中に存在する
Q @masterq_mogumog
だから #型コンストラクタを呼ぶと #値 ができるというのは、順序がおかしい
Q @masterq_mogumog
そこで、 #値観測者が自分自身が思い描いた #型 をわりふる #AppiedType
h_sakurai @h_sakurai
@masterq_mogumog そうですね。 もっと良い入門記事はあると嬉しいと思います。 やさしいHaskellだけじゃあれですよねw
Q @masterq_mogumog
#値 の定義を思いだしてみよう。 #値 はいつでも変化する可能性がある。しかし、観測者は #値 がかわっても #意味 つまり #型変動してほしくないと願っている
Q @masterq_mogumog
つまり、観測者にとってモノは2つの部分からなりたっている。変化するものかわらないもの。前者が動的な部分、後者が静的な部分。この後者を #静的な意味 と呼び、これが #型 になる
Q @masterq_mogumog
もちろん観測者の願いは整合されないかもしれないかってに型をふっても世界の型はwell-typedになるわけがない
Q @masterq_mogumog
そこで、すべての型を観測者がわりあてたあとに #型推論 を行なう。このとき、世界のどの部分集合の値もかならず唯一一つだけ#意味 を持たなければならない。一つの #値 が2つの #意味 を持つことは許されない。それが世界の認識が間違っている。観測者の願いは整合していない
Q @masterq_mogumog
これが #ATS2 の見做す #型安全 ということになる。世界の部分集合には、それぞれ唯一の #静的な意味 つまり #型 が自動導出されなければならない。
Q @masterq_mogumog
これは、複雑な水道管の迷路と考えることもできる。水道管は水という #値 を通す。水道管は #静的 であり、けっして変化しない。そして一つの箇所に2つの水道管が同時に存在することはない。量子力学が適用されなければ。
Q @masterq_mogumog
、、、わかっていただけた、、、でしょうか。。。 #禅問答
Q @masterq_mogumog
この考え方のすばらしいところは、 #コンストラクタ という概念を型理論から排除できるところにある。値はそもそも存在する。すばらしい。
h_sakurai @h_sakurai
@masterq_mogumog その辺を、是非MLのアドベントカレンダーで書いてもらえれば良い気がw ううテレビみたいw
Q @masterq_mogumog
@h_sakurai あとでtogetterにまとめておきますー。てれびどぞー
残りを読む(154)

コメント

Q @masterq_mogumog 2014-12-03 02:10:34
まとめを更新しました。
人類を絶滅させる1000の方法 @tikal 2014-12-03 03:16:52
あー、これはさらなる解説として曼荼羅が書かれるパターンだ
Q @masterq_mogumog 2014-12-03 03:56:11
したたらずでしたか。。。 #orz
日比野 啓 (Kei Hibino) @khibino 2014-12-03 08:42:47
.@masterq_mogumog この禅問答を読んで、Haskell でもそっくりなプログラミングをやったことがあると私は思いました。 幽霊型を使った newtype を定義することで値に型をわりあてるとちょうどこうなるんじゃないかな。まあでも比喩だという話なのでズレがありそうですが。
虚無山ロボ @nida_001 2014-12-03 12:32:16
Applied Typingを動的型付け言語に乗っけるという話は,今主流(?)のGradual Typingと比してどういう得があるのだろうか
Q @masterq_mogumog 2014-12-04 13:00:40
まとめを更新しました。
Q @masterq_mogumog 2014-12-04 13:28:49
まとめを更新しました。
Q @masterq_mogumog 2014-12-04 21:15:01
まとめを更新しました。
Q @masterq_mogumog 2014-12-04 21:21:14
まとめを更新しました。
Q @masterq_mogumog 2014-12-06 18:04:59
まとめを更新しました。
Q @masterq_mogumog 2014-12-13 16:28:55
まとめを更新しました。
Q @masterq_mogumog 2014-12-14 17:45:57
matzからの返信をいろいろ追加しました。
Q @masterq_mogumog 2014-12-14 17:57:15
全ての発言を再度、デコレーションしました。
Q @masterq_mogumog 2014-12-15 00:34:53
koieさんとの議論を追加しました
Q @masterq_mogumog 2014-12-15 00:36:10
デコレーションしました
Q @masterq_mogumog 2014-12-16 23:25:07
タイトルを変えてバズりやすくしてみました
ログインして広告を非表示にする
ログインして広告を非表示にする