matzにも解るよう、禅問答的に #ATS2 の型理論を説明してみたよ
-
masterq_mogumog
- 15459
- 1
- 15
- 3
-
- いいね！3
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 がんばって日本語訳もしてみました。。。 / github.com/jats-ug/transl…
2014-12-03 01:26:44
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
そこで、 #値 に観測者が自分自身が思い描いた #型 をわりふる #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:54:26
h_sakurai
@h_sakurai
@masterq_mogumog その辺を、是非MLのアドベントカレンダーで書いてもらえれば良い気がw ううテレビみたいw
2014-12-03 01:54:28