編集部が選ぶ「みんなに見てほしい」イチオシまとめはこちら

#ATS2 の作者Hongwei Xiの研究室に行ってきたよ

#ATS2 の作者Hongwei Xiの研究室に行ってきたよ
ネタ
1711view 1コメント
2
Q @masterq_mogumog
ちょっと時間があるからHongweiのコメントでもまとめよう。
Q @masterq_mogumog
Xanaduは悪いアイデアだったのか?」「DML=>Xanadu=>ATSのようにコンパイラは成長した。Xanaduで採用したC言語文法は型表現に対して柔軟ではなかった」C言語文法の方がユーザフレンドリだけどしょうがないのかな cs.bu.edu/~hwxi/Xanadu/X…
Q @masterq_mogumog
「読むべきソースコードのリストはあるか」「今はセッション型のコードがおすすめ。現状はErlangバックエンドに対する実装がある。C言語でも相当のC言語コードサポートを書けば使えるはず」 github.com/githwxi/ATS-Po…
Q @masterq_mogumog
「セッション型の実装ではボイラープレート対策のために #codegen2 という新しいキーワードを使っている。これはHaskellのderiveのようなことができるが、テンプレートを使っているためその挙動を細かくユーザが調整できる」 github.com/githwxi/ATS-Po…
Q @masterq_mogumog
「コーディングスタイルはどうしてあんななの?型シグニチャの宣言はあれでいいけど、インデントはつけてよ。日本のユーザにはフォーマッタ作る動きさえあるよ」「フォーマッタ作るのはいいね!」はぐらかされた。
Q @masterq_mogumog
「将来的にC言語側でのエラーをATS側のエラーに持ち上げることは可能なのか。今のC言語側でのエラーはわかりずらい」「C言語側でのエラーをATS1のようにもっとわかりやすくすることは可能だと思う」
Q @masterq_mogumog
「丁度良い証明コード量とは?多すぎると証明が大変。少ないとコードが危険」「Z3を使った自動証明が可能になるケースはあると思う。ただし、証明できなかったときに型エラーから判別するのは困難になるだろう」つまり半自動の証明作ってもパラダイスがひろがってる訳じゃないってことですね。。。
Q @masterq_mogumog
「ATS1時代の思い出ある? ATSfloat scg.ece.ucsb.edu/ats.html とかあったけどあのユーザ層はどこいっちゃったの?」「ATSfloatは僕とは別に開発していた。最近はコンタクトがないね」やっぱりATS1=>ATS2の移行でかなりのユーザが消えたのでは
Q @masterq_mogumog
「ATSに関する論文を出すならFlopsも良いのではないか。日本で開催するし」
Q @masterq_mogumog
William Blairから。「Habitっていう組込Haskell実装があるよ hasp.cs.pdx.edu 」「ぼくの古いAVRなどの記事は blogs.bu.edu/wdblair/ から読めるよ」
Q @masterq_mogumog
「セッション型は多数のホスト間でのプロトコルやメニーコア上のコードなどに有効。最近はAmazonがお金を出して研究している。君も parallella.org とかで #ATS2 のセッション型を使ったアプリケーション作ってみるのもいいんじゃない?」
Q @masterq_mogumog
「ボストン大学でドイツの組み込みOS規格にのっとったOSを作っていて、その上で動くアプリケーションを #ATS2 で書くこころみをやってみたことがある。この時はOS実装そのものはC言語で書いた」
Q @masterq_mogumog
証明コードを書くときは、あまり束縛名を上書きしない方が良い。型エラーがどの束縛に対するものなのかわかりにくくなる。」
Q @masterq_mogumog
ミーハーだけど写真取った。左から Steinway Wu, Hongwei Xi, 僕, William Blair pic.twitter.com/TpWA3jaGgW
 拡大
Q @masterq_mogumog
Hongweiの研究室に行くには、この地図にしたがって歩いて、、、 pic.twitter.com/URY8KmJvHz
 拡大
Q @masterq_mogumog
ボストン大学でATS言語アプリケーションを作った際のドイツの組み込みOS規格のRTOSはOSEKだった。思い出した。 / OSEK - Wikipedia, the free encyclopedia en.wikipedia.org/wiki/OSEK

コメント

Q @masterq_mogumog 2015-09-28 21:47:32
まとめを更新しました。
ログインして広告を非表示にする
ログインして広告を非表示にする