type t (* void *)

ソフトウエアのこととか

ML勉強会まとめ

僕がML情報が集まる会が欲しくて開催しました。
@blackenedgold さん、@khibino さんにご協力頂きましてありがとうございました。

connpass.com

発表一覧

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は辛いことだらけやで……。

ML-userのためのCoq入門(tmiya_ さん)

www.slideshare.net

MLユーザ向けのCoqチュートリアル
Coqでどういうことができるのか説明されていました。
アチラコチラにパワーワードが飛び出していました……!

信用できる言語SML(fetburner さん)

github.com

正しく動くプログラムを書くのにコンパイラも検証されている必要があるので、 コンパイラの正当性が示された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が使えるML- (@bd_gfngfn さん)

www.slideshare.net

macrodownの紹介。他の発表は闇の話だらけでしたがMLの光の側面でした。
macrodownはマクロにocamlライクな文法を採用していてよりベターな マークアップ言語で、それの機能紹介ややや実装が微妙な部分の紹介でした。

https://twitter.com/01expr/status/751696965520416768

雑感

私の時間管理が甘くてご迷惑をお掛けしました。
もみあげさんも発表予定だったのですが時間が足りず発表できないことに……。 大変申し訳無いです。
わたしも喋りすぎてしまって、もっと厳密な時間管理が必要だなと感じました。

どの発表も非常にレベルが高くて聞いていて面白かったです。
まるでSMLがメジャー言語かのように錯覚できる良い会でした。

懇親会は何を喋っていたのかよく思い出せないですが とにかく笑い転げていたような気がします。。。。

第二回を開催?できるといいなぁと思いました。
皆様お付き合い頂きありがとうございました。