Togetter/min.tを安心してお使い頂くためのガイドラインを公開しました。

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

禅問答的に #ATS2 の型理論 "Applied Type System" を説明してみたよ (参考文献: 静的な意味論 http://jats-ug.metasepi.org/doc/ATS2/INT2PROGINATS/x235.html )
17
I moved to Mastodon. @masterq_mogumog

彼は型理論をまったく理解しようとしていないからな。。。 #matz

2014-12-02 20:32:54
Yukihiro Matsumoto @yukihiro_matz

@masterq_mogumog 理解しようとはしたんですよ。型システム入門も読んだし。

2014-12-03 01:25:16
I moved to Mastodon. @masterq_mogumog

@yukihiro_matz どうでした?あと最新の論文がります。是非一度で良いので目を通していただきたく。。。 Applied Type System / ats-lang.org/Papers.html#Ap…

2014-12-03 01:26:14
I moved to Mastodon. @masterq_mogumog

@yukihiro_matz 型システム入門はあまりにも詳細すぎて、エッセンスが抽出されていないんじゃないかと思うんです。。。

2014-12-03 01:27:19
I moved to Mastodon. @masterq_mogumog

@yukihiro_matz 是非この文書も一読していただけると、、、たいへん高階で哲学的な表現ですが、型とはなんなのかを短かく説明しています / 静的な意味論 jats-ug.metasepi.org/doc/ATS2/INT2P…

2014-12-03 01:28:26
I moved to Mastodon. @masterq_mogumog

@yukihiro_matz 僕は未読なのですが、より詳細でわかりやすいそうです Dependent ML: An approach to practical programming with dependent types ats-lang.org/MYDATA/DML-jfp…

2014-12-03 01:32:18
I moved to Mastodon. @masterq_mogumog

そうだね。 #ATS2 の型について聞かれたら、禅問答ができるように、うまい説明を準備しておいた方がいいんだろうな。そのためにもDependent ML=>ATSの詳細な型理論をちゃんと理解する必要がある。その上でエッセンスだけを比喩表現で説明できるようにならなきゃいけない

2014-12-03 01:42:36
I moved to Mastodon. @masterq_mogumog

#ATS2 ではじめてプログラミングしたときの、わけがわからなさを軽減する方法は比喩表現による教育しかない。。。たぶん。

2014-12-03 01:43:26
I moved to Mastodon. @masterq_mogumog

#意味 という単語が #ATS2 の型を理解する上で大変重要。 #意味 とはなんなのかを考えることが #ATS2 プログラミング

2014-12-03 01:44:23
I moved to Mastodon. @masterq_mogumog

実世界には #意味 は存在しない。 #値 は存在する。 #意味 はその #値 を解釈する観測者の中に存在する

2014-12-03 01:45:43
I moved to Mastodon. @masterq_mogumog

だから #型コンストラクタを呼ぶと #値 ができるというのは、順序がおかしい

2014-12-03 01:46:06
I moved to Mastodon. @masterq_mogumog

そこで、 #値観測者が自分自身が思い描いた #型 をわりふる #AppiedType

2014-12-03 01:47:00
h_sakurai @h_sakurai

@masterq_mogumog そうですね。 もっと良い入門記事はあると嬉しいと思います。 やさしいHaskellだけじゃあれですよねw

2014-12-03 01:47:09
I moved to Mastodon. @masterq_mogumog

#値 の定義を思いだしてみよう。 #値 はいつでも変化する可能性がある。しかし、観測者は #値 がかわっても #意味 つまり #型変動してほしくないと願っている

2014-12-03 01:48:08
I moved to Mastodon. @masterq_mogumog

つまり、観測者にとってモノは2つの部分からなりたっている。変化するものかわらないもの。前者が動的な部分、後者が静的な部分。この後者を #静的な意味 と呼び、これが #型 になる

2014-12-03 01:49:09
I moved to Mastodon. @masterq_mogumog

もちろん観測者の願いは整合されないかもしれないかってに型をふっても世界の型はwell-typedになるわけがない

2014-12-03 01:49:37
I moved to Mastodon. @masterq_mogumog

そこで、すべての型を観測者がわりあてたあとに #型推論 を行なう。このとき、世界のどの部分集合の値もかならず唯一一つだけ#意味 を持たなければならない。一つの #値 が2つの #意味 を持つことは許されない。それが世界の認識が間違っている。観測者の願いは整合していない

2014-12-03 01:51:10
I moved to Mastodon. @masterq_mogumog

これが #ATS2 の見做す #型安全 ということになる。世界の部分集合には、それぞれ唯一の #静的な意味 つまり #型 が自動導出されなければならない。

2014-12-03 01:52:07
I moved to Mastodon. @masterq_mogumog

これは、複雑な水道管の迷路と考えることもできる。水道管は水という #値 を通す。水道管は #静的 であり、けっして変化しない。そして一つの箇所に2つの水道管が同時に存在することはない。量子力学が適用されなければ。

2014-12-03 01:53:26
I moved to Mastodon. @masterq_mogumog

、、、わかっていただけた、、、でしょうか。。。 #禅問答

2014-12-03 01:53:44
I moved to Mastodon. @masterq_mogumog

この考え方のすばらしいところは、 #コンストラクタ という概念を型理論から排除できるところにある。値はそもそも存在する。すばらしい。

2014-12-03 01:54:26
h_sakurai @h_sakurai

@masterq_mogumog その辺を、是非MLのアドベントカレンダーで書いてもらえれば良い気がw ううテレビみたいw

2014-12-03 01:54:28
I moved to Mastodon. @masterq_mogumog

@h_sakurai あとでtogetterにまとめておきますー。てれびどぞー

2014-12-03 01:54:53
残りを読む(154)

コメント

新型コロナ系VTuber 王冠ころな @tikal 2014年12月3日
あー、これはさらなる解説として曼荼羅が書かれるパターンだ
0
日比野 啓 (Kei Hibino) @khibino 2014年12月3日
.@masterq_mogumog この禅問答を読んで、Haskell でもそっくりなプログラミングをやったことがあると私は思いました。 幽霊型を使った newtype を定義することで値に型をわりあてるとちょうどこうなるんじゃないかな。まあでも比喩だという話なのでズレがありそうですが。
0
虚無クロニクル @nida_001 2014年12月3日
Applied Typingを動的型付け言語に乗っけるという話は,今主流(?)のGradual Typingと比してどういう得があるのだろうか
0
I moved to Mastodon. @masterq_mogumog 2014年12月14日
matzからの返信をいろいろ追加しました。
0
I moved to Mastodon. @masterq_mogumog 2014年12月14日
全ての発言を再度、デコレーションしました。
0
I moved to Mastodon. @masterq_mogumog 2014年12月15日
koieさんとの議論を追加しました
0
I moved to Mastodon. @masterq_mogumog 2014年12月16日
タイトルを変えてバズりやすくしてみました
1