チェシャ猫の消滅定理

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

Haskell ライブラリにスターを送るツール thank-you-stars を作ってみました

HaskellGitHub レポジトリを眺めてみると、有名ライブラリであってもスター数が意外と少ないことがあります。かの Yesod ですら本記事執筆時点で 1,794 個であり、Rails の 36,933 個や Django の 28,165 個と比較すると文字通り桁違いです。

スター数は必ずしも OSS としての評価や価値を反映しませんし、そもそも Haskell ユーザの絶対数が少ないからと言ってしまえばそれまでなのですが、若干寂しい感じがしません?

一方、先日 id:teppeis さんが 依存しているライブラリにスターを送る npm ツール を公開されていました。そこで真似して作ってみた Haskell 版が以下です。

github.com

セットアップ後、自分の Cabal / Stack プロジェクトのルートディレクトリで実行するだけで OK。package.cabal から依存ライブラリを読み取り、それが GitHubホスティングされていればスターを付けにいってくれます。

なお、現在の実装では依存先ライブラリのレポジトリ情報をローカルの Hackage DB から取得しています。初めて package.cabal に記述したライブラリはローカルに存在しない可能性があるので、一度ビルドを通してから試してください。スターを付ける GitHub API は冪等なので重ねて実行しても大丈夫です。

ちなみに、このツール自体が予想以上にスターを集めてしまい、

f:id:y_taka_23:20170914143013p:plain

GitHub Trending で Haskell 部門トップになってしまったのですが、それはまた別の話。

JJUG CCC 2017 Spring で Haskell on JVM について話してきました

先日行われた JJUG CCC 2017 Spring で、JVM 上で動作する Haskell について発表してきました。

www.slideshare.net

メインになるコンテンツはふたつの JVM 言語、FregeEta です。

今回はあくまでも Java のイベントなので、発表前半では Haskell の基本概念、特にモナドについてそれなりの時間を割いて説明してみました。さらにそれを踏まえて後半ではモナドを利用した Java ライブラリの呼び出しに焦点を当て、Frege と Eta それぞれの戦略の違いについて解説しています。

そもそも Haskell on JVM というマニアックで Java そのものと無関係なテーマ、かつ時間的に最後の枠ということで、個人的には若干集客を危惧していました。しかしフタを開けてみれば文字通り満席という結果で、それなりに怖いもの見たさ需要はあったのかもしれません。

また、このイベントではアンケートシステムが実装されていて講演者は結果が見られるのですが、その中で「今日の中で一番参考になりました」「monad の解説として非常にわかり易かった」というコメントをくださった方がいました。少しでも誰かの役に立ったのであれば幸いです。

ちなみに、発表中ではあまり掘り下げていませんが、Frege と Eta で実用的なプログラムを書こうとする上で最も大きな違いは、GHC 拡張のサポートです。

Frege は初めから “Vanilla Haskell” がターゲットであると明言しており GHC 拡張がサポートされる予定はありません。一方 Eta は「実用的な機能」を標榜して積極的なサポートを宣言しており、そもそも Java ライブラリの呼び出しからして GHC 拡張を利用する仕組みになっています。

では具体的には Eta はどうやって GHC 拡張を利用しているのか? このあたりを掘り下げた解説もいずれこのブログで書きたいですが、それはまた別の話。

超技術書典で同人誌『入門 LiquidHaskell』を頒布できませんでした

先日、ニコニコ超会議内で行われた「超技術書典」にて、LiquidHaskell の同人誌でサークル参加してきました。

lh101.dodgsonlabs.com

技術書典 2 ではそこそこの部数が出た ので Haskell 同人誌の需要はゼロではないと踏んでいたのですが、びっくりするぐらい売れません でした。とりあえず後に続く人が同じ轍を踏まないように、今回の様子について記録しておきます。

頒布物

頒布した同人誌は以下の 2 種類です。前者は技術書典 2 で頒布したものの増刷、後者は id:kazeula さんから委託を受けた新刊です。

持ち込んだ(冊子版の)部数と実際に売れた部数は以下の通りでした。

  • 入門 LiquidHaskell : 持ち込み 12 部、実売 1 部
  • GHCJS 入門 : 持ち込み 32 部、実売 7 部

技術書典 2 では開始から 3 時間で 50 部実売できたことを考えると、だいぶ客足に差があることがわかります。『入門 LiquidHaskell』は再販なので売れ行きが落ちるのはわかるのですが、『GHCJS 入門』は新刊にもかかわらずあまり売れていません。

設営

ディスプレイは前回とほぼ同じですが、POP のデザインを変更して簡単な要約をつけてみました。上が今回の超技術書典、 下が前回の技術書典 2 です。

当日の様子

売り上げが芳しくなかった原因ですが、やはり客層というかイベントの趣旨の違いが大きかった、というのが実際に参加した印象です。

前回の技術書典 2 はオンリーイベントで、かつ秋葉原という好立地でした。一方、超技術書典はニコニコ超会議のいちコーナであり、しかも会場は都内から 1 時間はかかる幕張、さらにゲーム実況ステージの正面で大音響にさらされる配置です。

実際、売れるかどうか以前にブースに足を止めるお客さん自体がずっと少なかったように思います。もう少し一般ウケするテーマだったらまた違ったかもしれませんが、いかんせん Haskell は世間的にはマイナすぎました。

釣り糸は、魚がいそうな場所で垂らしましょう。

直販できます

というわけで冊子版の在庫があるので、物理的にコンタクトできる方であれば直販が可能です。冊子 + PDF ダウンロードコードで 800 円です。

『入門 LiquidHaskell』についてはとりあえず次回 5 月 21 日の Haskell-jp もくもく回に在庫を持っていきます。欲しい方は声をかけてください。

haskell-jp.connpass.com

なお PDF 版のみ(内容・価格は冊子付きと同じ)は引き続き BOOTH で委託販売していますので、こちらもよろしくお願いします。

booth.pm

ちなみに「次に書く同人誌」のテーマはすでに決まっていて、Haskell 絡みの内容になる予定です。お披露目は早くても冬のコミックマーケットになりますが、それはまた別の話。

技術書典 2 で同人誌『入門 LiquidHaskell』を頒布しました

先日、秋葉原で行われた技術書のオンリーイベント技術書典 2」にて、LiquidHaskell の同人誌を頒布してきました。

lh101.dodgsonlabs.com

LiquidHaskell は、SMT ソルバをバックエンドとして利用することで、Haskell の持つ型の表現力をより強化する仕組みです。通常の Haskell では型情報としてエンコードできない値レベルの制約を記述できるため、例えば「0 でない Int 型」を定義すればゼロ除算をコンパイル時に検知できます。以前の記事 にちょっとした解説があります。

当日は冊子版を 30 冊と PDF 版ダウンロードカードを 50 シリアル用意し、「冊子 + ダウンロードカード」または「ダウンロードカードのみ」という組み合わせで合計 50 点頒布できるようにしてありましたが、おかげさまで開始から 3 時間の時点で完売しました。正直、もう少し強気の部数でもよかったかなという感じです。

現在、BOOTH にて PDF 版の委託販売を行っています。興味はあったけど買えなかったという方がもしいたらご検討ください。

dodgsonlabs.booth.pm

また、4 月 29 日のニコニコ超会議併設イベント「超技術書典」にもサークル参加予定(1 日目 A-04)です。冊子版の増刷は未定ですが、少なくともダウンロードカードは頒布したいと思います。

techbookfest.org

ちなみに今回の技術書典、実はサークル参加はおろか同人誌の即売会というものに参加すること自体はじめてでした。申し込みの経緯や準備の流れ、当日の参加レポートなどはエントリを改めて投稿する予定ですが、それはまた別の話。

LiquidHaskell コトハジメ

このエントリは Haskell Advent Calendar 2016 および Formal Method Advent Calendar 2016 の 23 日目の投稿です。のはずでしたがすでに日付が変わりました。謹んでお詫び申し上げます。

ちなみに 22 日目の担当者はそれぞれ

です。偶然ですが同じ方が執筆担当ですね。

さて、本エントリでは Haskell の型の表現力をより豊かにする仕組み、 LiquidHaskell について概要を紹介します。使用するサンプルコードは Samples of Verification by LiquidHaskell · GitHub にアップロードしてあります。

実行時エラーを防ぐには

簡単な例として、リストの先頭要素を取る関数 head の型を考えてみましょう。

*Main> :t head
head :: [a] -> a

型としてはもちろんこれで正しいのですが、しかし空リストに対して haed を呼ぼうとすると実行時エラーが発生してしまいます。

*Main> head []
*** Exception: Prelude.head: empty list

では、このような実行時エラーをコンパイル時に、何らかの静的検査によって防ぐことはできないでしょうか?

head :: [a] -> a という型は、「何らかの型 a の要素を持つリストを引数に取って、同じ型 a を持つ値を返す」という head の制約を規定していますが、リストの長さについては何も主張していません。つまり上のエラーを防ぐためには、「引数となるリストが空でない」という事前条件を型にエンコードできればよいことになります。

これを実現する方法はいくつか考えられます。GADTs 言語拡張 を使って型レベル自然数を定義し、さらに型レベル自然数を長さとして持つ「長さ付きリスト型」を定義すれば空リストかどうかが型によって判定できそうです。また、依存型をフルに使える Haskell 以外の言語であればもっと素直な方法で表現できるでしょう。しかし、いずれも元の実装からは大きな改修が必要で、しかも関連箇所すべてを「長さ付きリスト型」で置き換えることになるため、なかなか骨が折れそうです。

LiquidHaskell では、専用のコメント {-@ ... @-} を使用して次のように記述します。

{-@ safeHead :: { xs:[a] | len xs > 0 } -> a @-}
safeHead :: [a] -> a
safeHead [] = liquidError "empty list"
safeHead (x : _) = x

「長さが 0 を超える (= 空リストでない)」という事前条件がコメント内に型として表現されていることがわかります。LiquidHaskell が使用する情報は通常の GHC から見るとあくまでも単なるコメントであって、通常と同じように (検証を行わない) コンパイルが可能です。実際、ここでは分かりやすさ優先で safeHead と名前をつけましたが、関数名を head にしておけば呼び出し側モジュールの import 文を書き換えるだけで実装の差し替えが可能です。

新しく登場した liquidError が何者なのかは若干気になりますが、とりあえず先に処理系を動かせる状態を作りましょう。

インストールと最初の一歩

LiquidHaskell はバックエンドとして SMT ソルバを使用するため、あらかじめ本体とは別にセットアップしておく必要があります。自分の場合は Z3 の最新版 v4.5.0を選択しました。

github.com

本体の方は cabal でインストールするか、もしくはソースコードを clone してきて stack buildコンパイルするかの選択肢が提供されています。残念ながら Stackage には登録されていないようで、だいぶ前から "We are working to put liquid on stackage" のままになっています。

github.com

セットアップができたら先ほどの例を動かしてみましょう。以下のコードを Sample.hs として適当なところに保存し、liquid Sample.hs を実行してみてください。

module Sample where

import Language.Haskell.Liquid.Prelude ( liquidError )

{-@ safeHead :: { xs:[a] | len xs > 0 } -> a @-}
safeHead []      = liquidError "empty list"
safeHead (x : _) = x

実行時にいくつか進捗メッセージが表示されますが、最終的に

**** RESULT: SAFE **************************************************************

が表示されれば問題なくインストールできています。ようこそ、LiquidHaskell の世界へ!

LiquidHaskell の仕組み

型検査とサブタイピング

先ほどのコードスニペットをもう少しいじって動作を確かめてみましょう。まず、元のコードに次の関数を付け加えてみてください。

badUsage = safeHead []

safeHead を、事前条件に反して呼び出そうとしているわけです。liquid Sample.hs を実行すると、以下のようなエラーメッセージが返ってくるはずです。

**** RESULT: UNSAFE ************************************************************


/your/path/to/Sample.hs:9:12-22: Error: Liquid Type Mismatch

 9 | badUsage = safeHead []
                ^^^^^^^^^^^

   Inferred type
     VV : {VV : [a] | len VV == 0
                      && (null VV <=> true)
                      && len VV >= 0
                      && VV == ?a
                      && len VV >= 0}

   not a subtype of Required type
     VV : {VV : [a] | len VV > 0}

   In Context
     ?a : {?a : [a] | len ?a == 0
                      && (null ?a <=> true)
                      && len ?a >= 0}

「推論された型が要求された型のサブタイプではない」と言われていますね。

先ほど「a を要素とする空でないリスト」の型を { xs:[a] | len xs > 0 } と表現しましたが、LiquidHaskell では一般に「型 a のうち述語 P を満たすもの」は { x:a | P x } で表現されます。そして a 型の任意の値 x について P x => Q x が成り立つと SMT ソルバが判定した場合、LiquidHaskel は { x:a | P x}{ x:a | Q x } のサブタイプであると判断します。

この例でいえば、実引数 [] から推論された述語 len VV == 0 && ... から safeHead の事前条件 len VV > 0 は (当然) 従わないため、コンパイルエラーとして検出されているのです。

それでは逆に badUsage を削除、さらに safeHead{-@ ... @-} コメントも無効化して実行してみましょう。今度は別のエラーになります。

**** RESULT: UNSAFE ************************************************************


/your/path/to/Sample.hs:6:32-43: Error: Liquid Type Mismatch

 6 | safeHead []      = liquidError "empty list"
                                    ^^^^^^^^^^^^

   Inferred type
     VV : {VV : [Char] | VV ~~ ?b
                         && len VV == strLen ?b
                         && len VV >= 0
                         && VV == ?a
                         && len VV >= 0}

   not a subtype of Required type
     VV : {VV : [Char] | false}

   In Context
     ?b : {?b : Addr# | ?b == "empty list"}

     ?a : {?a : [Char] | ?a ~~ ?b
                         && len ?a == strLen ?b
                         && len ?a >= 0}

これを見ると、liquidError の正体がわかります。

liquidError の引数として要求されている型は {VV : [Char] | false} です。false は決して真になることがない述語なので、いかなる引数であっても事前条件を満たすことができません。すなわち、liquidError は呼び出されうる場所に配置されると直ちにコンパイルを失敗させます。

もともとは safeHead の事前条件 { xs:[a] | len xs > 0 } が約束されていたためこのパターンマッチを通過しないことが LiquidHaskell によって推論されていたのですが、事前条件を外したことでエラーになったのでした。

もう少し単純な例を使って制約のかけ方を定式化してみましょう。

事前条件

上でも使用していたパターンですが、引数 (のうちのいくつか) に制約をつけることで関数の事前条件を表現することができます。例えば以下はゼロ除算エラーが発生しない割り算の定義です。

{-@ safeDiv :: Int -> { d:Int | d /= 0 } -> Int @-}
safeDiv :: Int -> Int -> Int
safeDiv n 0 = liquidError "zero divide"
safeDiv n d = n `div` d

事前条件が指定されると、その関数のすべての呼び出しについて事前条件が守られているかどうかが検査されます。また、関数内のロジックや事後条件の検証は事前条件の仮定下で行われます。

事後条件

引数ではなく戻り値側に制約をつけて事後条件を表現することもできます。例えば以下は絶対値関数が常に 0 以上の値を返すことを表しています。

{-@ safeAbs :: Int -> { n:Int | n >= 0} @-}
safeAbs :: Int -> Int
safeAbs n
    | n >= 0    = n
    | otherwise = 0 - n

事後条件が指定されると、関数の事前条件および関数内のロジックから事後条件が従うかどうかが検査されます。また、他の関数内で呼び出された呼び出し側の検証は事後条件の仮定下で行われます。

事前条件に依存した事後条件

場合によっては、事前条件に依存した事後条件を記述する必要があります。

例えば整数に 1 を加算する関数について、事後条件に「戻り値は引数より真に大きい」という事後条件を与えてみましょう。条件を記述する際、次のように引数に名前をつけることができます。

{-@ safeIncr :: n:Int -> { v:Int | v > n } @-}
safeIncr :: Int -> Int
safeIncr n = n + 1

引数に事前条件を課し、さらに名前をつけて事後条件で引用することも可能です。

{-@ safeDouble :: n:{ v:Int | v > 2 } -> { w:Int | w > n + 2 } @-}
safeDouble :: Int -> Int
safeDouble n = 2 * n

例:ベクトルの次元付き計算

それでは例として、依存型を説明する際によく登場するベクトルの次元付き計算について、LiquidHaskell で表現してみましょう。

Haskell 上でベクトルを表現するもっともナイーブな方法は、単に Num インスタンスを要素とするリストを使用することです。例えばベクトル同士の足し算であればこんな感じでしょうか。

vecSum :: (Num a) => [a] -> [a] -> [a]
vecSum xs ys = zipWith (+) xs ys

しかしお気付きの通り、次元が違うベクトル同士が加算できてしまうため、本来表現したい制約が表現できていません。

badSum = vecSum [1, 2, 3] [4, 5]

*Main> badSum
[5,7]

LiquidHaskell を使って、次元が異なるベクトルについて計算できないようにしてみましょう。そもそもの原因は、zipWith 関数が短い方のリストに合わせて残りを切り捨ててしまうことにあるため、まずこれを LiquidHaskell で書き直しておきます。

{-@ vecZipWith :: (a -> b -> c) ->
    xs:[a] -> { ys:[b] | len ys = len xs } -> { zs:[c] | len zs = len xs } @-}
vecZipWith _ []       []       = []
vecZipWith f (x : xs) (y : ys) = f x y : vecZipWith f xs ys
vecZipWith _ _        _        = liquidError "dimension mismatch"

事前条件として「第 2 引数の長さが第 1 引数に等しい」こと、さらに事後条件として「戻り値の長さが第 1 引数に等しいこと」が要求されています。この「次元付き zipWith」を使ってベクトルの足し算を以下のように定義すると

{-@ vecSum :: (Num a) =>
    xs:[a] -> { ys:[a] | len ys = len xs } -> { zs:[a] | len zs = len xs } @-}
vecSum xs ys = vecZipWith (+) xs ys

LiquidHaskell は狙い通り警告を出してコンパイルを失敗させます。

/your/path/to/Sample.hs:37:10-33: Error: Liquid Type Mismatch

 37 | badSum = vecSum [1, 2, 3] [4, 5]
               ^^^^^^^^^^^^^^^^^^^^^^^^

同様にして引き算や

{-@ vecSubtr :: (Num a) =>
    xs:[a] -> { ys:[a] | len ys = len xs } -> { zs:[a] | len zs = len xs } @-}
vecSubtr xs ys = vecZipWith (-) xs ys

ベクトル同士の内積

{-@ dot :: (Num a) => xs:[a] -> { ys:[a] | len ys = len xs } -> a @-}
dot xs ys = sum $ vecZipWith (*) xs ys

あるいはベクトルのスカラー

{-@ vecMap :: (a -> b) -> xs:[a] -> { ys:[b] | len ys = len xs } @-}
vecMap f []       = []
vecMap f (x : xs) = f x : vecMap f xs

{-@  scalar :: (Num a) => a -> xs:[a] -> { ys:[a] | len ys = len xs } @-}
scalar c xs = vecMap (c *) xs

も次元に対して安全に定義可能です。長さが正しくないリストをこれらの関数に与えて、実際にエラーになることを確認してみましょう。

まとめ

本エントリでは、LiquidHaskell を利用してリスト操作関数に対して事前条件と事後条件を定義する方法を扱いました。通常の Haskell ではリストの長さに関するエラーは型検査の対象外であり実行してみるまでわかりませんが、LiquidHaskell を用いることでコンパイル時に検出することができます。

今回紹介したのは、LiquidHaskell が持つ機能の一部分にすぎません。もし面白そうだと感じた人は、対話型チュートリアル もしくは 公式ブログ を眺めてみると良いと思います。というかこれを書いている自分自身もまだ全容を把握できていません。一緒に勉強しましょう。

さて、Advent Calendar の 24 日目の担当者はそれぞれ

  • Haskell Advent Calendar 2016 : タイトル未定 (@maoe さん)
  • Formal Method Advent Calendar 2016 : 空席

となっておりますが、それはまた別の話。

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

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

www.slideshare.net

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

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

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 が何を表しているのか、あるいはどのようにしてこのモデルを実装したかという話題も色々と面白いところではあるのですが、ちょっと長くなるので、それはまた別の話。

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 できちんと指定する必要があるのですが、それはまた別の話。