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

型のヒントを言語に埋め込めないからオーバーロードとかは難しいのか

2014-12-03 11:39:12

二つ以上の意味を持てない、というのが対応してるのか

2014-12-03 11:42:16

ATS2 いじってみてえな。ATS (算法の方)ってのは依存型システムに、型レベルの計算と項レベルの計算の間に厳格な phase separation を導入したもので、staging と非常に強い関連がある。

2014-12-03 11:46:49

…という程度の認識だったんだけど、JavaScript にも自然に型放り込めるってー事は、汎用性に関して大分成熟してるらしい。

2014-12-03 11:47:44

ATS と似たような phase separation を導入している体系としては Concoqtion や Ωmega がある。作者の Xi, Taha, Sheard は全員一時期 OGI という今は亡き大学院にいた事があるので、多分同じようなマインドセットになったんだろう。

2014-12-03 11:50:06

@jun0inoue その時代をよく聞くのですが、まったくわからないです。。。

2014-12-03 11:55:45

@masterq_mogumog 分かりそうな人が TL にいてますね? (・д・)ｼﾞｰｯ @esumii @camloeba

2014-12-03 12:05:21

@jun0inoue @esumii @camloeba Hongweiのモチベーションはどこから湧いてくるのか興味があります。ぼくのモチベーションと同じなのか、それとも方向が違うなにかなのか。。。

2014-12-03 12:06:58

@jun0inoue @esumii @camloeba マジHongweiは殺戮マシンのように開発をしていて、ものすごい危機せまるものを感じるのです。。。

2014-12-03 12:07:48

@jun0inoue ほんと狂ってますよ。。。 #Hongwei

2014-12-03 12:24:51

@masterq_mogumog 話し変わりますけど、ATS ってリポ公開してます?

2014-12-03 12:30:42

@jun0inoue github.com/githwxi/ATS-Po… です。

2014-12-03 12:34:46

@jun0inoue 毎日5回ぐらいコンスタントにpushがあります。。。化け物。。。

2014-12-03 12:35:15

本家のページに掲載された "Zen(禅) Practice on ATS by Kiwamu Okabe at METASEPI DESIGN" / ats-lang.org/Community.html

2014-12-03 12:36:41

@masterq_mogumog あざっす。ヤバいですね。

2014-12-03 12:42:33

@jun0inoue なんかcommitで彼が起きたのがわかりますよ。

2014-12-03 12:42:56

日比野啓 (Kei Hibino) @khibino

@m2ym @masterq_mogumog 値に意味を後付けするのがまさに型付けなんじゃないかと考えています。私の HRR で幽霊型を使った SQL への型付けもそのようなアプローチです。

2014-12-03 13:07:06

m2ym @m2ym

@khibino @masterq_mogumog 論文を読んでいないので間違っていると思いますが、ポイントは、ATSでは矛盾なく意味を与えられるならプログラマの自由である、という考え方に基いていることだと思います。

2014-12-03 13:25:11

日比野啓 (Kei Hibino) @khibino

@m2ym @masterq_mogumog はい。幽霊型を使う場合でも、そのように型を設計できますよね。

2014-12-03 13:28:08

英語版を作った / Zen Practice on ATS · githwxi/ATS-Postiats Wiki github.com/githwxi/ATS-Po…

2014-12-03 13:28:31

EDSLのような言語内言語が欲しい人間としては値は複数の意味を持てないという制限が厳しいのでnewtypeみたいなものが欲しいといえば欲しい

2014-12-03 13:49:52

この禅問答に対してHongweiから採点メールが来ました #ATS2 / groups.google.com/forum/#!topic/…

2014-12-03 18:13:01

日比野啓 (Kei Hibino) @khibino

@jun0inoue その部分が分けられていることで、どのような違いがあるのかがいまいちしっくりきません。 staging というと、メタプログラミング的な操作を連想するのですが、それが関係してくるのでしょうか?

2014-12-03 21:47:05

@ruicc オーバーロードは可能です。ただし、文脈によって一つだけのインスタンスが導出される必要があります。2つのインスタンスが付くのは許されません。 / overload · githwxi/ATS-Postiats Wiki github.com/githwxi/ATS-Po…

2014-12-04 00:18:41