2015年8月30日

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

#ATS2 の作者Hongwei Xiの研究室に行ってきたよ
2
I moved to Mastodon. @masterq_mogumog

ちょっと時間があるからHongweiのコメントでもまとめよう。

2015-08-30 00:47:47
I moved to Mastodon. @masterq_mogumog

Xanaduは悪いアイデアだったのか?」「DML=>Xanadu=>ATSのようにコンパイラは成長した。Xanaduで採用したC言語文法は型表現に対して柔軟ではなかった」C言語文法の方がユーザフレンドリだけどしょうがないのかな cs.bu.edu/~hwxi/Xanadu/X…

2015-08-30 00:49:38
I moved to Mastodon. @masterq_mogumog

「読むべきソースコードのリストはあるか」「今はセッション型のコードがおすすめ。現状はErlangバックエンドに対する実装がある。C言語でも相当のC言語コードサポートを書けば使えるはず」 github.com/githwxi/ATS-Po…

2015-08-30 00:52:04
I moved to Mastodon. @masterq_mogumog

「セッション型の実装ではボイラープレート対策のために #codegen2 という新しいキーワードを使っている。これはHaskellのderiveのようなことができるが、テンプレートを使っているためその挙動を細かくユーザが調整できる」 github.com/githwxi/ATS-Po…

2015-08-30 00:54:34
I moved to Mastodon. @masterq_mogumog

「コーディングスタイルはどうしてあんななの?型シグニチャの宣言はあれでいいけど、インデントはつけてよ。日本のユーザにはフォーマッタ作る動きさえあるよ」「フォーマッタ作るのはいいね!」はぐらかされた。

2015-08-30 00:56:04
I moved to Mastodon. @masterq_mogumog

「将来的にC言語側でのエラーをATS側のエラーに持ち上げることは可能なのか。今のC言語側でのエラーはわかりずらい」「C言語側でのエラーをATS1のようにもっとわかりやすくすることは可能だと思う」

2015-08-30 00:57:30
I moved to Mastodon. @masterq_mogumog

「丁度良い証明コード量とは?多すぎると証明が大変。少ないとコードが危険」「Z3を使った自動証明が可能になるケースはあると思う。ただし、証明できなかったときに型エラーから判別するのは困難になるだろう」つまり半自動の証明作ってもパラダイスがひろがってる訳じゃないってことですね。。。

2015-08-30 00:59:15
I moved to Mastodon. @masterq_mogumog

「ATS1時代の思い出ある? ATSfloat scg.ece.ucsb.edu/ats.html とかあったけどあのユーザ層はどこいっちゃったの?」「ATSfloatは僕とは別に開発していた。最近はコンタクトがないね」やっぱりATS1=>ATS2の移行でかなりのユーザが消えたのでは

2015-08-30 01:01:30
I moved to Mastodon. @masterq_mogumog

「ATSに関する論文を出すならFlopsも良いのではないか。日本で開催するし」

2015-08-30 01:02:16
I moved to Mastodon. @masterq_mogumog

William Blairから。「Habitっていう組込Haskell実装があるよ hasp.cs.pdx.edu 」「ぼくの古いAVRなどの記事は blogs.bu.edu/wdblair/ から読めるよ」

2015-08-30 01:04:53
I moved to Mastodon. @masterq_mogumog

「セッション型は多数のホスト間でのプロトコルやメニーコア上のコードなどに有効。最近はAmazonがお金を出して研究している。君も parallella.org とかで #ATS2 のセッション型を使ったアプリケーション作ってみるのもいいんじゃない?」

2015-08-30 01:06:20
I moved to Mastodon. @masterq_mogumog

「ボストン大学でドイツの組み込みOS規格にのっとったOSを作っていて、その上で動くアプリケーションを #ATS2 で書くこころみをやってみたことがある。この時はOS実装そのものはC言語で書いた」

2015-08-30 01:09:54
I moved to Mastodon. @masterq_mogumog

証明コードを書くときは、あまり束縛名を上書きしない方が良い。型エラーがどの束縛に対するものなのかわかりにくくなる。」

2015-08-30 01:11:05
I moved to Mastodon. @masterq_mogumog

ミーハーだけど写真取った。左から Steinway Wu, Hongwei Xi, 僕, William Blair pic.twitter.com/TpWA3jaGgW

2015-08-30 01:14:37
拡大
I moved to Mastodon. @masterq_mogumog

Hongweiの研究室に行くには、この地図にしたがって歩いて、、、 pic.twitter.com/URY8KmJvHz

2015-08-30 01:15:53
拡大
I moved to Mastodon. @masterq_mogumog

ボストン大学でATS言語アプリケーションを作った際のドイツの組み込みOS規格のRTOSはOSEKだった。思い出した。 / OSEK - Wikipedia, the free encyclopedia en.wikipedia.org/wiki/OSEK

2015-09-28 21:47:07

コメント