type t (* void *)

関数型言語や英語学習の事とか。

OCaml: RWOを読み進めるためのOCaml設定

20150426加筆 RWOの説明を書いた
20150422加筆 より細かく書いた

20150909加筆 以下の内容はDebian 7向けに書かれており古いです! Debian 8ではより簡単にopamをインストール出来るようになっています! 下の記事では重複する部分は書きませんでしたが、インストール方法については下の記事が最新です。

no-maddojp.hatenablog.com

なんかちょっとだけOCaml環境構築が面倒みたいな話があったので、構築手順を書く。
大体確かめられた手順なのでよいはず。

Emacsのインストールまで解説しますが、RWOを読み始めるにあたりエディタの設定は必ずしも必要ではありません。
楽しんで下さい。

続きを読む

ML_Day#2を開催しました

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

今回もドワンゴさんのセミナー室をお借りしました。 この規模のセミナー室が便利に利用できるのは本当に助かります、巨大なITコミュニティに対する貢献や。。。

発表の紹介

発表枠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のパターンマッチがどういうふうに実装されているのかのサーベイの話でした。パターンマッチを実装する方法はだいたい3つあるそう。

  • 愚直な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でお会いできると嬉しいです。。。。

ocamlのctypesで.oをリンクする

昔はもっと面倒だったと思うのですが、いつの間にか動くようになっていました。OCaml 4.07, ctypes 0.11.5で確認。
ocamloptでは普通に.oをリンクするだけでctypesで作った関数が呼び出せる。
ocamlcではできない。

open Ctypes
open Foreign

let f = foreign "f" (void @-> returning int)

let _ =
  Format.printf "%d@." @@ f ()
int f ()
{
  return 100;
}
OCAMLC=ocamlfind ocamlc -package ctypes,ctypes.foreign
OCAMLOPT=ocamlfind ocamlopt -package ctypes,ctypes.foreign

test.x: lib.o main.cmx
        ${OCAMLOPT} -o $@ -linkpkg $^

test: lib.o main.cmo
        ${OCAMLC} -o $@ -linkpkg $^

clean:
        rm *.o *.cm? *.so

# 使ってない
lib.so: lib.o
        gcc -shared $^ -o $@

%.o: %.c
        gcc -c $<

%.cmo: %.ml
        ${OCAMLC} -c $<

%.cmx: %.ml
        ${OCAMLOPT} -c $<

OCamlのformat型の変な?型付け

ツイッターやらリアルで話しすぎてどこまで書いたかわからないけどformat型についてまとめておく。 言いたいことはほとんどこれだけ。

続きを読む

antlr4の生成するプログラムのインデントがおかしい気がする

追記:普通に解決方法があった。。。。。。。。

stackoverflow.com

つらい。最新版4.7.1で確認。

gist.github.com

antlr4は{}の中にアクションを記述することができるが、複数行になるときにインデントが考慮されていない気がする。 上のプログラムでDebugParser.py の34行目、インデントがおかしいので生成したプログラムを実行しようとするとインデントエラーになる。

昼間に起きてられるおくすり

最近睡眠外来にかかってまして、検査入院の結果特発性過眠症という診断をもらいました。 原因はよく分かってないけど、昼間の眠気が非常に強いというものみたいです。

特発性過眠症 - Wikipedia

昼間に2時間に一回入眠の早さを見る、みたいな検査を受けたのですが成人が横になって入眠するのに大体15分かかるところ、ワタシは1分未満でした。 まぁうすうすなんか異常なんだろうなと思っていたものに病名が付きました。

治療する方法はよく分かってないためないらしく、対処療法で薬を飲み続けることになりました。薬を飲みはじめて数日しか経ってないけど、世界が変わるようです。 朝昼でお薬を飲んでおくと、昼間全く眠くなりません。起きてられる世界素晴らしいです。

わたしは気付いたときには既に人の話を聞いていると起きてられず、12歳くらいから授業中居眠りするようになってました。 学部生のときはとてもひどくて、毎日4つ講義あるうち全く起きてられない日もあるくらいで、学部の成績はひどいものです。 人の話を聞くことが出来ないというのはとてつもないハンデで、単位取得した講義でも全く起きてられずに夜になんとか勉強してとったものもありました。

講演会で話を聞いていても最後まで起きてられたことはほぼなくて、学会に行ってもだいたいは居眠りしてしまう状態でした。 コンピュータを使う科目は手を動かすからか眠くなりにくく(それでもたまにPCの前で寝始めるんですが、、、)、まぁこの仕事でよかったと思っていました。 が眠くなければ他の道もあったのかもなぁみたいな気持ちになります。学部生の頃に眠気覚ます薬があれば。。。。。。

f:id:no_maddojp:20180803002711j:plain

というわけで眠いですがなんとか薬でやっていくぞ。

レジスタ割付けにグラフ彩色を使うの微妙だなという話

レジスタ割付け

コンパイラはコード生成の最後に変数(無限にレジスタがあると仮定したときの仮想レジスタ)を実際のレジスタに対応付ける、レジスタ割付けを行う。 この際には一般的にはグラフの彩色問題に帰着して解く事が多い。

彩色問題の色を使用レジスタに見立てて、何色で塗ることができるかというのを求め、それが実際のレジスタ数を超えていれば spill(メモリに退避)/fill(メモリから復帰)の処理を追加して仮装レジスタの生存区間を分割し、もう一度彩色を試みる。

疑問

  • コンパイルターゲットが分かっているわけだからNはもう分かっており、N色で塗れるかどうかを解くべきで、何色で塗ることができるのかという問題を解くのは変なのでは? これはRegister-Pressure-Aware schedulingの論文を読んで、これでこんなに性能が向上するのか、、、今まで何をしていたんだ感を感じました(@tanimocchi さん @khibino さんに感謝) Register pressure aware scheduling for high level synthesis - IEEE Conference Publication
  • CPUでしかうまく動かなくないですか?
    例えばVideoCore4というGPUでは自由に読み書きできるローカルメモリがないので、スピルを行うためにはCPU側のメモリにDMA転送でに書き戻さなければならないが、スタックポインタというものはない。アドレッシングモードでBase+Offsetを計算せずにいっぺんに行うLoad命令みたいなものがないので多数の演算が必要である。 更に書き戻す先のアドレスを保持する変数が生きている必要があり、Base+Offsetの計算のための演算命令を挿入する必要がありそのレジスタも要求するようになる。

    そうすると次はその命令をスケジューリングしたり、共通式の除去などの最適化を行いたくなるだろう。フェーズ間で影響を与え合いすぎてしまう。

    スピルをしやすいアーキテクチャでしかうまくいかないのでは?という疑問