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

I moved to Mastodon. @masterq_mogumog

@miura1729 そうだと思います。Rubyのようなやわらかい対象物に型を付けるのにも使える技術だと思います。是非

Miura Hideki @miura1729

@masterq_mogumog Rubyで型推論をしたい理由が高速化のためなので、この意味ベースで行った型付けから、メモリレイアウトなどの構造に関する情報が得られるかが最大の問題の気がします。行き詰っていたのでブレークスルーになりそうな気がします。ありがとうございます

I moved to Mastodon. @masterq_mogumog

@miura1729 いえいえ。こちらこそです。数年前にRubyの型推論の発表を聞いてからずっとその後が気になっていました。。。ぼくも今Rubyを仕事で使っているので、是非がんばってください！！！ _o_

Miura Hideki @miura1729

@masterq_mogumog ありがとうございます。今はmrubyをJITコンパイルをできるよう改造しています。やはり静的に型を決めてガードを無くさないと速度が頭打ちになるので、型推論を考えています。今度は推論器を独立して設けようと考えています。

Jun Inoue @jun0inoue

@masterq_mogumog @khibino drive.google.com/open?id=0B09qk… 書きました。okular で開けて下さい。取り消し線の一部を除いて、どの注釈にも理由付けか詳細が書いてあるのでカーソル合わせて読んで下さい。

I moved to Mastodon. @masterq_mogumog

というかokularにこんな添削機能があるって知らなかった。。。

I moved to Mastodon. @masterq_mogumog

とりまチケットを切った / ATS-types03-ja.pdfの添削結果をmergeする · Issue #10 · jats-ug/translate github.com/jats-ug/transl…

Jun Inoue @jun0inoue

@masterq_mogumog 注釈の意味がわからないところが有ったら遠慮なく聞いて下さい。

I moved to Mastodon. @masterq_mogumog

@jun0inoue はい。ありがとうございます。大変丁寧なレビュー助かりました。用語から不安だったので、、、年内には必ずmergeしたいと思います。

I moved to Mastodon. @masterq_mogumog

#matz にも解る #ATS2 言語入門

Yukihiro Matz @yukihiro_matz

@masterq_mogumog 欲しいですねえ。紹介してもらった文書は読みましたが、よくわかりませんでした。多分背景となる基礎知識が足りない。

I moved to Mastodon. @masterq_mogumog

@yukihiro_matz うう。。。ぼくの説明不足です。。。 #orz

I moved to Mastodon. @masterq_mogumog

@yukihiro_matz 僕がOCamlを学ぶとき、この本が役に立ったので、同じ章構成で #ATS2 の解説をしてみようと思います。来年いっぱい時間をいただきたく。。。 / プログラミングの基礎 amazon.co.jp/%E3%83%97%E3%8…

Yukihiro Matz @yukihiro_matz

@masterq_mogumog どう考えても私の無知と能力不足が原因ですからご自分を責めないでください。

I moved to Mastodon. @masterq_mogumog

@yukihiro_matz いえ。まつものさんの持つ言語感覚が、この分野に圧倒的に不足していると考えるからの発言でした。学者は良い言語を作るのですが、その見た目はML同等で良いと考えるふしがあります。良い言語デザイナが不在です.. github.com/githwxi/ATS-Po…

Yukihiro Matz @yukihiro_matz

@masterq_mogumog 頭のいい人は難しいと思う前にわかっちゃいますからね。言語デザインにも庶民感覚重要ですね。

I moved to Mastodon. @masterq_mogumog

@yukihiro_matz "常識の活用" という言葉の意味を再認識しています。。。

鯉江 @koie

@masterq_mogumog ふとアートは意味が先にあって形を作るかなとおもった。

I moved to Mastodon. @masterq_mogumog

@koie ぉぉ。つまり人間の内なるものが形を成すこともあるんですね。 #数学における発見 も意味が先にあって、それが数式として具現化するのかもしれませんね。。。

I moved to Mastodon. @masterq_mogumog

#設計 もそうかもね。人間の中に意味があり、それを物理にコンストラクトする。

鯉江 @koie

@masterq_mogumog 物理学でも保存則は先にあるよなあとか。

I moved to Mastodon. @masterq_mogumog

@koie 物理は逆じゃないでしょうか。。。物理現象はもう値として存在しています。物理法則は人間の心の中の意味としてしか存在しないうたかたのものなのではないでしょうか。統一理論が存在する、というのは人間の願望にすぎません。。。

I moved to Mastodon. @masterq_mogumog

保存則はじつはないかもしれないですしね。。。

鯉江 @koie

@masterq_mogumog もし保存則がなければ宇宙は死産してたと思うんだな。

I moved to Mastodon. @masterq_mogumog

@koie それはぼくらの宇宙が死産していたかも、ってことですよね。おそらくほとんどの宇宙は死産なんだ、とこないだ教えてもらいました。 #息子から