僕がML情報が集まる会が欲しくて開催しました。
@blackenedgold さん、@khibino さんにご協力頂きましてありがとうございました。
発表一覧
ATSで捕捉されたリアルタイムOSのシステム状態(masterq さん)
www.slideshare.net
リアルタイムOSのChibiOSの紹介とATS2の宣伝(?)
ChibiOSは内部的に状態を持っており、API関数を呼ぶときに普遍条件があるけども、
C言語から呼び出すとそれをキャプチャできないのでプログラムが危険になっていました。
それをATS2の依存型を用いて現在のOSのステートを型にエンコードして解決している話でした。
ステートを埋め込むだけならば幽霊型を用いてエンコードできそうですが、
線形型でステートを消費して次の状態に移る、みたいなのはATSじゃないと出来なさそうです。
Socket on SML#(Keen さん)
Socket on SML# | κeenのHappy Hacκing Blog
SML#からSocketのAPIとか叩く辛い話。 SocketのAPIをいい感じに設計するのは難しいのだなぁと感じました。 (完全に理解しているわけではないので深く説明できない……)
CとのFFIは辛いことだらけやで……。
socket の話をしていたと思ったら、いつの間にかメモリの話になっていた... #ML_study
— あっきー(慢性五月病) (@ackey_65535) July 9, 2016
ML-userのためのCoq入門(tmiya_ さん)
MLユーザ向けのCoqチュートリアル。
Coqでどういうことができるのか説明されていました。
アチラコチラにパワーワードが飛び出していました……!
「一個二個テストケースを満たしていることを確認するいい加減な開発ではなく」強い言葉だ… #ML_study
— コスモ (@cosmo__) July 9, 2016
tmiyaさん相変わらず絶妙につよいw #ML_Study
— ELD-R-ESH-2 (@eldesh) July 9, 2016
Coq は ML ユーザであればすぐ慣れる #ML_study
— あっきー(慢性五月病) (@ackey_65535) July 9, 2016
信用できる言語SML(fetburner さん)
正しく動くプログラムを書くのにコンパイラも検証されている必要があるので、
コンパイラの正当性が示されたCakeMLの紹介とその証明状況について。
色々パワーワードが飛び出して良さがありました
結論:SMLは信用できる
Sized Linear Algebra Packageのチュートリアル(@ackey_65535 さん)
www.slideshare.net
OCamlのライブラリSLAPの紹介。
線形代数の演算をやる上でベクトルや行列の大きさの整合性が取れてなくて
実行時エラーになったりよくわからないエラーが出て辛いのでそういうのを
静的に保証しながら演算できるBLASSとかLAPACKのラッパー。
生成的な幽霊型をうまいこと使っていているところがミソです。
型推論器と現実(インターネットの闇)
ml-study-typing/main.md at master · nomaddo/ml-study-typing · GitHub
型推論器の話。
理論的なあれこれから始まって、min_camlの破壊的代入を用いた
型推論アルゴリズムをなぞったのち、OCamlで実際に使われている
RemyさんのLevel-Basedな型推論アルゴリズムを紹介しました。
あとOCamlの中身をみて闇の深さを振りまきました。
着地点が不明と思ったけど闇の話だから当然だった (°_°) #ML_Study
— ELD-R-ESH-2 (@eldesh) 2016年7月9日
OCamlの型検査器の実装,思いのほか破壊的代入だらけ #ML_study
— gfn (@bd_gfngfn) 2016年7月9日
■■■■■■■■■ -MLが使えるML- (@bd_gfngfn さん)
www.slideshare.net
macrodownの紹介。他の発表は闇の話だらけでしたがMLの光の側面でした。
macrodownはマクロにocamlライクな文法を採用していてよりベターな
マークアップ言語で、それの機能紹介ややや実装が微妙な部分の紹介でした。
https://twitter.com/01expr/status/751696965520416768
— あおい@Python初心者 (@aoi1049) 2016年7月9日
#ML_study macro down 割と便利そうに見えるなぁ。ただこれで markdown を生成するのはどうだろう... どっちかというとHTML生成のテンプレート言語目的なのかな?
— Takashi Miyamoto (@tmiya_) 2016年7月9日
雑感
私の時間管理が甘くてご迷惑をお掛けしました。
もみあげさんも発表予定だったのですが時間が足りず発表できないことに……。
大変申し訳無いです。
わたしも喋りすぎてしまって、もっと厳密な時間管理が必要だなと感じました。
資料です https://t.co/mzk0YyttaZ #ml_study
— ナゲット・もみあげ (@pocketberserker) 2016年7月9日
どの発表も非常にレベルが高くて聞いていて面白かったです。
まるでSMLがメジャー言語かのように錯覚できる良い会でした。
懇親会は何を喋っていたのかよく思い出せないですが とにかく笑い転げていたような気がします。。。。
ろんださんの口からどんどん名言が湧いてくる懇親会であった
— gfn (@bd_gfngfn) 2016年7月9日
— インターネットの闇 (@no_maddo) 2016年7月9日
第二回を開催?できるといいなぁと思いました。
皆様お付き合い頂きありがとうございました。