2016-12-19

NGK2016B で Kubernetes + Alloy について話してきました

先日、毎年恒例のなごや LT 大会 NGK2016B / 名古屋合同懇親会 2016 忘年会で発表してきました。

机上の Kubernetes - 形式手法で見るコンテナオーケストレーション #NGK2016B from y_taka_23

www.slideshare.net

当日の動画は NGK 2016B LT #2 - YouTube から見ることができます。

ちなみに NGK での発表は 4 年連続 4 回目です。今回も含めてすべてモデル検査が題材になっています。

NGK2013B : Alloy ではじめる簡単モデル検査
NGK2014B : 猫でもわかる！モデル検査器 SPIN 入門 (ブログ記事)
NGK2015B : AWS は形式手法の夢を見るか？ - モデル検査器 Alloy によるインフラ設計 (ブログ記事)

Kubernetes に関わる役者たち

さすがに 5 分に詰め込むにはハイコンテクストすぎました。いろいろな登場人物が出てくる上に図でしか説明していない部分もあるため、後からスライドだけ見て最低限の意味が取れるように補足しておきます。

Master/Node

Master がいわゆるコントロール用のサーバ (群) であり、その下に実際にコンテナが載る Node がぶら下がる形になっています。

なぜか Kubernetes のバージョンによってしばしば呼び名が変わっていて、過去には Master/Minion とか、Master Node/Worker Node とか呼ばれていたりしました。

Pod

Kubernetes がコンテナを管理する単位で、1 個以上のコンテナからなります。スライド中では破線で囲まれた「A」と「B」のペアが Pod です。

同じ Pod に属するコンテナ同士は常にひとまとまりになって同じノードにデプロイされます。例えば、アプリケーションのコンテナとそれを監視するエージェントのコンテナを Pod として組にしておく、といった使い方が典型的です。

Replica Set

常時起動させておきたい Pod に対して、使用する Docker イメージや環境変数などの設定と合わせて必要な Pod 数を定める定義書のようなものです。スライド中では「× 2 組」という表現で Replica Set を表しています。

何らかの原因で Pod が異常終了してしまった際は、Replica Set で指定された個数に合わせるように自動で新しい Pod が作成されます。これは後述する Controller Manager のはたらきによるものです。

ちなみに、今回はモデリングの都合上 Replica Set が生で登場していますが、実際には直接扱うことはあまりなく、rolling update など高レベルな操作が可能な Deployment と呼ばれる仕組みと組み合わせて使用するのが普通です。以前のバージョンの Kubernetes では Replication Controller という仕組みがこのポジションにいたのですが、Deployment と組み合わせるため、より柔軟にラベリングが可能な Replica Set に移行しました。

etcd

Kubernetes の状態を保持している分散 KVS です。分散なのでもちろん etcd 自体もクラスタリングできるのですが、今回は話がややこしくなるので単独のサーバが存在する体で説明しています。

API Server

ユーザ、あるいは他のコンポーネントに対して JSON ベースの REST API を提供します。Controller Manager や Scheduler は etcd 上の情報を監視して必要に応じて書き換えますが、その際、直接 etcd にアクセスすることはなく、常に API Server が窓口役になります。

Controller Manager

API Server 経由で etcd に登録されている Replica Set の定義を確認し、それに見合った Pod が存在するかどうかをチェックします。前述のようにもし Pod が足りなくなっている場合は新規登録し、逆に多すぎる場合は登録を抹消します。

Scheduler

コンテナのスケジューリング (= どこのサーバに配置するか) を担当します。より具体的には、API Server 経由で etcd に登録されている Pod の中から割り当て Node が未定になっているものを監視し、見つけた場合にはあらかじめ与えたアルゴリズムにしたがって適切な Node に割り当てます。

Kubelet

各 Node に常駐しているエージェントです。API Server 経由で etcd に登録されている Pod の情報をチェックして、自分がいる Node に割り当てられた Pod を発見すると Docker に命じてコンテナを立ち上げさせます。また、今回のモデルには含まれていませんが、Node やコンテナに関して必要な情報を取得する監視エージェントとしての役割も持っています。

サンプルコードを動かしてみよう！

さて、Kubernetes の動作についてスライド + 上の説明で大体のところを理解したら、ぜひ実際に Alloy のモデルを確認してみましょう。

インストールと実行

公式のダウンロードページ Alloy - download から alloy4.2.jar をダウンロードしましょう。dmg 版は古い JRE でしか動かない ので使わないように。

java -jar alloy4.2.jar

でウィンドウが起動するはずです。

今回使用するサンプルコードは Alloy による Kubernetes のコンテナスケジューリングのモデリング · GitHub にアップロードしてあります。kubernetes.als をダウンロードして開いてください。

Alloy が正しく動作していれば、Execute をクリック (もしくは command + E ) すると以下のような図が表示されるはずです。何も出ない場合は Show をクリックしてみてください。

f:id:y_taka_23:20161219052801p:plain

……なんかやばいのが出ました。矢印が多すぎて訳がわからない！

可視化結果を整える

図がごちゃごちゃになっている原因のひとつは、etcd の持つデータが時刻に依存しており、それを 1 枚の図にすべて表示していることです。まずこれをどうにかして、各時刻における状態をそれぞれ独立して図示できるようにしましょう。

先ほどの状態から、可視化ウィンドウのツールバーにある「Projection: none」を開いて「Time」にチェックを入れてください。図が次のように変化するはずです。

f:id:y_taka_23:20161219053327p:plain

ちょっとましになりました。またよく見ると、ウィンドウの下側に「Time0」と表示されるようになったはずです。Time は今回のモデルで時刻を表すパラメータになっていて、etcd の状態の時間断面を表示することができます。射影 (projection) と呼ばれる操作です。射影する時刻を動かして図が変化することを確認しましょう。

それでもまだ矢印が多すぎてわかりづらいので、必要な情報だけを残して非表示にしてしまいたいと思います。手動で設定することも可能ですが、Alloy は可視化時の設定を XML ファイル (拡張子は .thm) として書き出す/読み込む機能があるのでこれを使います。

先ほどの Alloy による Kubernetes のコンテナスケジューリングのモデリング · GitHub から、alloy_kubernetes.thm をダウンロードしておきます。メインウィンドウのツールバーから「Theme」を選び「Load Theme...」してください。

f:id:y_taka_23:20161219054148p:plain

この状態で「Time0」で射影すると、上のような状態になるはずです。これは etcd の初期状態で、

API Server は etcd に接続している
etcd は Node の一覧を持っているが、Replica Set や Pod はまだ登録されていない

という状態を表しています。時刻を変化させて、上の説明で登場した各コンポーネントが仕事する様子を心ゆくまで確認してみましょう。

まとめ

さて、本エントリでは NGK2016B での LT を補足するものとして

Kubernetes のコンポーネントの概要
サンプルコードを使ってスライドと同じ可視化結果を得る方法

を説明しました。

サンプルコード alloy_kubernetes.als が何を表しているのか、あるいはどのようにしてこのモデルを実装したかという話題も色々と面白いところではあるのですが、ちょっと長くなるので、それはまた別の話。

2016-11-20

Frege のチュートリアル集「Frege Goodness」を翻訳しました

Frege のチュートリアル集を日本語に翻訳しました。原著は Dierk Koenig 氏による Frege Goodness · GitBook です。

www.gitbook.com

対象読者

まえがきでも述べられている通り、Frege の (すなわち Haskell の) 基本的な文法については既知のものとして扱われます。より具体的には「すごい Haskell」の前半部分を読んだ、ぐらいでしょうか。例えば型クラス自体は知っている必要がありますが、モナドに対する理解は要求しません。

ちなみに、目を通していただけるとすぐにわかりますが、実は Frege に特有な内容はさほど登場しません。どちらかというと Java プログラマに対して Haskell 的な考え方を導入するために Frege を題材にしている、という印象が近いでしょう。

ただし「ドット記法の威力」の記事は例外 です。Frege では Haskell と異なり、 Lens に似たドットアクセッサを使用する機能がデフォルトで定義されています。ちょっとした目新しさのある部分なので、すでに Haskell をよく知っている方はここをエントリポイントにするのがオススメです。

公開プラットフォーム

今回の翻訳版は、原著に合わせる意味もあって、GitBook で公開しています。GitBook は特定の形式を持つ Git レポジトリと紐付けておくと自動で電子書籍としてレンダリングしてくれるサービスです。原稿は Markdown あるいは AsciiDoc が使用可能で、各種形式でのダウンロードにも対応しています。

なお、原稿本体は GitHub にホスティングしてあります。誤植や表記ゆれ、誤訳などお気付きの際には issue や PR を上げていただけると大変にありがたいです。

github.com

ところで現状、GitBook から日本語書籍を PDF 出力するとフォントが正しく埋め込まれず、中国語フォントになってしまうようです。CSS できちんと指定する必要があるのですが、それはまた別の話。

2016-10-30

Frege からメールが送信できるようになりました

ちょっとした Web アプリを作成しようと思うと、メール送信機能がないと困ります。例えば、ログイン機能を持っていれば必然的にパスワードリセットとかも必要になりますからね。

Haskell 風の JVM 言語 Frege でもフレームワーク Chinook を使用して Web アプリが作れますが、メールを送信するライブラリが見当たらなかったので自作しました。

github.com

なお、すでに Bintray に公開済みなので、各種ビルドツール経由で呼び出すことができます。現状、Frege のビルドは Gradle がデファクトスタンダードなので、以下でも Gradle で説明しましょう。

bintray.com

使い方

Gradle ビルド時に Bintray に問い合わせに行くように、build.gradle にリポジトリを追加する必要があります。普段 Maven Central とか jCenter だけ使っていると忘れがちなので気を付けましょう。

あとは Frege コンパイラ自体と、Frege 用のタスクを Gradle に認識させるプラグインを追加すると、ビルド可能な最小の build.gradle は以下のようになります。

plugins {
    id 'org.frege-lang' version '0.5'
}

apply plugin: 'org.frege-lang'

repositories {
    jcenter()
    maven {
        url 'http://dl.bintray.com/y-taka-23/maven'
    }
}

dependencies {
    compile 'org.frege-lang:frege:3.23.288-gaa3af0c'
    compile 'io.cheshirecat:frege-email:0.1.0'
}

さて、実際にメールを送信するコードを書いてみましょう。

送信サーバとしてはとりあえず Gmail を使用します。残念なことに現状安全性の低いアプリからのアクセスを許可しておく必要がありますが、いずれは対応したい。

コードはこんな感じになります。yourusername と yourpassword は手持ちの Google アカウントに差し替えてください。

module Main where

import io.cheshirecat.frege.Email

server = sslSMTPServer.{ hostName = "smtp.gmail.com" }
auth   = authentication.{ userName = "yourusername"
                        , password = "yourpassword"
                        }
addr     = address.{ email = "foo@gmail.com" }
testMail = email.{ subject  = "Test Mail"
                 , from     = addr
                 , to       = [addr]
                 , message  = "This is a test mail."
                 }

main _ = do
    flip catch handler $ do
        sendEmail server (Just auth) testMail
  where handler = \(e::EmailException) -> e.printStackTrace

このコードを src/main/frege/Main.fr に置いておきます。

生成されるクラスファイルを直接 java コマンドで叩いても実行できますが、Gradle から実行するのであればさらに build.gradle に

apply plugin: 'application'
mainClassName = 'Main'

を追加した上で gradle run で実行すると Gmail にテストメールが届くはず。

Frege のおいしいところ

今回のライブラリは Apache Commons Email を呼び出していて、自前で実装しているロジックはほとんどありません。JVM 言語の利点としてよく「既存の Java 資産を使用できる」という点が挙げられますが、Frege もその例外ではなく、面倒な処理は全部 Java 呼び出しで済ませました。

ちなみに呼び出し部分のコードはこんな感じになります。Frege による Java 連携に興味がある人は、次のスライドが役に立つはずです。

すごい Frege たのしく学ぼう！ from y_taka_23

www.slideshare.net

また、前述の Gradle ビルドからわかる通り、作成したライブラリの配布についても、既存の Java のエコシステムに乗っかることができます。ライブラリを作る側の作業については若干気をつける点があるため、備忘録を兼ねてこのブログで書くつもりではありますが、それはまた別の話。

2016-10-23

JAWS FESTA 東海道 2016 で形式手法によるネットワーク設計について話してきました

先日行われた JAWS FESTA 東海道 2016 で登壇してきました。

形式手法と AWS のおいしい関係。- モデル検査器 Alloy によるインフラ設計技法 #jawsfesta from y_taka_23

www.slideshare.net

テーマは以前 AWS Summit で発表したものと同じですが、前回が 5 分の LT だったのに比べて今回は 25 分の枠を頂きました。そこで、形式手法を用いる動機を中心に据えた前回と比較して、以下のような実践的なトピックを充実させてあります。

Alloy を使うためにの最低限必要な言語機能を知る
シンプルな Web サーバ周りのネットワークについて、仕様から設計を導出する

ちなみに前回の AWS Summit 2016 での発表に関してはこちらから。

ccvanishing.hateblo.jp

寄せられた質問

発表後に頂いたいくつかコメントや質問について、ここで説明しておきます。

「全探索」と言っているが、無限の範囲を探索するのは不可能なのでは？

はい、その通りです。Alloy におけるシグネチャは有限集合でしかありえないので、探索はその範囲に限られます。例えば、

run fooPred for 5

とすると各シグネチャの要素数が 5 個以下の場合を探索します。デフォルトは 3 です。

とはいえ、資料中に登場する 3 個の要素を持つ 2 種類のシグネチャ間の関係だけを考えるケースでさえ、考えうる関係の数は 2 の 3 * 3 乗で 512 通りもあります。実用的なモデルを書こうと思えば場合の数は急激に増えていくため、人力でテストケースを組むことを考えれば Alloy も捨てたものではありません。

ちなみにこのような Alloy の設計思想は「もし仕様バグが存在するなら、それは比較的小さなモデルの時点ですでに問題になるはずだ」というアイデアで正当化されています。この考え方は 小スコープ仮説 (small scope hypothesis) と呼ばれています。

AWS リソースを自前でモデル化するのは辛そう。ライブラリ化の予定は？

できたら面白いとは思っていますが、現実的には厳しそうです。

これは、ライブラリを作成しようと思うと、必然的に個別事例では必要のない部分（例えばセキュリティグループのみ考えてネットワーク ACL は使わない、など）までモデルに含まれてしまうためです。Alloy のモデルは関係が必ず集合に結びつく形で定義されているため合成可能性に乏しく、必要な要素のみライブラリから取り出して使用することが困難なのです。

現時点では、個別にそのとき必要な部分を取捨選択してモデル化するのが妥協案だと思います。

Alloy を勉強しようと思ったら何から始めるのがいい？

毎回名前を挙げていますが、以下の書籍がおすすめです。初見だと多少記述がとっつきづらく感じるかもしれませんが、実際に Alloy を動かしつつ読むと理解が深まるでしょう。なおこの本の内容を把握したら後は慣れの問題です。

estore.ohmsha.co.jp

おわりに

今回の発表、実は当初はここまで Alloy に特化せず、参照した論文中で述べられている AWS 内での取り組みをもう少し前面に出そうかと思っていました。スライドの途中で TLA+ の名前が出てくるのは名残です。

ただ TLA+ は完全にオートマトン型の典型的なモデル検査器であり、AWS を 使う側 とは相性があまり良くなかったため、具体的な内容は結局すべて外してしまいました。その分 Alloy についてはこの発表を聞いた人がとりあえず触ってみる程度のことは説明できたので、まあ結果オーライかなとは思います。

ところで、今年もまた名古屋のコミュニティ合同忘年会 NGK2016B がありますね？自分はここ数年連続して色々なモデル検査ツールの発表をしているのですが、それはまた別の話。

2016-06-06

AWS Summit Tokyo 2016 で形式手法について話してきました

先日行われた AWS Summit Tokyo 2016 で、形式手法のインフラ設計への応用について発表してきました。

形式手法で捗る！インフラ構成の設計と検証 from y_taka_23

www.slideshare.net

モデル検査器 Alloy を利用して AWS の設定を検査する、という内容の LT で、昨年 12 月の NGK2015B でも同じテーマについて話しています。よければ以下の記事も合わせてお読みください。

ccvanishing.hateblo.jp

NGK2015B の発表ではサンプルコードの紹介に比較的時間を割いているのに対して、今回の発表では「動機」の部分によりウェイトを置いた構成になっています。

なぜ形式手法なのか？

今回のテーマを一言でまとめると以下のようになります。

インフラ構成が「秘伝のタレ」と化すのをどう防ぐべきか？

ある程度の規模のインフラを長期間運用していると、どうしても初期の想定が変質してくることは避け得ません。アプリ側の要件が変わったりして、インフラ側がアドホックな対応を迫られるケースも（本来望ましくないですが）一定の割合で生じるものです。また、担当者が代替わりして暗黙知がうまく引き継がれない状況もあるでしょう。

必然的にカオスの縁にいる我々は、どうやってこの状況に対抗すべきでしょう？アプリ開発であればきっと「単体テスト書こうぜ！」みたいな流れになるわけですが、さてインフラを検証したい場合にどんな手段が取れるのか？

awspec

「AWS + テスト」というキーワードで真っ先に思い出すのはおそらく awspec ではないかと思います。

github.com

awspec は servespec に着想を得たツールで、RSpec を利用して AWS リソースをテストできるようになっています。また、人間が直接 spec を記述するだけでなく、現に存在するリソースから awspec generate コマンドを使ってテストケースを自動生成することも可能です。

しかし、すでに存在するリソースをテストするという性質上、設計を考える段階での試行錯誤にはあまり向いていません。また、何かを変更しようとした際にそれをあらかじめ検証するという用途も難しいでしょう。好き好んで Amazon にお布施をしたい人は別として、テストそれ自体に掛かるコスト面も大きな問題です。

IAM Policy Simulator

さて、翻って他の方法を考えてみると、IAM のアクセス権限については、公式がシミュレータを提供してくれています。

docs.aws.amazon.com

実際の操作を行わなくとも dry run で検証できる、というのが大きなメリットで、例えば「削除」の権限をテストするのに実際の削除は発生しません。これがあれば、少なくとも IAM のアクセスポリシーを設定する際には、心ゆくまで試行錯誤ができそうです。

しかし（当たり前ですが）この機能は IAM 限定。となると、以下のような疑問が自然に生じます。

「現物」がなくても検証できる、汎用的な手法はないか？

この疑問への答えとして、現物ではなく形式化したモデルを検証することで有益な結果が得られるのではないか、というのが今回の発表の主題です。

形式手法とその限界

形式手法とは、システムの静的解析の中でも特に

システムの仕様を数学的に厳密に記述する
その正しさをやはり数学的に保証する

という特徴を持つ一連の手法を指して使われる用語です。現物と離れたところで堅く検証を行う、という意味では今回の目的にはピッタリです。

しかし如何せん、形式手法はコストがかかります。そもそも形式手法が扱える人間が少ないことに加え、大抵のツールでは従来のテストよりもずっと多くの工数が必要になります。そのため実際の形式手法の導入は、そのコストを支払ってもお釣りがくるほど高信頼性が求められる案件に限られているのが現状です。

今回の場合、どの程度ならコストとメリットが釣り合うのかはよく考える必要があります。形式手法を採用するのは手段であって目的ではないわけで、そこに必要以上に時間をかけるのはどう考えても本末転倒です。

このジレンマをなんとかするために登場するツールが Alloy Analyzer です。

アンチテーゼとしての Alloy

Alloy では関係論理を利用してシステムのモデルを定義し、さらにそこに検査したい制約を加えたものを充足可能性問題に変換することで、SAT ソルバを利用して条件を満たす例・満たさない例を全探索します。モデルの定義や制約の記述にはやや慣れが必要ですが、他のツールと異なり検証作業自体は自動化されており、上で述べたコストの問題はある程度クリアできます。

手軽に使用できる反面、当然ある種の欠点もあります。テストと比較して形式手法を語る際、メリットとしてよく「テストは有限個のケースしか検証できない。形式手法では無限個の入力に対して正しさを保証できる」という言い回しがなされることがありますが、Alloy についてこれは成り立ちません。

全探索を行うことからもわかる通り、Alloy による検証では、モデル中の要素の個数を制限する必要があります。この制限は例えば今回であれば「セキュリティーグループが 3 個以下の場合」のような但し書きとして現れます。

実は Alloy の背景には「仕様バグは小さなモデルで十分再現できる」という哲学があります。つまり、セキュリティグループが 10 個以上の場合に初めて現れる問題はそうそうないだろう、というわけです。この哲学は 小スコープ仮説 (small scope hypothesis) と呼ばれており、ある種の割り切りによって支えられています。

おわりに

今回の発表では、インフラの検証に形式手法が使えること、およびそのためのツールとして Alloy Analyzer を紹介しました。Alloy に興味を持った人は、以前の記事でも紹介していますが、以下の参考書が鉄板です。

estore.ohmsha.co.jp

ちなみに余談ですが、実は（AWS を利用する側ではなく）AWS そのものの設計にも形式手法が利用されています。しかも、形式手法を導入するにあたって Alloy が検討されていたにもかかわらず、結果的には要件に合わずに TLA+ という別のツールが採用されるという経緯を辿っています。

cacm.acm.org

この辺り、ツールの特性の比較などと絡めて考えると面白い話題でもあるのですが、それはまた別の話。

2016-04-17

NL 名古屋で Frege の評価戦略について話してきました

先日の歌舞伎座.tech に引き続き、NL名古屋 - connpass で Haskell 風 JVM 言語 Frege について発表してきました。

今回の発表では、Frege の持つ Haskell 的特徴である非正格評価に焦点を当て、正格評価を行うはずの Java 上でなぜ評価を遅延させられるのか、その内幕を解説しています。

Frege, What a Non-strict Language from y_taka_23

www.slideshare.net

なお当日の様子は NL名古屋 -NLとはなんだったのか- #nlnagoya - Togetterまとめにまとめられています。長丁場でしたが、各々さまざまなテーマの発表があり、楽しめるイベントだったと思います。

Java のコード生成を試してみよう！

発表中に述べている通り、Frege のコンパイラはバイトコードではなく Java のソースコードを出力します。ただしスライド中で言及されているコードは Frege が生成した Java コードそのものではなく、今回の内容との関連が薄い部分をわかりやすく改変したものです。ここでは実際にどのようなコンパイル結果が得られるのかを見てみましょう。

コンパイラとコードの準備

Frege の Java 生成ロジックは、最新バージョン v3.24 から大きく変更になりました。今回の発表で述べられているのはこの新しい方のロジックです。

最新のコンパイラはまだ α 版で、各種ビルドツールではまだ使用できないようなので、直接バイナリをダウンロードします。

$ wget -O fregec.jar https://github.com/Frege/frege/releases/download/3.24alpha/frege3.24.61.jar
$ chmod +x fregec.jar

次に、スライド中で登場した竹内のたらい回し関数をサンプルとして使用します。以下の Frege コードを Tarai.fr として保存してください。

module Tarai where

tarai :: Int -> Int -> Int -> Int
tarai x y z =
    if x <= y
        then y
        else tarai (tarai (x - 1) y z)
                   (tarai (y - 1) z x)
                   (tarai (z - 1) x y)

ビルド結果が散らからないように、出力先として build ディレクトリを作成しておきましょう。

$ mkdir build

コンパイル結果の確認

以下のコマンドでコンパイルを実行します。

$ java -Xss1m -jar fregec.jar -d build Tarai.fr

しばらく待つと build 以下に Tarai.java と Tarai.class が生成されます。

今回の目的である build/Tarai.java を確認してみましょう。ファイルの前半はボイラープレートなので無視して、以下の部分が tarai 関数の変換結果です。

final public static int tarai(int arg$1, int arg$2, Lazy<Integer> arg$3) {
  tailrecursion: while (true) {
    final int arg$1f = arg$1;
    final int arg$2f = arg$2;
    final Lazy<Integer> arg$3f = arg$3;
    if (arg$1f <= arg$2f) {
      return arg$2f;
    }
    else {
      arg$1 = Tarai.tarai(arg$1f - 1, arg$2f, arg$3f);
      arg$2 = Tarai.tarai(arg$2f - 1, (int)arg$3f.call(), Thunk.<Integer>lazy(arg$1f));
      arg$3 = Thunk.<Integer>shared(
            (Lazy<Integer>)(() -> Tarai.tarai((int)arg$3f.call() - 1, arg$1f, Thunk.<Integer>lazy(arg$2f)))
          );
      continue tailrecursion;
    }
  }
}

まず気づくこととして、Frege 側の tarai 関数は再帰の形で定義されていましたが、末尾再帰最適化の結果ループ tailrecursion に変換されています。このままだと本題が見えづらいので、Tarai.fr を以下のように書き換えてあえて最適化しないようにしてみましょう。

module Tarai where

tarai :: Int -> Int -> Int -> Int
tarai x y z =
    if x <= y
        then y
        else 0 + tarai (tarai (x - 1) y z)
                       (tarai (y - 1) z x)
                       (tarai (z - 1) x y)

生成される build/Tarai.java は以下のように変化します。

final public static int tarai(final int arg$1, final int arg$2, final Lazy<Integer> arg$3) {
  if (arg$1 <= arg$2) {
    return arg$2;
  }
  else {
    return 0 + Tarai.tarai(
              Tarai.tarai(arg$1 - 1, arg$2, arg$3), Tarai.tarai(arg$2 - 1, (int)arg$3.call(), Thunk.<Integer>lazy(arg$1)),
              Thunk.<Integer>shared(
                    (Lazy<Integer>)(() -> Tarai.tarai((int)arg$3.call() - 1, arg$1, Thunk.<Integer>lazy(arg$2)))
                  )
            );
  }
}

ここから、識別子をわかりやすく x y z に変更して不要な修飾子も削ったものがスライド中に登場したコードです。

static int tarai(int x, int y, Lazy<Integer> z) {
  if (x <= y) {
    return y;
  } else {
    return tarai(
        tarai(x - 1, y, z),
        tarai(y - 1, (int)z.call(), Thunk.<Integer>lazy(x)),
        Thunk.<Integer>shared(
            (Lazy<Integer>)(() -> tarai((int)z.call() - 1, x, Thunk.<Integer>lazy(y))))
    );
  }
}

まとめ

本記事では、発表中に端折り気味だった Java のコード生成部分について、実際のたらい回し関数のコンパイル結果を挙げて補足しました。スライドも合わせて確認してもらえると幸いです。

ちなみに、今回のたらい回し関数は単純に int をとって int を返すだけの関数でした。しかし実際の Frege コードにはもっと複雑な言語機能がいくらでも登場し、

高階関数や部分適用のマッピング
代数的データ型のマッピング
モナドのマッピング

などを Java 上で再現するために語るべきことは尽きません。いずれこのブログのネタにでもしますが、それはまた別の話。

2016-03-22

歌舞伎座.tech #9 で Frege について話してきました

先日行われた歌舞伎座.tech#9「異種プログラミング言語格闘勉強会」 - connpass で Haskell 風 JVM 言語である Frege について発表してきました。

今回の勉強会のテーマは「様々な言語に触れて視野を広げる」ということだったので、細かな言語仕様にはあえて触れていません。Frege 自体の紹介と、あとは JVM 言語として一番キャッチーな機能である Java 呼び出しについて解説しました。

すごい Frege たのしく学ぼう！ from y_taka_23

www.slideshare.net

勉強会自体も、マイナ言語の話を一度にこれだけ聞けるというのは珍しくなかなか面白い経験でした。ちなみに個人的に一番の収穫だったのは Pony。歌舞伎座.tech#9でPonyについて発表しました - だいたいよくわからないブログに発表者のブログ記事があります。

話さなかったこと

今回の発表で触れなかった部分にも、興味を惹くトピックがいくつか残っています。

例えば、今回メインに据えた Java バインディング周りでは

frege-native-gen について
基本型、特に String の扱い
null や例外の扱い

さらに、Java 呼び出しとは別の Haskell にない機能として

ドット演算子による Lens 風の関数呼び出し

また、開発環境周りでは

JVM 系ビルドツールとの連携
Eclipse Plugin

などが二の矢として温めてある状態です。

これらについては近いうちにこのブログのネタにしようかとも思っているのですが、それはまた別の話。

チェシャ猫の消滅定理

数学にプログラミング、素敵なもの何もかも。

NGK2016B で Kubernetes + Alloy について話してきました

Kubernetes に関わる役者たち

Master/Node

Pod

Replica Set

etcd

API Server

Controller Manager

Scheduler

Kubelet

サンプルコードを動かしてみよう！

インストールと実行

可視化結果を整える

まとめ

Frege のチュートリアル集「Frege Goodness」を翻訳しました

対象読者

公開プラットフォーム

Frege からメールが送信できるようになりました

使い方

Frege のおいしいところ

JAWS FESTA 東海道 2016 で形式手法によるネットワーク設計について話してきました

寄せられた質問

おわりに

AWS Summit Tokyo 2016 で形式手法について話してきました

なぜ形式手法なのか？

awspec

IAM Policy Simulator

形式手法とその限界

アンチテーゼとしての Alloy

おわりに

NL 名古屋で Frege の評価戦略について話してきました

Java のコード生成を試してみよう！

コンパイラとコードの準備

コンパイル結果の確認

まとめ

歌舞伎座.tech #9 で Frege について話してきました

話さなかったこと