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

櫻井洋志 @h_sakurai

変数aはintならint以外に変わってもらっては困るってのは、静的型付ける場合は当たり前だよなとか。場合に寄っては型を変えたい事もあるので、そこは明示してあればいいのだけど、同じにしろってunsafeとか書かされると嫌なのだわなぁ。

I moved to Mastodon. @masterq_mogumog

@m2ym とにかくこの作者、Hongweiはおそろしく論理的な人間です。論文をおすすめします ats-lang.org/Papers.html cs.bu.edu/~hwxi/academic…

m2ym @m2ym

@masterq_mogumog すみません。例えば命題の「意味」を何ぞや、と言ったときに、論理学的な一つの答えは、意味とは命題集合のべき集合から真理値への関数だ、というのがあるのです。つまり意味というものは最初からあるのではなく、後から決めるものだ、ということです。

I moved to Mastodon. @masterq_mogumog

@m2ym それって、物理学的にもそうだと思うんです。意味は人間の心の中にしかなくって

m2ym @m2ym

@masterq_mogumog これがそのまま、型（意味）がまずあって、次にコンストラクタ（命題）がある、という不自然な順序を否定する根拠になると思うのです。

I moved to Mastodon. @masterq_mogumog

@m2ym nなるほど。。。

I moved to Mastodon. @masterq_mogumog

@m2ym 不自然ですね

m2ym @m2ym

意味が一つに割り当てられるというのは、矛盾のないモデルを見つけられる、というふうに解釈できそう。そうするとここで言う型推論は証明の探索にもっと近くなるのではないかな

I moved to Mastodon. @masterq_mogumog

@m2ym その通りです。ソルバを使っていて、内部ソルバと外部ソルバがあります。外部ソルバにはz3を使うこともできます / github.com/githwxi/ATS-Po…

I moved to Mastodon. @masterq_mogumog

@m2ym つまりソルバを強力にすればするほど、豊かな静的な意味を使うことができるようになります。今の #ATS2 は線形計算しか許しませんが、z3を使えばもっといろいろできるはずです

m2ym @m2ym

@masterq_mogumog そこはあまり心配しなくても良いと思います。なかなか興味深いアイデアですし、哲学的・論理学的にも面白いと思います。おまけに実用可能性があると来れば、何も問題ないのではないでしょうか。

I moved to Mastodon. @masterq_mogumog

@m2ym うーん、研究者はぜんぜんサーベイしてないですね。はっきりいってやくたたずです。。。ICFPレベルだと

I moved to Mastodon. @masterq_mogumog

@m2ym #Oleg もサーベイしてません #ATS2

I moved to Mastodon. @masterq_mogumog

@m2ym sそうですね。すごく #ATS2 のドキュメントを読んでいると哲学的なものを感じます。世界の見え方がかわるといいますか。。。 / ATSプログラミング入門 jats-ug.metasepi.org/doc/ATS2/INT2P…

櫻井洋志 @h_sakurai

寝ようと思いつつ、RubyとかにもATSみたいなので型を外から付けてやることもできるぜって事もあるんだなっと思ったりして

m2ym @m2ym

@masterq_mogumog ホスト言語の意味論をあまり気にせず論理のレベルでヒャッハーできるのは個人的にすごく面白いと思います。というかこれ論文生産マシンになり得ますよ。たとえば様相論理を入れてみました、みたいな（安直な）拡張が考えられますよね

I moved to Mastodon. @masterq_mogumog

@m2ym 様相論理、、、がわからないでゲソ。。。 #orz 様相論理 - Wikipedia ja.wikipedia.org/wiki/%E6%A7%98…

I moved to Mastodon. @masterq_mogumog

@m2ym あーでも、いろいろな論理体系をつっこめるメリットがあると思います。静的な意味なのでやりたい砲台なんですよ。今は線形型と依存型がありますが、数学の他の論理体系を比較的容易に実装できると思います。制約をつけて、解くだけなので

m2ym @m2ym

@masterq_mogumog 単に他の研究で忙しいだけではないでしょうか。本当に良いアイデアであれば研究してくれるように思います。誰もが世界の発展を望んでいるはずですので。

m2ym @m2ym

@masterq_mogumog そうですね。研究のネタになるかどうかで言えば理想的な環境な気がします。

櫻井洋志 @h_sakurai

Cのレベルだと、そういう事も多々あるわけで。ビットで型変わるとか諸々扱えると嬉しい。チャンクの値がいくつだと、その後ろのデータがどうとか、結構ごちゃ混ぜな事もあるし。面白いなぁw

m2ym @m2ym

いつから型があって次にコンストラクタがある、という考え方になったのかを考えるとちょっと面白いかもしれない

m2ym @m2ym

そういう風に作ったほうが理論的にも実装的にも楽だった、という面が大きそう。実際それだけでも十分うまみがあったのだろう

日比野 啓 (Kei Hibino) @khibino

.@masterq_mogumog この禅問答を読んで、Haskell でもそっくりなプログラミングをやったことがあると私は思いました。 幽霊型を使った newtype を定義することで値に型をわり.. togetter.com/li/752948#c169…

I moved to Mastodon. @masterq_mogumog

@khibino 幽霊型がまだよくわかっていません。。。 #ATS2 ではたぶん幽霊型を使うケースはかなりマレではないかと思っています。