matzにも解るよう、禅問答的に #ATS2 の型理論を説明してみたよ
-
masterq_mogumog
- 15966
- 1
- 15
- 3
-
- いいね！3
I moved to Mastodon.
@masterq_mogumog
つまり、参照という概念はポインタを使って後付けで作ることができる。もちろんポインタは危険。ところが #ATS2 ではこのポインタを #線形型 を使って安全に操作できる。
2014-12-03 01:55:56
I moved to Mastodon.
@masterq_mogumog
#ATS2 は参照渡しという概念がない。つまりすべては値でしかない。値のサイズはある。しかしただそれだけ。値と値の関係は型によって作ればいい。つまりポインタと値の関係を #参照 と見做すこともできるし #線形型 のポインタである #駐観 と見做すこともできる。設計者の自由
2014-12-03 01:58:16
I moved to Mastodon.
@masterq_mogumog
つまり組み込みで値と値の関係が言語処理系に組込まれることはない。すべてはライブラリによって実現される。Hongweiがバグバグの処理系になりたくない、というのはこの #意味 を言語処理系内に持つのはゴメンだ、と言っているんだよ
2014-12-03 01:59:40
I moved to Mastodon.
@masterq_mogumog
で、Haskell脳もML脳もこの議論にはついてこれない。だからサーベイしてくれ。たのむよ。仕事してくれ。お前の専門なんだろ？
2014-12-03 02:00:22
I moved to Mastodon.
@masterq_mogumog
@yukihiro_matz いまこんなのも作ってみました / 禅問答的に #ATS2 の型理論を説明してみたよ - Togetterまとめ togetter.com/li/752948
2014-12-03 02:15:20
m2ym
@m2ym
これが本当にうまくいくなら既存の動的型付きプログラミング言語にとっても朗報なのでは / “禅問答的に #ATS2 の型理論を説明してみたよ - Togetterまとめ” htn.to/D75gnd
2014-12-03 03:10:30
I moved to Mastodon.
@masterq_mogumog
@m2ym あ、もうあります / code generation · githwxi/ATS-Postiats Wiki github.com/githwxi/ATS-Po…
2014-12-03 03:11:24
m2ym
@m2ym
@masterq_mogumog 正しく理解していない可能性がありますが、値に意味を後付けして型安全性を設計できるのなら、既存の言語、例えばRubyやPythonでも同様のことが出来るだろうと思ったわけです。リンク先のものはそういったものなのでしょうか。
2014-12-03 03:17:44
I moved to Mastodon.
@masterq_mogumog
@m2ym はいそうです。JSの意味論の上に #ATS2 の型をつけることができます。その対応はライブラリで行なうことができます / github.com/githwxi/ATS-Po…
2014-12-03 03:19:59
I moved to Mastodon.
@masterq_mogumog
@m2ym もちろんこんなチートっぽい技を使わなくても、LLの処理系の中にちゃんと組み込んで、まっとうな型をつける方法もあると思います。ただ、、、型検査も全部実装しなけばですが。。。
2014-12-03 03:23:51
I moved to Mastodon.
@masterq_mogumog
@m2ym ぼくもこれ以上の説明は困難です。詳しくは論文をとしか。。。 / github.com/jats-ug/transl…
2014-12-03 03:24:36
m2ym
@m2ym
@masterq_mogumog なるほど。なんとなく理解できたように思います。こういう表現が正しいかは分かりませんが、外延的に型を定められる、ということなのかなと思いました。
2014-12-03 03:27:06
櫻井洋志
@h_sakurai
参照はポインタってのはまぁそうだし、全て値っていうのが参照ってのもMLではそうだよなぁ。実行時に型を持ち込まないで、Cのプログラムを吐き出すだけだとか、線形型は、リソース管理出来ますよってことなので、mallocしてfreeを型が管理してうまく行くってことですよねぇ
2014-12-03 03:27:16
I moved to Mastodon.
@masterq_mogumog
@m2ym ぼくにはむしろむつかしくなりました。。。 #orz / 内包と外延 - Wikipedia ja.wikipedia.org/wiki/%E5%86%85…
2014-12-03 03:27:49
I moved to Mastodon.
@masterq_mogumog
@m2ym あーHongweiの説明にこんなのが "型を分類された値の集合のように扱います。 けれども、私は型を意味の形として扱う方がより適切であることを見つけました" / 静的な意味論 jats-ug.metasepi.org/doc/ATS2/INT2P…
2014-12-03 03:28:58
m2ym
@m2ym
@masterq_mogumog その言語の利用者からすると言語に組込まれていたほうが良さそうに思いますが、実装コスト的につらい気もします。誰かにやってもらうにしても、その人が理論を理解していないといけませんし。
2014-12-03 03:29:23
I moved to Mastodon.
@masterq_mogumog
@m2ym そこらへんはバランスだと思います。#ATS2 は全部外においだしていますが、これが良いバランスだとは、、、ちょっと思えません。よりよい言語デザイナが求められていると思います
2014-12-03 03:30:56
m2ym
@m2ym
@masterq_mogumog 内包・外延より、論理学的に理解したほうが間違いがない気がしてきました。命題の意味は解釈で決まる、というやつです。というか、まるきりそれと同じなので少し驚いています。
2014-12-03 03:34:08
I moved to Mastodon.
@masterq_mogumog
@m2ym というかそっち方面にうといので、むしろついていけなくなりました。。。 #orz
2014-12-03 03:35:06
I moved to Mastodon.
@masterq_mogumog
@m2ym もっとこのApplied Type Systemを応用した言語処理系が増えてほしいです。。。もっとさかんに研究されてほしいです。。。
2014-12-03 03:36:15