NII Shonan School on Coq 参加報告


NII Shonan School on Coq に参加して来ました。

Coq というのは定理証明支援系のソフトウェアです。関数型言語に興味のある方の中にはカリー=ハワード対応という言葉をご存知の方もいるのではないかと思いますが、これはプログラム⇔証明、型⇔命題という対応がある、というものです。Coq は依存型という、通常の静的型付け言語 (Haskell とか Scala など) より強力な型システムを用いることで、述語論理 (「全てのεに対して、あるδが存在して、どうのこうの」の様な量化子を含んだ式を表現出来る論理) の証明に対応するプログラムを書き、そしてその証明が正しいかを型検査することで機械的に確認出来ます。

じゃあ Coq を使うと何が良いのかというと、まず数学的な定理の証明を機械検証可能な形で証明出来ます。最近だとケプラー予想の機械的証明が話題になりましたね。他にも四色問題などが定理証明系の上で証明されています。どちらも数学者の人力では証明の検証が難しい問題です。
それとは別に、ソフトウェアが満たすべき仕様を述語論理で記述して、プログラムを実装し、実装が仕様を満たすことを証明出来ます。ユニットテストなどのテストでは網羅的でなかったりなどの問題がありますがCoqを使えばそのような問題はありません。
では、そんな素晴らしいツールがなぜ世の中で広く使われていないのかというと…単純に証明を書くのは難しいからです。Coqで証明を書くにはCoqの技術を磨く必要があります。
そしてその機会が、今回のセミナーという訳です。

セミナーは、葉山のセミナーハウスにて合宿形式5日間コース(半日の鎌倉見物含む)で開催され、内容はCoqの開発元のINRIAから訪れた講師によるCoqチュートリアルでした。
朝から夕食の時間までCoqに関する授業あるいは課題による実習、その後も解けなかった問題を寝るまで解く、というハードな毎日でした。私自身はここんとこあまりCoqで何かを証明してなかったので、多少錆び付いていたCoqのスキルを取り戻す良い機会でした。

残念ながら講義資料は参加者以外に公開されていない様です(パスワードで保護)。ただ、Coq については名古屋のProofCafeや、東京だとSF読み進捗ダメです会議 #9 #readcoqart #Coq(こちらは私も参加しています)といった勉強会が定期開催されているので、興味があれば参加されるとCoqについて学べると思います。

Functional News はじめました


冷やし中華はじめました(挨拶)

暑いので逆に、と思って激辛ラーメン食べたら呪術「激しい発汗」を使ったみたいになった平岩です。こんにちは。

毎日暑くて嫌になりますね。

それはそうと、このたび弊社で Functional News というサービスを立ち上げました。
http://functional-news.com/

関数型言語に関するニュースやイベント情報を自動収集するサービスです。カテゴリ名が表示されているタグっぽいところをクリックすると、絞り込みができます。

イベント情報を言語に絞って見られるのは意外と便利なのではないかと思うのですが、いかがでしょうか。ちなみに AngularJS + play2 scala + scalikejdbc + heroku + postgreSQL という構成です。

今はほぼ自動収集された情報のみですが、ニュースやブログ記事を掲載して、ゆくゆくはメディア化していけるといいなと思っています。

まだまだ荒削りなサービスですが、コミュニティに少しでも恩返しする意味でも、少しずつ良くしていきたいと思っています。フィードバックいただければ大変嬉しいです。

あ、あと、うちはシステム開発会社なので冷やし中華ははじめてません。ごめんなさい。

でも、新メンバー募集中なので(forkwell jobs)、会社に遊びに来ていただければ冷やし中華でも食べに行きましょう。

Scala Days 2014 に参加してきました (3)


前回 の続きです。

私が聴講したセッションのみのレポートとなります。

2014-07-04追記:
全セッションの動画とスライドはこちらにアップロードされています。

3日目


カンファレンス最終日。
この日はホテルで自転車をレンタルし、会場までサイクリングで移動しました。
ベルリンは自転車人口が多く、どんな通りにも自転車専用レーンが整備されています。
道中には歴史的な建造物や緑地が数多くあり、随所でドイツの文化を体感することができました。

  • 国会議事堂

a

[09:00] キーノート: Chad Fowler – @chadfowler

スピーカーの Chad Fowler 氏は、Immutable Infrastructure という言葉を世に広めた1ことでも有名な方です。

印象的なスライドとBGMを駆使した素晴らしいプレゼンテーションに引き込まれました。
話題としては Scala に限った話ではありませんが、キーノートらしい内容だったと思います。

chad

  • レガシーとは何か
    • 多くのエンジニアが持つ偏見: ひどい、嫌い、変化を恐れる頭の硬いマネージャー
    • 一方で、動けばいい、枯れている方が安心、安定しているという意見も
    • 音楽、文学、建築物、ファッション、絵画 ……
      今日でも通用する『レガシー』は皆、素晴らしいもの
    • レガシーを悪い意味で捉えてはいけない
  • 良いソフトウェアになるには 10年かかる
    • にも関わらず、ほとんどのソフトウェアは 5年以内に死ぬ
    • 20年以上生き延びているソフトウェア: TCP/IP, DNS, Linux, Emacs, grep, …
    • Scala は今年で10年。良いソフトウェアの仲間入りができた (笑)
  • 『レガシー』なソフトウェアを作るために
    • 最初の一歩は作ること
    • 価値を提供し続け、替えのきかない存在になる2
  • 生き残るのは、小さな部品システム
    • 人間こそがシステム
    • 細胞のように常に殺し、入れ替えることで、部品は正しく機能する
    • インタフェースは極力シンプルに
  • イミュータブル・デプロイ
    • 既存のノードでは一切のソフトウェア更新を行ってはいけない、という考え方
  • 最初から異なる環境を想定する
    • 例: 特定のプログラミング言語に依存した設計をしない
  • 故障(失敗/障害)を前提とする
    • 全てを監視し、自律的なサービスを
    • Chaos Monkey を使って様々な障害シナリオをランダムに引き起こす
      • 最悪のシナリオを知れば、何も恐れることはない

[10:00] Building a DBMS in Scala or how types can turn a SQL interpreter into a SQL compiler

  • スピーカー: Tiark Rompf – @tiarkrompf
  • スライド (coming soon)

Scala で高性能の DBMS を作れるか、という話。
スピーカーは、EPFL内のOracleの研究施設で働いているという方。

  • 一般化(拡張性・汎用性の向上)と特殊化(応答性能向上)はトレードオフの関係
    • それでも、コンパイル時に計算したり、特殊化のコードを生成することで汎用的な最適化を実現できる

10-01

  • LegoBase という RDBMS を Scala で開発中
    • LMS: Lightweight Modular Staging フレームワークの話
      • ステージング: 順序や使用頻度によってプログラムを置いておくステージを変える
    • クエリの処理順序の最適化: Filter 処理を再帰に実行するなど
    • TPC-H のベンチマークでも良好な成績
  • データベース以外のプロジェクトも、ローレベルなCコードに対抗すべく取り組んでいる
  • Play 2.4 も Reactive Stream ベースの実装に書き換えて、レイテンシが改善しているとのこと

[11:00] Building a Reactive Application

  • スピーカー: Duncan DeVore – @ironfish
  • スライド

  • スピーカーは Viridity Energy という企業の方
    • 電力の大口顧客に対して、プロファイルを受け取って分析・効率化を提案している
  • VPower というクラウドベースのアプリケーションの話
    • 旧来のバージョンは、デプロイ・レスポンス性能・スケーラビリティなどに問題があった
    • ドメイン駆動 + Reactive な設計で作り直した
    • Scala + Akka + Spray.io
  • CQRS: Command/Query Responsibility Segregation
    • コマンドとクエリの分離
    • CRUD モデルは苦痛
    • Append-only アーキテクチャは良い。簡単に分散できてロックを大幅に削減できる
    • 整合性を保つ仕組みの説明
  • ドメイン駆動: 1行のコンフィグで、ビジネスロジックを記述できるようにした
  • 読み込み用と書き込み用のマイクロサービスを異なるJVM上で稼働
    • それぞれ数十個のアクターが動いている
  • Reactive なショッピングカートの実装例
  • 今年の夏に、Manning から本を出版する予定
    • Building Reactive Applications by Duncan DeVore and Sean Walsh

[12:00] ランチ

前日と同じビュッフェスタイルでしたが、メニューは若干変わっていました。


[13:00] Futures and Async: When to Use Which?

Future と Async の違いについて。きちんと理解しておきたいところです。

  • Future について
    • 指定した秒数待機してから結果を返すコードを例に具体的に説明
    • 非同期でないAPIが必要になったら、scala.concurrent.blocking を使う
  • Promise について
    • Promise から future を作る
    • 必要になった場合にのみ使えばよい
  • Async について
    • パイプラインとして使用する例
    • ボクシングの回数が減り、性能が向上するケースもある
    • Production-ready (実業務に耐えうる品質である)
  • Async を使う動機
    • Future ベースのコードをシンプルに書き直せる
    • ただし現在のコードに十分満足しているなら、無理に書き直す必要はない

[14:00] specs2 2.3 whirlwind tour

スピーカーは Specs2 の作者。Specs2 の現状と将来像についてのセッションです。

  • 設計思想の根底にあるのは、実世界とコードの橋渡し
  • Specs2 の機能と使い方を一通り説明
    • sbt, IntelliJ IDEA からテストを実行する例
    • デフォルトでテストは並列処理
      • テストコードの分離性をチェックする助けにもなる
    • Isolation と Selection、タグを付ける
    • コマンドライン引数の解釈
    • ScalaCheck との統合
    • データテーブル形式の記法
    • その他の多種多様な機能
  • Specs2 3.0 の予定
    • 様々なバグ修正
    • オンライン Specification
    • よりライブラリらしく
  • コントリビュートを期待
    • Eclipse プラグイン
    • HTMLレポーティング
    • Selenium と連動した Web テスティング
  • Q&A
    • マッチャーなど、同じ意味のものに様々な書き方がある。
      (===, must_==, must beEqualTo など)
      なぜこのようにしているのか?

      • できるからできる! ルールは自分たちで決めてください (意訳)

早めに終わったのでメイン会場に行くと、こちらのセッションがまだ続いていました。

Scala: The First Ten Years

会場爆笑のムービーが流れた後は撮影会のような様相に。

b


[15:00] Effective APIs

  • スピーカー: Josh Suereth – @jsuereth
  • スライド (coming soon)

本カンファレンスの司会も務めていた Joshua Suereth氏。満を持しての登場です。
API開発のベストプラクティスを紹介してくれました。

josh

  • 良いAPIの基本
    • 型・名前は重要
      • ガイドなしでもユーザが学習できるように、それら自身が説明的であるとよい
    • エラーハンドリング
      • リカバリ可能か
      • ユーザが気にする必要があるか
    • ScalaDoc、チュートリアルを書く
  • バイナリ互換を保つのは大変
    • やってはいけないこと
      • case class のコンストラクタの変更
      • メソッドに引数を追加
      • トレイトに具体メンバを追加
      • クラス/メンバ/引数の削除
    • テクニック
      • 抽象クラスの利用
      • パッケージレベルのプライベート化
      • 独自の unapply 関数を定義して、case class を隠蔽
  • 拡張性を持たせる
    • 公開APIは最小限に留める
    • 引数のデフォルトは避け、オーバーロードを
    • トレイトは pure virtual に
    • final class を適切に利用
    • 既存のメソッドを変えるのではなく、新しいメソッドを追加する
  • Q&A
    • バイナリ互換性が保たれているかどうかを確認する方法はあるか
      • ある。セマンティック・バージョニングによって付けられる番号の変化を確認すればよい。

[16:00] Scala in Numbers – The Ecosystem Census

数字で見る Scala ライブラリ。
GitHub 内の Scala ライブラリを様々な観点でランキングしてみました、というコーナー。
終始和やかな雰囲気で進んでいきました。

  • 識別子の名前
    • ローカル val でよく使われている名前 => result
    • ローカル var でよく使われている名前 => i
    • var が多く使われているライブラリ => rapture-io
    • 引数でよく使われている名前 => f
    • 変数名の長さ => scalaz は 90% の変数名が 2文字以下 (会場爆笑)
  • ライブラリの利用実態
    • 最も多く使われているメソッド => Boolean.&&
    • 最も多く使われているコレクションのメソッド => TraversableLike.map
    • 最も多く使われている predef => augmentString
    • 最も多く定義されている predef 拡張 => any2ArrowAssoc ->
  • 暗黙的な利用
    • 最も多く使われている暗黙的パラメータ => _root_.scala.Function1
    • 最も多く使われている暗黙的パラメータ(Scalaライブラリ) => ClassTag
      • Functor など同じものが複数回出ているのは、表示上 prefix を省いているから
  • 検索ツールの紹介、デモ
    • 構成要素とクローラー
  • 会場からは、deprecated にすべきかどうかの判断材料として便利そう、という意見も
  • さいごに
    • 最も多く記号演算子を定義しているライブラリ => 圧巻の scalaz
    • ユニコードの演算子を定義しているライブラリ => やっぱり scalaz

[17:00] Sparkle: Reactive streams to the browser with scala and d3

スピーカーは Nest、Google、Typesafe といった名だたる企業を渡り歩くエンジニア。
Scala と D3 を使ってデータ可視化のライブラリを作った、という話です。

  • 動機
    • ブラウザ上で大規模データを扱ってインタラクティブな操作(ズームなど)をしたい
    • Scala, JavaScript でデータの変換処理をしたい
  • Sparkle は様々な用途に、誰でも利用可能
    • ビッグデータも素早く可視化
  • Sparkle Data Protocol: WebSocket 対応プロトコルを独自で作成
  • コンポーネントの説明
    • Loaders
    • Fast Storage: Casandra ベースのカラム志向 インメモリDB
    • API
    • Transform
    • Stream
    • Display
  • デモ
    • ダッシュボード
    • repl の操作で正弦波を描画

sparkle

スライドの方にはおまけとして、『Scala の良いところ』や『スタートアップ企業となぜ相性が良いのか』についても記述がありました。


[18:00] クロージング

最後のセッション。
メイン会場で、Typesafe社の方たちへのインタビューが行われました。

closing

  • Scala 2.12 の目玉機能は?
    • Java8対応
    • 邪悪にならないように、Scalaライクに。小さく、速くを目指している
  • Scala 2.13, Scala 3 では、バイナリ互換用の移行ツールを作る予定
  • Scala はオープンなコミュニティ。誰でもコントリビュートできます!

こうして熱狂冷めやらぬままカンファレンスは閉幕。
私自身も、非常に有意義な体験を得られました。

スピーカー・スタッフ・Scala Days 2014 に貢献してくださった全ての方に感謝します。

おわり

  1. Trash Your Servers and Burn Your Code: Immutable Infrastructure and Disposable Components – Chad Fowler []
  2. 出典: Michael Feathers: Your Code.. it’s Alive.. []

Scala Days 2014 に参加してきました (2)


前回 の続きです。

私が聴講したセッションのみのレポートとなります。

2014-07-04追記:
全セッションの動画とスライドはこちらにアップロードされています。

2日目


いよいよカンファレンス本編のスタートです。
ホテルから電車を乗り継ぎ Weberwiese 駅で降り、歩いて会場の Kosmos Berlin へ。

weber

[09:00] キーノート: Erik Meijer@headinthebox

スピーカーの Erik Meijer 氏は昨年の Coursera の講義 で Martin Odersky 氏らとともに講師を務めておられた方です。

講演のタイトルは『The Lost Art of Demotational Semantics』。
ホームページ上の記載とは異なる内容ですね。全編手書きのスライドが Cool なセッションでした。

内容は氏のツイートにもあるように

関数型プログラミングの始祖ともされるクリストファー・ストレイチー氏の理論に従って
Scala の try – finally を再実装してみようという話です。

  • Scala の try – finally の実装は Java のそれとは異なっています。
  • 以下のコードで定義した関数は、それぞれどのような結果が得られるでしょうか。

erik1

なにゆえこんな(一見)奇妙な動作をするのか、そこにはしかるべき基礎があるとのことです。

  • いくつかの記号を定義して try – finally を議論していく様子

erik5
erik2

  • 最後は双対(dual)、カタモルフィズム、アナモルフィズムに話が及びます。

erik3

圏論をきちんと学んでいれば、より理解が深まっただろうと感じたセッションでした。
後日改めて復習しようと思います。


[10:00] Functional Query Optimization with Spark SQL

  • スピーカー: Michael Armbrust – @michaelarmbrust
  • スライド
  • Spark の概要説明
    • Hadoop と親和性が高く、MapReduce よりも高機能
    • Scala との相性もよく、開発者の手間を削減できる
  • Spark SQL の紹介
    • まだ発表して間もないプロダクト
    • Shark との違い
    • スキーマRDDを宣言可能
    • クエリを解析して自動的に最適化する (フィルタ処理を先に実行したりなど)
    • TPC-DS (ビッグデータ向けの標準的なベンチマーク) のテストでは Shark より良い成績
    • Scala の リフレクション + 準クォート(quasiquotes) 機能を使うことで、 Spark SQL 自体も非常にシンプルなコードになっている
    • 将来的には、型安全なクエリ結果にも対応する予定

[11:00] Reactive Streams: And why you should care.

息の合ったお二人の掛け合いが絶妙で、常に会場の笑いを誘っていました。
『Reactive Stream』は、他のセッションでも度々登場した重要なキーワード。
リアクティブ宣言 の流れをくんだものです。

  • ストリームとは何か
    • サイズに依存しないデータの流れ
    • プロセスネットワークとして表現できる
  • Reactive Stream
    • java.util.stream は他のコレクションと異なる挙動があり、直感的でない
    • みんな同じ問題を抱えており、それぞれのコミュニティが独自のソリューションを開発していた
    • 共通のソリューションを提供することが狙い (組織の垣根を超えてトップエンジニアが集結)
    • ストレージ、メモリ量には制限をかけつつも異なる処理性能に柔軟に対応する
    • Push と Pull のハイブリッド機構 (Dynamic Push-Pull) なので、どんなに負荷をかけても OutOfMemory が起こらない
      • といいつつもセッション最後のデモで OutOfMemory が発生し会場爆笑
    • Reactive Stream では最小限のインタフェースだけを提供し、APIに完全な自由を与える
    • 将来は JDK への統合も提案している
  • デモ

銀行口座の振込フローのプログラムがデモで実行されました。

kuhn2

  • Q&A
    • scalaz-stream との関連はあるのか
      • インスピレーションを受けてはいるが、Reactive Stream は別のものを目指している

[12:00] ランチ

ビュッフェ形式で肉も魚もなんでもあり。
スイーツがおいしかったです。


[13:00] Learn you an sbt for fun and profit!

  • スピーカー: Daniel Westheide – @kaffeecoder
  • スライド
  • コード
  • 基本的な SBT の使い方

  • Setting[T], Task[T] について
  • 独自プラグインの作成方法
    • 例として、リリースノートを自動で生成するプラグインを作成
  • 便利なプラグインの紹介
    • sbt-revolver: sbtシェルのバックグラウンドでアプリケーションを実行して監視
    • sbt-updates: Mavenリポジトリを参照して、依存ライブラリの更新をチェック
    • sbt-license-report: プロジェクトで使われているライブラリのライセンスを報告
    • sbt-git: sbtシェルから直接 Git の操作を可能にする

[14:00] akka-http: (un)REST for your Actors

  • スピーカー: Mathias Doenitz – @sirthias
  • スライド

  • akka-http とは

    • spray.io を改善したもの
    • Reactive Stream を使用した HTTPモジュール
    • 並行・分散処理を簡単にする、という Akka の思想を受け継いでいる
  • akka-http サーバ/クライアントAPIの利用方法の説明
    • パイプライン処理
    • エンティティが読み込まれる前にレスポンスを返すことも可能
  • Q&A
    • 次期バージョンのリリース次期は未定
      • HTTP2.0 の対応はその後
    • 現時点で、これから(プロダクション環境向けに)新しいプロジェクトを始めるとしたら Spray と akka-http のどちらを使うのがよいか。
      • akka-http の機能がどうしても必要という場合を除いて、現時点では安定している Spray を推奨する

[15:00] Lightning-Fast Standard Collections With ScalaBlitz

スピーカーはEPFLの方。

  • Scala のコレクション操作は Java と比べてなぜ遅いのか
    • とあるコード例で Scala が遅い原因を分析
      • 引数および結果のボクシング
      • foreach, reduce 関数の動的ディスパッチ
      • イテレーションそのものではなく、メソッド呼び出しのオーバーヘッドが大きい
  • ScalaBlitz を使えば、optimize {} を付けるだけで性能向上
    • 並列コレクションも大幅に性能アップ
    • Range, Array は顕著に性能改善、他のコレクションにも効果あり (スライド55ページ参照)
  • ScalaBlitz はマクロ(準クォート/quasiquotes)を使ってコードを解析し最適化されたコードを生成している

[16:00] Simplifying Scala — The Past, Present and Future

スピーカーは Scala のイシューを管理している方。
Scala言語そのものの進化の軌跡を辿るセッションです。
立ち見が出るほど大盛況でした。

  • Scala が目指す方向性
    • シンプルに、一貫性のある形に
    • 学習曲線を緩やかに
    • 落とし穴(ハマりどころ)を少なく
  • イシューの影響度と頻度を考慮して優先順位付けをしている

  • 過去のイシュー対応
    • 暗黙的なUnit型の挿入をなくす
    • 浮動小数点記法の改善 (1 .+(2)1.+(2) の違いに気づかせる)
    • 8進数リテラルを非推奨に
    • for 糖衣構文中の val 使用に関する曖昧さを排除
  • 現在のイシュー対応
    • プロシージャ構文の改善
    • View Bounds (<%) を非推奨に (implicit パラメータを推奨する)
  • 今後のイシュー対応
    • map関数のパラメータなどで、=> の左側のタプル指定をデフォルト不可に
    • 情報落ちの発生する暗黙的な型変換に対する警告
    • 列挙型
      このような構文を検討中とのこと。

  • デフォルトのインポートの改善 (使われない/使えない インポートが含まれている)

  • Avian VM というJVM互換の軽量なVMを開発中

    • 試してみてください、とのこと

[17:00] Spores: Towards Function-Passing Style in the Age of Concurrency and Distribution

発表者は Heather さんという女性の方。現在EPFLの博士課程で、Odersky氏とともに Scala チームの一員であるそうです。
(そういえば Coursera のコースでも色々サポートされていました)

とてもオシャレなスライドでした。フォントの使い方とか、(真似できないけど)勉強になります。

  • 現在の2つのトレンド
    • データセントリック (コールバック、リアクティブ、クロージャ)
    • 関数型プログラミング (不変なデータに対して関数を適用する)
  • クロージャをそのまま分散処理するのは難しい
    • いくつもの頭痛の種
    • Scala に限った話ではない
    • シリアライズ不能な具体例

h1

  • Spores とは
    • 移動可能な関数の振る舞いの小さなパーツ
    • 分散/並行実行環境でクロージャのような抽象化を実現
    • メモリリークやレースコンディション、シリアライズのエラーのない、安全なクロージャを目指す
    • Spore の中身はローカル変数、とクロージャのみ
  • デモ
    • 車種の提案用の検索ツール (車の条件(色・価格帯など)を入れるとマッチするものが返ってくる)
    • クライアント・サーバ間で一定のやりとりが発生する場合、Spore を送ればいい
    • 従来のような個々のマッピングがいらない
    • クライアントサイド(JavaScript) <-> サーバサイド(Scala) で通信する例
    • RDD (Resilient Distributed Dataset) も扱いやすい

懇親会

アレキサンダープラッツ駅近くの Weekend Club の屋上で開催。
エレベーターでビルの最上階まで行き、さらに長い階段を上った先が会場でした。

ビールと3種類の料理が振る舞われ、参加者同士が自由に歓談するスタイル。
私も数名の方と会話したのですが、意外と普段 Scala をメインで使う方ばかりではなかった、という印象を受けました。

さる大学の講師の方いわく、一般的な生徒に教えるには難しすぎる、とか
またとある方は Java がメインの大企業で、Scala の導入がなかなか進められず苦労している、とか。

  • ベルリンのシンボル、旧東ドイツのテレビ塔と美しい夕日

  • 空撮もあったんですね

<

p>つづく


  • おまけ: 次回予告

Scala Days 2014 に参加してきました (1)


Scala というプログラミング言語がこの世に誕生してちょうど 10年。
その Scala にまつわる世界最大のカンファレンスといえば Scala Days!

今年は 2014年6月16日〜18日の期間、ドイツはベルリンで開催され
私も参加者の一人として現地の熱気を生で体感してきました。

本ブログでも、その雰囲気を少しだけお伝えしようと思います。

blog1

1日目


実は私は今回初めてヨーロッパを訪問したのですが、ベルリンの気候は北海道と同じくらい。
昼間は半袖のTシャツ一枚で平気ですが、夜1になると何か羽織るものがないと肌寒いです。

そんなわけで街並みの美しさや、改札のない鉄道網に感動しつつ会場の Kosmos Berlin へ。

blog2

この日は前夜祭といった趣で、講演は Martin Odersky 先生のキーノートだけ。
ドイツ名物のビールも振る舞われて、既に盛り上がっています。
そして夕方 16:30、いよいよ開幕です。

blog3

800人の世界中のScala愛好者が一堂に会しました。

連絡事項など

まずは Josh (Joshua Suereth @jsurerth)が壇上に立ち挨拶と連絡事項について話がありました。
内容は以下のとおり。

  • 挨拶とこの日の段取りについて
  • Scala Days App のデモ

<

p>Android/iPhone 向けのアプリの紹介。
セッションのスケジュールを確認したり、参加者全員の名札に印刷されたQRコードをスキャンしてコンタクト情報を共有することができたりします。

  • セッション投票

セッションが終わると扉の出入口にいるスタッフがスマートフォンをかざしています。
そこには、悪い・普通・良いの三段階のアイコンが表示されており、参加者はタッチするだけで
評価を投票することができました。

  • Phil Bagwell Award

私は知識がなかったのですが、Scala 草創期からの貢献者 Phil Bagwell氏 にちなんだ Scala コミュニティ主体の賞のようです。
受賞者は Kojo というプログラミング言語の作者、Lalit Pant さん。

blog4

キーノート: Martin Odersky

そして、いよいよ Martin Odersky 先生が入場。

スライドは SFScala で発表されたもの と同じだったようです。

blog5

タイトルは、Scala – The Simple Parts。要旨は以下になります。

  • Scala が誕生して10年

多くの開発者によって大きな成長を遂げ、現在は『スケーラブル』な言語になっている

  • 『スケーラブル』の定義

言語自体が進化できること: DSLによる特殊化 – sbt, scalaz, specs, akka など
伸張自在であること: システムの規模に関わらずでも同じように使えること、小規模から大規模なシステムへスムーズに移行できること

オブジェクト指向 + 関数型 という特性が、これを可能にしている。
でも、本当に正しく使えているのか?

  • Scala は Modular 言語でもある

基礎的なパーツ(通常一つの機能だけを持つ)の組み合わせで複雑なシステムを表現できる。
関数やオブジェクトが必ずしも1個のモジュールに対応するとは限らない。

  • シンプル is not 簡単

小さな部品の組み合わせを効果的に行うための具体的なコーディングパターンを紹介。
compose – match – group – recurse – abstract – aggregate – mutate

一つの式で複雑な処理をせず、小さな関数にして意味のある名前を付けよう
暗黙的引数(implicit parameter)を使って抽象化しよう、など。

  • 静的な型チェックの目的

Clojure / Scala / Haskell / Idris / Coq の5つを比較。
正解はなく、トレードオフの関係にあるとのこと。

  • ではモジュールとは何か

自由に組み合わせ可能な小さなパーツ。色々な姿で表現される。
関数 / オブジェクト / クラス / アクター / ストリーム変換 / マイクロサービス

参加者との質疑応答の中で、Scala の将来についての話も出ましたが
言及されたのは Java8 への追従ということのみ。他はアイデアの検討段階だそうで、Scala 3 の登場はまだ先になりそうです。

ワールドカップ ストリーミング観戦

この日は奇しくもサッカーW杯ブラジル大会でドイツ代表の初戦が行われた日。
相手はポルトガルと好カードです。
18:00 にキックオフとなった試合は会場の壁に映し出されると同時に、ビール片手の多くのエンジニアの耳目を集めていました。

blog6

結果は4対0とドイツの大勝だったこともあり、会場は大変盛り上がりました。

つづく

  1. 日没が21時過ぎなので夜は短い []

ScalaNLP/Breeze入門 2


ScalaNLP/Breezeの使い方の第2回です。

ScalaNLP/Breezeが何かとか、インストール方法などについては第1回をご覧下さい。

Breezeを用いた行列とベクトルの復習

簡単な例として、2行2列の例で説明しましょう。

オブジェクトの生成

breezeでは下記のような(密)ベクトル

\( \displaystyle x = \left( \begin{array}{c} 1 \\ 2 \end{array} \right) , \; y = \left( \begin{array}{c} 3 \\ 4 \end{array} \right) \)

と書く事が出来ます。

下記のような(密)行列

\( \displaystyle A = \left(\begin{array}{cc}
2 & 3 \\
1 & 2
\end{array}\right), \;
B = \left( \begin{array}{cc} 3 & 4 \\ 2 & 3 \end{array}\right)\)

を定義するには、行ベクトル(横ベクトル)を縦に並べて表現します。

加減算、積など

行列の加減算は通常の +, - といった演算子が使用出来ます。また行列の積も * で計算出来ます。

\( \displaystyle
x+y = \left( \begin{array}{c} 4 \\ 6 \end{array}\right), \;
A+B = \left( \begin{array}{cc} 5 & 7 \\ 3 & 5 \end{array}\right), \;
AB = \left( \begin{array}{cc} 12 & 17 \\ 7 & 10 \end{array}\right), \;
Ax = \left( \begin{array}{c} 8 \\ 5 \end{array}\right)
\)
は、

となります。

要素の取得、スライス

行列 \(A\) の要素を取り出したり、その部分(slice)を取り出す事も出来ます。行列 \(A\) をa で表すならば、\(A_{ij}\) は a(i,j) で表現されます。但し数学と違って添字が1-originではなく0-originであることに注意する必要があります。要素やスライスを取得する例は下記の様になります。(ここだけ判り易い様に3行3列の行列を使ってます)

各行や各列のsliceを作るには別の記法もあります。こちらの方が判り易いかもしれません。

mutable object

行列やベクトルは、メモリ使用量や効率を考えmutable objectとして作成されます。従って要素を変更可能です。またsliceは元のobjectを参照しているので下記の様にzの変更を通じてcが変更されます。また*=の様な自分自身を更新する演算子も多数用意されています。

逆行列

逆行列などを計算するにはDouble型の行列である必要があります。

\( \displaystyle A = \left(\begin{array}{cc}
2 & 3 \\
1 & 2
\end{array}\right), \;
B = \left(\begin{array}{cc}
3 & 4 \\
2 & 3
\end{array}\right),
\;x = \left(\begin{array}{c}
1 \\
2
\end{array}\right)
\)

を下記の様に定義します。

\(A\) の逆行列 \(A^{-1}\) はinv(a)で計算出来ますが、\(A^{-1}B, \; A^{-1}x\) と逆行列を用いて計算したいだけの場合は、a \ b, a \ x\ という演算子を用いて逆行列を計算しない事が推奨されています。

\( \displaystyle A^{-1} = \left(\begin{array}{cc}
2 & -3 \\
-1 & 2
\end{array}\right), \;
A^{-1}x = \left(\begin{array}{c}
-4 \\
3 \end{array}\right), \;
A^{-1}B = \left(\begin{array}{cc}
0 & -1 \\
1 & 2
\end{array}\right)
\)
は下記の様になります。

不思議の国のAnsible – 第4話


 
logo


不思議の国のAnsible1

第4話 全ては脚本のままに

 

前回より続く

 

はじめての playbook

 


アリスは レベルが上がった!

コマンド ansible-playbook を手に入れた!
モジュール yum をおぼえた!


icon_bob01よしっ、それでは早速 playbook を書いていこう!
icon_alice01はい! お願いします!
icon_bob01と、その前に……以前 ansible コマンドを実行したとき
SSH接続のための鍵の設定をしたのを覚えてる?
icon_alice01はい。
icon_bob01実は、鍵の設定を Ansible の hosts ファイルに書いておくこともできる。
こうすれば playbook を実行するときにもその鍵を使ってログインできるんだ。

/etc/ansible/hosts

icon_bob01このように、ansible_ssh_user と ansible_ssh_private_key_file を指定しておこう。
icon_alice01はい。できました。

icon_alice01ちゃんとつながりますね。
icon_bob01よし、ではこのような YAML ファイルを作ってみよう。
04-01.yml

icon_alice01たったこれだけですか?
icon_bob01うん。playbook として必要な最低要素はこれだけなんだ。

まず最上位にシーケンスを作って、その中にマッピングを書く。
マッピングには hosts と tasks という 2つの名前が定義されているね。

hosts には値を文字列として書いて、
tasks にはさらに内部にシーケンス書く。そのシーケンスの中身が、ping という名前のマッピングだね。

icon_alice01きちんと YAML のフォーマットに沿っていますね。
icon_bob01hosts の箇所には、どのサーバに対して処理を行うかを書く。
今回は all と書いてあるので、さっき書いた Ansible の hosts ファイル中に登録されている全てのサーバが対象となる。

tasks には、実行すべきモジュールとそのパラメータをシーケンスとして書くんだけど
ping モジュールはパラメータを必要としないので、値は空になっている。

tasks の直下のシーケンス一個一個がそれぞれタスクとして認識されるんだ。

icon_alice01Python で構造をチェックしてみますね。

icon_alice01ping に対応する部分には None が入るんですね。

それでは、実行してみましょうか。

icon_bob01ちょっと待って。その前に構文チェックをしてみよう。

環境によっては以下のようなメッセージが表示されることがあります。
これは EPEL のビルド済みパッケージのバージョンが原因で表示される警告であり、対応するライブラリ(gmp)を更新すれば解消されます。

Ansible の動作上は問題ないのでメッセージは無視して構いません。

icon_bob01このように表示されればOKだ。

icon_alice01大丈夫でした!
icon_bob01ちなみに、例えば hosts を書き忘れるとこんな感じになる。

icon_alice01書き間違いにすぐ気づけるのは便利ですね。
icon_bob01–list-hosts や –list-tasks も、事前に情報を確認するための便利オプションだ。

icon_bob01では playbook を実行してみよう。ansible-playbook コマンドのパラメータとして YAML ファイルのパスを渡すだけでいい。

icon_alice01ok と結果が返ってきましたね。
icon_bob01おめでとう!
ちなみに -v オプションを付けると、詳細な情報を表示できる。
-vv , -vvv まで 3段階で詳細度を変えられるよ。


 

playbook を繰り返し実行する

 

icon_bob01次は、新しく覚えたモジュール yum を使ってみよう。
icon_alice01はい。
icon_bob01これは、その名の通り yum コマンドを ansible で実行するためのモジュールなんだ。
icon_alice01ansible-doc で使い方を調べると、具体的な使用例が出てきました。

icon_bob01だいぶ慣れてきたようだね。
今回はそうだな……Webサーバの Nginx2をインストールしてみようか。
icon_alice01あ、はい。Nginx は使ったことがありますっ!
icon_bob01標準リポジトリにはないので、まずは EPEL リポジトリをインストールして、
その後で Nginx をインストールする YAML ファイルを書くよ。
icon_alice01わかりました。
icon_bob01ping モジュールの時と同じように tasks の下のシーケンスに yum と書いて、値にこんなふうに書いてみよう。
04-02.yml

このように パラメータ=設定値 という形式で書くことで、Ansible の中でモジュールのオプションを指定することができるんだ。

icon_alice01なるほど。name に指定するのは URL でもパッケージ名でもいいんですね。
icon_bob01その通り。
icon_alice01state=present というのはどういう意味ですか?
icon_bob01パッケージがインストールされていなかったら最新版をインストールして、
既にインストールされていたら何もしないという意味だよ。

他のオプションとしては、常に最新版をインストールする state=latest、
パッケージを削除するための state=absent がある。

icon_alice01では実行してみますね。一応構文チェックもやってみます。

icon_alice01あら、エラーになってしまったみたいです。
icon_bob01あ、そうだ、yum コマンドの実行には root 権限が必要だったんだ。

こんなふうに sudo: True という項目をマッピングに追加すれば、サーバ上の全てのコマンドを sudo 付きで実行してくれるよ。

icon_alice01はい。
icon_bob01そうそう、ansible-playbook には –check というオプションもある。

実際の変更を一切行わずに、どのような挙動が起こるかをあらかじめチェックできるんだ。

icon_alice01やってみます!

icon_alice011個エラーになってしまいました。
icon_bob01メッセージをよく見てごらん。
‘nginx’ というパッケージが見つからなかったみたいだけど、まだ EPEL をインストールしていない状態なのでこれは仕方ないんだ。

他は大丈夫そうだね。では本番、実行してみよう。

icon_alice01はい。

icon_alice01うまくいったみたいです!
changed=2 というのが 2つのパッケージのインストールが成功したという意味でしょうか。
icon_bob01ためしにもう一度、同じコマンドを実行してごらん。

icon_alice01今度は changed=0 になりました。
TASK の下の行も changed から ok に変わりましたね。
icon_bob011回目はまだインストールされていない状態なので、インストール処理、つまり変更が行われた。
それが成功したので「changed」と表示されたんだ。
2回目は既にインストール済みで、それが正しい状態であるので変更は行われず、
「ok」とされた。

こんなふうに、何回やっても状態が変わらないから、playbook を繰り返し実行しても安心なんだ。

icon_alice01なるほど。
icon_bob01実際に Nginx がインストールされたか確かめてみる?

icon_alice01ちゃんと、EPEL 経由で Nginx がインストールされています。
icon_bob01よかった。これで一安心だ。
あと、細かいところだけど表示されるタスクの表示名は、YAMLファイルで
こんなふうに指定することもできる。
04-03.yml

icon_alice01動かしてみます。

icon_alice01表示がだいぶスッキリしました……
ほんと、同じタスクを何度も動かせるのはいいですね。
icon_bob01「今どこまでやったっけ」ということを気にする必要がないからね。
特に、前回の作業から一定の期間が空いていたりするサーバだと、ありがたみが倍増する。
icon_alice01Ansible の世界の心地よさがちょっとだけ分かった気がします。
これから、playbook の使い方やモジュールをもっと覚えていきたいです。
icon_bob01Ansible の構成はすごくシンプルだから、アリスならきっとすぐにマスターできるよ!
icon_alice01ありがとうございます!

満足感に包まれたアリスは眩しい光に包まれていく。
するとアリスはこの不思議な夢から覚めて、日常の世界へと戻っていた。

次回へつづく

 
最後までお読みいただき、どうもありがとうございました。


  1. 画像素材 http://kage-design.com/wp/ []
  2. http://nginx.org/ja/ []

FLOPS2014報告


 FLOPS2014 に行ってきました、といっても発表しに行った訳でなく単に話を聞きに行っただけなんですが。

 FLOPS 2014 は二年に一回、日本で開催される関数型および論理型プログラミングに関する国際会議です。今年は6/4-6の日程で石川県金沢市で開催されました。
 弊社はアドテクの会社で開発言語もScalaだったりと、まぁほとんど会社の業務と関係無いのだけど、やはりせっかく日本で関数型言語の国際会議があるなら是非聞きに行かないとね、ということで聞きに行きました。

 以下、感想などです。各発表内容に関しては、プログラムのページから発表スライドを見る事ができるはず。

第1日目

★ “Liquid Types For Haskell” 招待講演
 今回のFLOPSで一番興味を持っていたのがこの話です。
 Liquid = Logically Qualified Data の略、のつもりらしく、liquid type というのは、{v: Int | v >= 0} の様に、論理式で修飾された型のことです。Coq などの依存型を用いた定理証明系でもこのような述語を伴った型を使ってプログラミングを出来るところは同じなのですが、liquid type は述語を決定可能なPresburger算術の範囲に限定し、SMTソルバーを用いて自動証明をさせようというところが大きく違います。まぁCoqの証明を書くのは大変だし、開発の現場で必要とされる検証課題はほぼPresburger算術で充分なのだとしたら、自動証明の方が普及までの敷居が低いのは自明。
 LiquidHaskell がどんなものか試したい人はオンラインでどんなものか試すことが出来ます。
liquid type の型定義は、{-@ type Even = {v:Int | v mod 2 = 0} @-} みたいにHaskell のコメントとして、実際のHaskellのコードに註釈します。すると double xs = [x + x | x <- xs] のようなHaskellの実装について、{-@ double :: [Nat] -> [Even] @-} の様な仕様を満たすことを自動証明してくれる、というのを試せます。
 個人的には Coq で証明を書くの好きなんだけど、やはり前の会社(SIer)や今の会社で仕事をしてみた印象としては、自動証明器も必要なのかなぁとも思います。ならば Why3 とか使って開発すれば良いかなとも思うけど、Haskell みたいに既にメジャーな言語でこの手のツールが使えるというのは、やはり強みなのかなぁと思います。

他の発表は簡単に(というか専門家じゃないから解説なんか出来ない)。詳しくは、proceedings読んで下さい。

★ “PrologCheck – property-based testing in Prolog”
 オブジェクト指向言語界隈では具体的なテストケースに対してユニットテストをすることが多い様ですが、関数型言語ではランダムにテストデータを生成して仕様(=満たすべき性質)を満たすことを確認するようなproperty-baseのテストツールが標準的です。(ScalaでもScalaCheckというのが有りますが、開発現場ではあまり使われてないみたい。勿体ない話です。)
 で、Prolog版のを作った、という話(だと思う)。

★ “Generating Constrained Random Data with Uniform Distribution”
 で、その手の XXX Check系のテストツールには、「もし入力データが◯◯という性質を満たすなら△△」みたいなのをテスト出来るのですが、◯◯という条件を満たすランダム入力データを作るのはなかなか面倒だったりします。その辺を工夫したよ、という話(だと思う)。

★ “Guided Type Debugging”
 関数型言語のエラーメッセージは、(C++ほどではないと思ってはいますが)Javaとかに比べると判りにくいところがあります。その原因の一つの、型の不整合の時のエラーのデバッグを容易にしようとする工夫(だと思う)。

★ “Using big-step and small-step semantics in Maude to perform declarative debugging”
 Maude (という項書き換え系言語)の上に、何か言語の big-step あるいは small-step semantics を定義して実行とかデバッグとか出来るフレームワークを作った、という研究の様に思えた。確かに small-step semantics とか Maude の上に定義すると便利そうに思えますね。

★ “Faustine: a Vector Faust Interpreter Test Bed for Multimedia Signal Processing – System Description -”
 Faust というのは信号処理用のDSLらしいのですが、これを使ったギターアプリ(タブレット上で動くギター風に演奏出来るアプリ)の動画デモが。こんな研究してる人もいるんだなー、と思いました。

★ “The Design and Implementation of BER MetaOCaml: System Description”
★ “On Cross-Stage Persistence in Multi-Stage Programming”
 MetaOCaml というのは OCaml を拡張して型安全 eval を使える様にしたようなものなのですが、それに関する発表が2件。

第2日目

★ “Programming Language Methodologies for Systems Verification” 招待講演
 L4 microkernel を作ってる研究機関での形式手法仕様に関する報告。当初OS班と形式手法班がIsabelle/HOLを使おうとして失敗し、Haskellを両者の共通言語として選択したら成功して、両者の共通言語としてのHaskellからIsabellあるいはC++を作る様になった(しかしその後、各班がHaskellをメンテしなくなって云々)みたいな報告。
 この手の話聞くと、OS班とはいえ研究者の方々でも、やはり Isabelle などの形式手法(定理証明系)とかで仕様記述するの嫌なのか、と思ってしまいますね。。。IsabelleはZとかほど抽象的ではないと思うのだけれどなぁ。あと、線形型は勉強した方が良さそうだなと思った。

★ “Lightweight higher-kinded polymorphism”
 OCamlには無いhigher-kinded polymorphismをdefunctionalizationすることで実現したよ、という話。

★ “Generic Programming with Multiple Parameters”
 HaskellのGeneric programmingでパラメータを複数個使える様に、という話。うーむ、Haskellのgeneric programmingの話、ちゃんと復習しないとなー。

★ “Type-Based Amortized Resource Analysis with Integers and Arrays”
 計算量というリソースを型として表現するという話。こういうことも出来るのか、と。

★ “Linear Sized Types in the Calculus of Constructions”
 CoqのInductionの停止性、CoInductionのproductivityの判定の為に、それらを表現出来るような型を、という話。

★ “Dynamic Programming via Thinning and Incrementalization”
 ナップザック問題を例にとってDPの解法アルゴリズムを、融合変換とかアルゴリズム変換とかを使ってアルゴリズムを最適化する話。この手の話に興味がある人は、”semiring fusion” とか “第三準同型定理” とかのキーワードでググると良いと知人より教わりました。勉強すること多いなー。

★ “POSIX Regular Expression Parsing with Derivatives”
 微分を用いて正規表現を扱う話は知っていたのですが、POSIX準拠のはずの各種正規表現ライブラリが、どこで部分文字列をマッチすべきかについて正しく無い答えを返す、という話は知りませんでした。ちゃんとPOSIX仕様に基づいて、部分マッチ箇所を計算するアルゴリズムの話です。Proceedingsにはプレゼンでは端折ってあった箇所が書かれてて面白そうなので、あとでちゃんと復習しよう。

★ “Semantics for Prolog with Cut – Revisited”
 Cut有りのPrologのsemanticsをCoqでやってる、という話。すみません、Prolog良く解らないので、どの辺が重要なポイントなのか判りませんでした。

★ バンケット
 コース+追加で寿司、天ぷら、日本酒という立派なバンケットでした。線形論理の話とか面白い話を聞けました。

第3日目

★ “Relating Computational Effects by TT-Lifting” 招待講演
 計算(computation)を扱う理論的枠組みとしてdenotational semanticsというのがあるのですが、圏論を使って色々統一的に議論出来るよという話で、最初は判る話だったんですが、後半はさすがに振り落とされました。が、こういう話聞くと、また圏論勉強しよう、という気分になりますね。

★ “A New Formalization of Subtyping to Match Subclasses to Subtypes”
 継承とジェネリクスと両方ある Java とか Scala みたいな言語だと、型宣言の際に共変反変の両方の制約を満たす為に(例えばScalaなら) sealed abstract class List[+A] extends ... { def ::[B >: A] (x: B): List[B] = ... } みたいなイディオムを使わざるを得ないとか色々不便なところもあるのですが、この論文は新しい subtyping の定式化をしてみたよという話。OO言語関係に近い話題はこの一件だけでした。Scala などに興味がある人は ECOOP とか聞きに行くべきなんですかね。。。

★ “Type Soundness and Race Freedom for Mezzo”
Mezzo というのはML風の言語なんですが、線形型を用いることでマルチスレッドプログラミングでロック取得の必要性などをコンパイル時にチェック出来る様にした言語で、言語の正しさ(型検査が通ればデータ競合が起きない事)を Coq で証明した、という話。Java とか Scala とかだとプログラマが正しくロックを取ってる事を保証しなくてはいけないので、Mezzo のこういう機能は素晴らしいと思います。

★ “Proving Correctness of Compilers using Structured Graphs”
 木構造ではなく(非循環)グラフを用いてコンパイラを改善するみたいな話で、グラフを用いてコンパイル&実行するのと、木も用いてとが等価だと言う証明の話(だと思う)。

★ “Constraint Logic Programming for Hedges: a Semantic Reconstruction”
 すみません、これは良く判りませんでした。semantics と solver のアルゴリズムについて話してたと思うのだが。

★ “How many numbers contains a lambda-term?”
 λ式でk-tupleとかを作った場合、λ式の型を決めると、そこに含む事の出来る自然数の個数には上限がある、という話(だと思う)。これも難しくて判りませんでした。

★ “AC-KBO Revisited”
 項書き換え系にはクヌース・ベンディックス完備化アルゴリズムという完備化アルゴリズムがありますが、結合則 x+(y+z) = (x+y)+z や交換則 x+y=y+x のような規則を満たす演算子に関する場合にどうするかという話。Steinbach という人の論文が間違っているという論文があったけど実はそれは正しくてみたいな話とか、順序付けがNP-hardなことはこうやってSATに変換してとか、(詳細は理解出来ない)門外漢にも楽しめる発表でした。

★ “Well-structured pushdown system: Case of Dense Timed Pushdown Automata”
 Timed Pushdown Automata の話でした。これも基礎知識が無くどういう話なのか良く判りませんでした。

終わりに

 社外勉強会の効能として、「今まで知らなかった話題に触れられる」「すごい人たちのやってるすごいことを知る」「もっと勉強しようというやる気を貰ってくる」といったことを主張する人は多いです。私もその意見に賛成します。
 だとしたら、学会とか国際会議に行けば、第一線の研究者がやっている最先端の話題を知る事が出来ます。
 そして、例えばHaskellとかOCamlなどは、言語の開発者がこういう学会で発表した事を言語の新機能として追加したりします。学会で話されている事は自分が使う機能と無関係な難しい話ばかり、という訳ではありません。
 
 勿論、聞いても分からない話も一杯有りますし、周りは見知らぬ研究者ばかりで話す相手も内容も無い、などなどというところはありますが、まぁその辺は我慢するとして。判らなかった内容とかは、各種勉強会とかに行って論文コピー片手に詳しそうな人に質問するとか方法はありますし。

 2016年のFLOPSは高知で春に開催だそうです。また PPL のような日本の学会とかなら敷居が低く感じるかと思います。

 社外勉強会に行く次のステップとして、学会とか国際会議を聞きに行くのを是非お勧めします。

不思議の国のAnsible – 第3話


 
logo


不思議の国のAnsible1

第3話 脚本のつくりかた

 

前回より続く

 

YAML Ain’t Markup Language

 

icon_alice01でもこうやってコマンドを実行できるのは確かに便利ですけど、
手で作業するのとあんまり変わらないような気もします……
icon_bob01うん、実はサーバの構築や運用にあたって ansible コマンドを直接実行
する場面はほとんどない。
Ansible では あるべき状態をファイルに記述して、それを実行するという
スタイルが普通なんだ。

icon_bob01ところでアリス、きみは普段の仕事でメモを取っているかい?
icon_alice01ええ。メモアプリ使ったり、手書きでノートに書いたり……とか色々ですけど、なるべく書くようにはしていますね。

『自分の行動を記録する(ログる)のがインフラエンジニアの基本』ですから。
(先輩の受け売りだけど……)

icon_bob01いい心がけだね。
もしそのメモが自動的に動き出したら、素敵じゃない?
icon_alice01えっ? そんなこと、あるわけないですよ……
icon_bob01その動かせるメモが playbook なんだ。
icon_alice01動かせる……なるほど! 勝手に働いてくれる手順書みたいなものですかね。
icon_bob01最初はメモだったものも、積み重ねるとやがて壮大な脚本になっていく。
とはいえ千里の道も一歩から。まずはフォーマットを覚えることからはじめよう。
icon_bob01playbook は、YAML2と呼ばれる形式で書く必要がある。
icon_alice01わいえーえむえる? XML の仲間でしょうか?
icon_bob01さすが鋭いね。XML や JSON のような構造化されたデータの記述方式の一つなんだけど、シンプルで人が読みやすいという特徴がある。
ちなみに「やむる」と読むのが一般的かな。
icon_alice01何の略なんですか?
icon_bob01YAML Ain’t Markup Language。
直訳すると「YAMLはマークアップ言語ではない」となる。
icon_alice01……って、あれ? 説明自体に略称が含まれていますね……結局 YAML の Y って何なのでしょう?
icon_bob01ははは、これはある種の言葉遊びだから 3、そんなに深く考えなくていいさ。
icon_bob01さて、本題に戻ると……
YAML の書き方を覚えて、playbook を書けるようになろう。
ポイントはそんなに多くないけどね。
icon_alice01はい、がんばります!
icon_bob01まずファイルの先頭の行にハイフン(-)を3つ書く。
これが、ここから YAML 文書の記述が始まる、という合図になる。

icon_alice01はい。
icon_bob01次に、シーケンスの書き方。
他のプログラミング言語で配列とかリストとか呼ばれる概念に近いけど、同じ階層の要素を順番に並べて書くときに使う。
行の先頭にハイフン(“-”)と半角スペース(” “)を書いて、その後に続けて内容を書くよ。
03-01.yml

icon_alice01はい。ファイルを作って書いてみました。何か確認する方法はあるのでしょうか?
icon_bob01やり方は色々あるけど……
そうさね、たとえば Python を使って YAML を読み込んでみよう。
さっきの内容を 03-01.yml として保存してこんなコマンドを打てば
Python のオブジェクトとして解釈された内容が表示される。
そうそう、ファイルの拡張子は “.yml” を使うといいよ。

icon_alice01やった! うまくいきました。
icon_bob01内容をシングルクォーテーション(‘)やダブルクオーテーション(“)で囲むと、
内部的に文字列として扱われるようになる。
今回はもともと文字列なので、同じ結果になるね。
03-02.yml

icon_bob01シーケンスの値として、中にシーケンスを入れることもできるよ。
03-03.yml

icon_bob01この場合、インデントの位置によって階層が決まっていくんだ。
インデントはスペース2個にすることが多いね。
icon_alice01あれっ? 何だかエラーが出てしまったみたいです。

icon_bob01アリス、作ったファイルを見せてくれるかい?
icon_alice01あ、はい。これなんですけど……
03-04.yml (フォーマットエラー)

icon_bob01フムフム。ファイルをよく見てごらん、一箇所インデントがずれているところがあるよ。
icon_alice01ほんとだ…… b2の部分ですね。ハイフンの前のスペースが1個足りませんでした。
icon_bob01このように、YAML ではインデントの位置が厳しくチェックされる。
インデントとしてタブ文字を使ってもエラーになるから注意してね。
icon_bob01次はマッピングを使ってみよう。
マッピングというのは、要は名前と値の組み合わせで、他のプログラミング言語におけるハッシュマップとかマップ、ディクショナリ、キーバリューペアと呼ばれる概念に対応するものだ。

まぁ例を見せたほうが早いか。こんな感じで、名前と値をコロンで区切って記述するよ。

03-05.yml

icon_alice01表示される順番が変わりましたね。
icon_bob01うん、マッピングの場合、値にアクセスする時にはその名前(キー)だけが手がかりになる。
書いた順番は評価されないんだ。

逆に、同じ名前(キー)を同じ階層で複数書くと正しく認識されない4 ので気をつけよう。

icon_alice01はい。
icon_bob01シーケンスとマッピングを組み合わせると、こんなふうに構造化されたデータが作れる。
03-06.yml

icon_alice01直感的で分かりやすいですね!
icon_bob01シーケンスとマッピングの書き方さえ覚えれば、もう YAML はほとんどマスターしたようなもんさ。

そうそう、さっきのファイルだけど、True や False というキーワードは
文字列でなくて真偽値(ブール値)として評価されている。このようなキーワードは他にもあるんだ。

プログラムでどのように評価されているか、注意深くみてほしい。

03-07.yml

icon_alice01なるほど。よくわかりました。
icon_bob01# で始まる行はコメントとして扱われ、実際のデータとしては見なされない。
行の途中でコメントを書くこともできる。これは Shell Script や Python と同じだね。
03-08.yml

icon_alice01ちなみに、複数行にまたがる文章をデータとして登録することはできるのですか?
icon_bob01もちろん可能さ。改行を含んだ文章を書くときは、その要素の先頭の行にこんな風に
縦棒(パイプ)を書けばいい。
03-09.yml

icon_bob01\n というのが改行を意味しているよ。
YAMLファイルの 3行目以降、インデントを揃えることに注意してね。
icon_alice01ありがとうございます。
だいたい YAML の書き方をイメージできるようになりました。
icon_bob01素晴らしい! どうやらまたレベルアップしたみたいだね。


アリスは レベルが上がった!

コマンド ansible-playbook を手に入れた!
モジュール yum をおぼえた!


icon_bob01よしっ、それでは早速 playbook を書いていこう!

次回へつづく

 
最後までお読みいただき、どうもありがとうございました。


  1. 画像素材 http://kage-design.com/wp/ []
  2. The Official YAML Web Site []
  3. 再帰的頭字語 – Wikipedia []
  4. あとに書いたもので上書きされる []

不思議の国のAnsible – 第2話


 
logo


不思議の国のAnsible1

第2話 忠実な兵士たち

 

前回より続く

 

はじめての Ansible コマンド


アリスは レベルが上がった!

コマンド ansible を手に入れた!
コマンド ansible-doc を手に入れた!
モジュール ping をおぼえた!

icon_bob01おめでとうアリス!
新しいコマンドとモジュールを手に入れたみたいだね。
icon_alice01コマンドは、OS から実行可能なコマンドという意味ですよね?
モジュールっていうのは、コマンドとは違うんですか?
icon_bob01モジュールっていうのは、Ansible の言葉なんだけど
管理対象サーバ上でどんな仕事をするのか、その命令の種類だと考えればいい。

Ansible では標準で 200以上のモジュールが用意されているし、
必要であれば2自由に拡張することもできる。

icon_alice01よく使う手順のパターンがまとまっている感じですかね。
icon_bob01その通り。ではまず手始めに ping というモジュールを使ってみよう。
icon_alice01ネットワークコマンドの ping とは別物なんですね。
icon_bob01うん、これはネットワークの疎通だけではなくて、Ansible のサービス階層で
対象サーバが利用可能な状態にあるかどうかをチェックできるんだ。
icon_alice01使い方を教えてください!
icon_bob01ansible というコマンドで、実際に管理対象サーバに命令を送ることができる。
書式は ansible 対象サーバのIPアドレス -m ping だよ。

アリスは、この不思議な世界でコマンドを頭に思い浮かべる。
するとどこからともなく奇妙な兵士が現れた。トランプの胴体にハート型の槍を携えている。

icon_alice01コマンド実行!

アリスがコマンドを唱えると、トランプ兵はそそくさとどこかへ帰ってしまった。

icon_alice01あれ? なんだかうまくいっていないみたいです。
icon_bob01あ、そうだった。Ansible では安全のため、あらかじめ指定したサーバ以外には
接続しないようになっている。
それを管理しているのが /etc/ansible/hosts というファイル3なんだけど、
このように、接続先の 192.168.100.12 という1行に書き換えてごらん。

元々書かれている内容は、全部削除して構わないよ。

icon_alice01できました。それでは気を取り直して……

またまた、どこかからトランプ兵が現れる。
今度は管理対象サーバへ繋がる扉の前4まで一目散へ駆け出していった。
ところが押しても引いてもドアが開かず、結局諦めて帰っていった。

icon_alice01あらら、まだダメみたいですね。
icon_bob01今度は SSH の認証に失敗したようだ。
君の秘密鍵は、実はココ (~/.ssh/alice.pem) に隠してある。
それを指定してみよう。
ansible コマンドに –private-key というオプションを付け加えるよ。

三たび現れたトランプ兵は、今度はアリスの目の前に駆けつける。
アリスがトランプ兵に扉の鍵を渡すと、うやうやしく敬礼して扉のもとへ。
今回は無事、扉を開けられたようだ。
程なく戻ってきたトランプ兵はアリスの元へ駆け寄り、「pong」と叫んで報告する。

icon_alice01うまくいきました!
icon_bob01Ansible の出力は、だいたいこんな感じになる。
FAILED の部分が success に変わって、付随する情報が出力されているね。

ちなみに、毎回秘密鍵を指定するのが面倒なら、こんな風に ssh-agent に登録しておくといいよ。

icon_alice01こっちのほうが後々楽になりそうです。
icon_bob01それと、IPアドレスの代わりに all と指定すれば
/etc/ansible/hosts ファイルに書かれた全てのサーバに対して
処理が実行される。
今はまだ管理対象サーバが1つしかないから、挙動は変わらないけどね。

icon_alice01all ですね。覚えておきます。

ドキュメントの参照

 

icon_alice01ところで、ansible-doc ってコマンドもありましたけど、使ってみていいですか?
icon_bob01もちろんだよ!
これはヘルプ用のコマンドで、ansible-doc モジュール名 と実行すれば説明や
使用例をすぐに参照できる。

icon_alice01英語ですけど、なんとなくわかるような、わからないような……
でも使用例が載っているのはありがたいですね。
モジュールの使い方を忘れてしまった時なんかに重宝しそうです。
icon_bob01もちろん、Ansible 公式ドキュメント も素晴らしく充実していて使いやすいよ。

さまざまな実行オプション

 

icon_bob01ansible コマンドの方にもまだまだ色んなオプションがあって……
そうだな、例えば-a オプションを使えば、管理されるサーバ側で
好きなコマンドを実行することができる。

icon_bob01--sudo オプションを使えば、管理対象サーバで root 権限が必要な作業もお手のものさ。

icon_alice01コマンド一つでいろんな事ができるんですね。すごい!
icon_bob01まだまだ、こんなのは序の口。でも雰囲気は掴めたんじゃないかな。
icon_alice01はい。おかげさまで。
私が指示したとおりに、忠実に働いてくれるんですね。
icon_bob01そこが Ansible を使う価値さ。
icon_alice01でもこうやってコマンドを実行できるのは確かに便利ですけど、
手で作業するのとあんまり変わらないような気もします……
icon_bob01うん、実はサーバの構築や運用にあたって ansible コマンドを直接実行
する場面はほとんどない。
Ansible では あるべき状態をファイルに記述して、それを実行するという
スタイルが普通なんだ。

それは、この世界では playbook と呼ばれている。
少し休憩したら、次はその話をしようか。

 

次回へつづく

 
最後までお読みいただき、どうもありがとうございました。


  1. 画像素材 http://kage-design.com/wp/ []
  2. ほとんどの場合は独自のモジュールを作らなくても事足りる []
  3. 正確に言えば、デフォルトの参照先の1つ []
  4. 第1章を参照 []