type t (* void *)

ソフトウエアのこととか

ML_Day#2を開催しました

ML Day#2を開催しました。 ML勉強会という名前にしていたときから数えて通算4回目です。

今回もドワンゴさんのセミナー室をお借りしました。 この規模のセミナー室が便利に利用できるのは本当に助かります。

発表の紹介

発表枠6 + LT枠5のあわせて11もの発表がありました。発表者の皆様に感謝です。
他のコミュニティだと割と発表者の確保に苦労しておられるようですがML勉強会からあまり困ったことがありません。

以下の紹介は私の理解ですので何か訂正があったらツイとかで指摘ください。。。

ラベルなしオプション引数のための型システムと型推論

unlabeled-opt-args.pdf - Google ドライブ

最初はSATYSFIでお馴染みの@bd_gfngfnさんの発表でした。 この発表はSATYSFI向けに、オプション引数のための型システムと型推論を考えてみたという話でした。

Latexではラベルなしのオプション引数が多用されており、SATYSFIのために同じような仕組みが必要だと考えたようで、 OCamlにはラベル付きのオプション引数が実装されておりますが、これには少し扱いづらい性質があると考えているそうです。それは、

  1. 最後の引数をオプショナルにできない
  2. 型推論の完全性を満たさない 例えば let f g = (g ~foo:0 true, g false)

そのため、ラムダ計算に

  • ラベルなしのオプション引数をとるラムダ抽象
  • オプション引数の関数適用
  • オプション引数がないことを表す適用（！）

などを追加し意味論や型システムを考えたという内容でした。

この発表の中でReferしているOCamlのオプション引数の論文は[ Furuse & Garrigue 1995]ですが、 この著者の古瀬さんが来られておりちょっと緊張気味に喋っていたのが印象的でした。 古瀬さんの仕事は今回でちょくちょく触れられており、世界狭いなと思いました。。。

gfnさんの発表は典型的なアカデミックスタイルで、問題の発見・定式化の流れがすごくわかりやすかったです。 秋で修士を卒業されたようなのでスシを奢らなければ。。。

循環証明の話

ML-Day-#2.pdf - Google ドライブ

秋津 早苗 (@akitsu-sanae)さんの、証明の話です。

議論は循環証明とは何かということから始まりました。 循環証明とは、

構造的証明（普通の証明） + 循環 + 健全性のための条件`

であるとし、循環した証明を許すと導出の途中に出てきた判断式を再利用できて便利だけど、循環を無限に許すと明らかに間違っている判断式が証明できてしまうために、制約をつけるそうです。 健全性のために、「循環が無限回使われない」ために循環を無限回つかうと何かしらの無限効果列が構成できて、それが整礎であることを示すそうです。

帰納法と無限降下法は言っていることが同じだという説明をしていて、個人的にはそうだなというお気持ちになれました。

Inside Pattern Machings

Inside Pattern Matchings | κeenのHappy Hacκing Blog

きーんさんだよー。

MLのパターンマッチがどういうふうに実装されているのかのサーベイの話でした。パターンマッチを実装する方法はだいたい３つあるそう。

  • 愚直なIf分変換
  • 決定木をつくる
  • backtracking automata

そのうちバックトラッキングで実装する方法について解説していました。

進捗魔神の進捗を煽ってしまっいました。てへっ。

Dive into Algebraic Effects

びしょ～じょさんのAlgebraic Effectsの紹介です。Algebratic Effectsとは”継続を持てる例外”のようなもので、例外ハンドラの中みたいなものの中でperform (Say "Hello")というプログラムが発火すると、披露法はその周りの継続をひろえるようで、| effect (Say msg) k -> print msg; k() というふうにハンドラ部分が書けるようです。

これにより、定義と実装が分離されたりハンドラが合成できたりモジュラなプログラミングを支援してくれます。また限定継続が利用可能で、例外よりも強力です。 MultiCore OCamlやEffで実装されており、色々遊ぶことができそうです。

[https://twitter.com/yyu/status/1041205861945815042:embed]

OCamlのトップレベルあれそれ

www.slideshare.net

わたくしの発表。OCamlにはCompiler-libsという形でコンパイラの内部モジュールを外に出しているものがあり、それを使うとevalとかできるよという紹介でした。

モチベーションとしてはOwlを見ていると、彼らはかなりトップレベルを使っているようで、それもevalとinstall_printerやadd_directiveを組み合わせてやっていくすごいスタイルのプログラミングでびっくりしたというのがあります。 OCamlのトップレベルとか結構適当なインタプリタで実行されているというお気持ちだったのでびっくりしました。

Haskellで依存型とコンパイル時インラインlisp

あいやさんのHaskellで依存型使ったりコンパイル時にlisp起動したりするはなし。

このへんわたしがあまり詳しくなくてコメントできない。。。

仮想通貨デザインにおけるML言語族適用の展望

docs.google.com

OCamlハッカーのcamloebaさんの発表です！ わたしも卒論やM1の学会の際の節々でおせわになりました。

ワタシがTwitterで「MLは金にならんから勉強会が平和」みたいなことを言っていたらそれに反応して頂いたようで、「MLはカネになるぞ」という話からスタートしてオチが面白いのでぜひスライド見てください！！

仮想通貨はバグ即ウン億円の損失につながるようで、これから仮想通貨を安全にするための取り組みに参加されていくようです。

自作SML処理系の進捗

my-sml-compiler.pdf - Google ドライブ

mod_poppoさんの自作SML処理系の話。 人間には三大欲求があって「言語処理系」「エディタ」「OS」「CPU」があるよねー、どうせなら型推論のある実用的なコンパイラを書きたいですよね、というところから話ははじまります。

SML、はじめました | 雑記帳

SMLコンパイラはワタシも昔少し作っていたので気持ちになりました。　

OCamlによる無限グラフにも使える ダイクストラ法の実装

fetburnerさんのOCamlで競プロやっている実装のはなし。 ダイクストラ法を使うような問題はよく出題されるのでライブラリを書いたという話っぽいです。

パターンマッチ指向プログラミング言語Egisonとその上に実装された数式処理システム

Satoshi Egiさんの、Egisonというパターンマッチが強力なS式ライクな処理系の紹介です。

（紹介を書きますが私もわかってない感じがあるので注意して読んでください）

Egisonのパターンマッチについて解説し、パターンマッチ機能を用いて、どういうふうに 数式処理システムを言語上に実装していくのかという話でした。
パターンマッチの機能によって微分演算子の定義やテイラー展開の定義がシンボリックに・シンプルに記述できるという という話をしていたと思います。

Egisonのはなしは初めて聞いたので全くプログラミングパラダイムが違うので新鮮に感じられました。 最近は数式処理を簡潔に書きたという気持ちはすごくわかるので、触ってみようという気持ちになりました。。。

FSDN

もみあげさんのC#/F#のAPIサーチエンジンの話。
コンソール版を作った人の前でWEB版欲しいです！って脊髄反射で言ったら作って!!!って言われたので作ったそうです。

APIサーチエンジンの話に加えて、ボランティア活動なので楽にするためにDBは運用せずに 検索情報のキャッシュをgithub上にそのままreleaseにアップロードしてしまい、起動時にメモリ上に展開する、みたいな話をされていました。 OSS活動はボランティアですからね、、、楽していく気持ち、、、

懇親会の様子

全体の感想

私の感想は、レベル高いな！！ という感じでした。
gfnさんの発表から始まりましたが、まず欲しい型システムの性質を考えて定式化して各種の性質を示していくというスタイルが 当たり前だと認識できる集まりはなかなか無い気がします。 それ以外にも、MLがわかってその上で色々なことをやっていく発表ばかりで非常に楽しませていただきました。

ぜんぶの発表枠で質問も活発で、ほぼ質疑の時間を使い切るくらいの程度でした。
発表者だけではなくて、参加者全体のレベル高さが感じられました。

今後？

ML Day半年開催をなるべく守っていきたいです。
毎度毎度、会場の問題や発表者の確保の問題がありますが私の気力が続く限りは頑張っていきたいと思います。

まぁ運営も楽なんですよね、ML勉強会から特に何か問題になったことはないです。
わたしも運営と言ってもconpass立てるのと質疑応答の時間に走り回るくらいです。

レベルの高い発表が続くととても嬉しいのですが、初心者の方が入りづらくならないように気をつけないといけないと思いました。 本当はOCamlなどのML入門ハンズオンみたいなのもやってもいいと思っているのですが、体力が必要なので なかなか踏み出せていません。協力していただける方が複数いて、どこかの会社が後援とかしてくれたらやっていくかもしれない。。。。

しめ

発表者の方も勿論ですが、参加して頂いた方々本当にありがとうございました。
会場の確保に協力して頂いたドワンゴ様、@pocketburserkerさんにも大変感謝しております。
ML Dayは参加者の皆様もリテラシが高くてたいへん助かっております。
また半年後のML Dayでお会いできると嬉しいです。。。。