チェシャ猫の消滅定理

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

Serverless Meetup Tokyo #6 で Kubernetes について話してきました

先日行われた Serverless Meetup Tokyo #6 で、Kubernetes 上で動作する Serverless フレームワーク Fission について発表してきました。

www.slideshare.net

先週も 似たようなブログ を書いたような気がしなくもないですが、KubelessFission を比較した前回の発表に対し、今回は話題を Fission に限定しています。一方で追加要素として、複数の Function を組み合わせるためのアドオン Fission Workflows を紹介してみました。

コンテナの再利用

スライド中でも言及している通り、一度「特殊化」されたコンテナは一定時間そのまま起動しており、再度同じ Function が呼び出された際に再利用されます。すなわち Function がコンテナ内部の環境に対して副作用を持つ場合、良くも悪くも次の呼び出しに影響するはずです。これを実際に確認してみましょう。

以下ではすでに 公式手順 に従って Fission が Kubernetes クラスタ上にデプロイされ、手元で fission コマンドが使用可能になっているとします。

Environment の作成

スライド中で挙げられていたコマンド例は Python でしたが、単純にするためにここではシェルスクリプトを使います。

$ fission env create --name binary --image fission/binary-env:0.3.0
Use default environment v1 API interface
environment 'binary' created

$ fission env list
NAME   UID                                  IMAGE
binary 00386979-b3c2-11e7-b4db-fa163ed87208 fission/binary-env:0.3.0

Function と Route の作成

コンテナが再利用されていることを確かめるために、コンテナ内の状態を変化させるような恣意的な Function を作成します。

以下のコードを counter.sh として保存します。なお公式で用意されている実行環境 fission/binary-env では Bash は使用できず、shebang に sh を指定する必要があるので地味に気をつけましょう。

#!/bin/sh

date >> /tmp/counter.txt
cat /tmp/counter.txt | wc -l

これで呼び出しごとにコンテナ内のファイルに追記が行われるはずです。このソースコードを指定して Function を作成します。

$ fission function create --name counter --env binary --code counter.sh
function 'counter' created

$ fission function list
NAME    UID                                  ENV
counter 217af646-b3c2-11e7-b4db-fa163ed87208 binary

さらに、この Function を呼び出すためのトリガーを作成します。

$ fission route create --method PATCH --url /counter --function counter
trigger '70a978a9-8cf9-42c3-a018-be0234785bc8' created

$ fission route list
NAME                                 METHOD URL      FUNCTION_NAME
70a978a9-8cf9-42c3-a018-be0234785bc8 PATCH  /counter counter

これでエンドポイントが定義されました。fission route create --help で出てくるオプション --method の候補に PATCH は入っていませんが、今回の例では期待した通りに動作します。

Function の実行

さて、この Function を実行してみると、

$ curl -X PATCH http://$FISSION_ROUTER/counter
1
$ curl -X PATCH http://$FISSION_ROUTER/counter
2
$ curl -X PATCH http://$FISSION_ROUTER/counter
3
$ curl -X PATCH http://$FISSION_ROUTER/counter
4

となり、実際に以前の実行の影響が残っていることがわかります。ちなみに 3 分ほど放置すると特殊化されたコンテナが消えるため、カウンタの値はリセットされます。

Kubernetes 側から直接確認してみましょう。プールされている 3 個 + 特殊化された 1 個で計 4 個の Pod があることが分かります。

kubectl -n fission-function get pods
NAME                                                              READY     STATUS    RESTARTS   AGE
binary-00386979-b3c2-11e7-b4db-fa163ed87208-glxmo1iv-189128r9t8   2/2       Running   0          6m
binary-00386979-b3c2-11e7-b4db-fa163ed87208-glxmo1iv-18912fhfp0   2/2       Running   0          2m
binary-00386979-b3c2-11e7-b4db-fa163ed87208-glxmo1iv-18912fpjtc   2/2       Running   0          8m
binary-00386979-b3c2-11e7-b4db-fa163ed87208-glxmo1iv-18912r3qwl   2/2       Running   0          8m

ひとつだけ AGE が若い Pod は、特殊化されて Deployment の管理下から抜けた Pod の穴を埋めるために新しく立ち上がったものです。今回の場合、Function counter 用に特殊化された Pod は 4 番目に表示されているもので、kubectl describe コマンドで確認するとラベルがひとつだけ付け替えられています。

$ kubectl -n fission-function describe pods/binary-00386979-b3c2-11e7-b4db-fa163ed87208-glxmo1iv-18912r3qwl
Name:       binary-00386979-b3c2-11e7-b4db-fa163ed87208-glxmo1iv-18912r3qwl
Namespace:  fission-function
Node:       calico-1/192.168.235.231
Start Time: Wed, 18 Oct 2017 05:05:48 +0000
Labels:     functionName=counter
        functionUid=217af646-b3c2-11e7-b4db-fa163ed87208
        poolmgrInstanceId=T2bveCV8
        unmanaged=true
...

実際にコンテナの中を覗くと、これまでの Function の呼び出しによって生成されたファイルが残っているはずです。

$ kubectl -n fission-function exec binary-00386979-b3c2-11e7-b4db-fa163ed87208-glxmo1iv-18912r3qwl cat /tmp/counter.txt
Defaulting container name to binary.
Use 'kubectl describe pod/binary-00386979-b3c2-11e7-b4db-fa163ed87208-glxmo1iv-18912r3qwl' to see all of the containers in this pod.
Wed Oct 18 05:12:20 UTC 2017
Wed Oct 18 05:12:38 UTC 2017
Wed Oct 18 05:12:39 UTC 2017
Wed Oct 18 05:12:40 UTC 2017

まとめ

Kubernetes 上の Serverless フレームワーク Fission について、間をおかず同じ Function が呼ばれた場合にコンテナの再利用が行われることを簡単な実験で確認しました。

なお発表中ではスライド 1 枚で済ませてしまいましたが、複数の Function でピタゴラスイッチできる Fission Workflows はなかなか面白い仕組みです。いずれちょっとしたサンプルを公開したいと思っていますが、それはまた別の話。

Kubernetes Meetup Tokyo #7 で Serverless について話してきました

先日行われた Kubernetes Meetup Tokyo #7 で、Kubernetes 上で動作する Serverless フレームワークについて発表してきました。

www.slideshare.net

Serverless on Kubernetes を謳うツールはいくつかありますが、今回はそのうち KubelessFission に焦点を当て、それぞれのアーキテクチャの違いを比較してみました。

当日の補足

Twitter 上で反応をもらった点についていくつか補足します。

Function の合成

回答になっているかどうかちょっと自信がないのですが、複数の Function を連鎖させるという意味であれば、ごく最近 Fission Workflow というツールがリリースされています。

github.com

Fission の追加コンポーネントになっていて、Function を他の Function のトリガにするための仕組みです。有名どころで例えるなら AWS Step Functions が近いでしょうか。

クラウド FaaS との比較

正直なところ自分も同じような印象を持ちました。クラウドベンダ各社が提供している FaaS の強みはマネージドサービスとの連携であって、その恩恵に預かれない Kubernetes はだいぶ Serverless のメリットが目減りしている感じです。

現状でメリットと言えなくもない点は以下のふたつ。

まず当然ですが、なんらかの政治的な事情によりパブリッククラウドが使用できない場合でも使用可能な点。どうせなら Serverless フレームワークと互換性があれば環境間の差異が吸収できるのですが、今のところ Fission はこの機能は提供していないようです。ちなみに Kubeless については Serverless Framework Plugin が提供されています。

もうひとつは、Kubernetes の Events をトリガとして使用できる点です。例えば Slack に通知するとか、外部サービスとのちょっとした連携には役に立つかもしれません。現状トリガに指定できる条件は Namespace、Kind、Label のみですが、前述の Fission Workflow と組み合わせて何かちょっとしたサンプルが作れないかと考えているところです。

総論

現状、ものすごく画期的だとは言い難いですが、とはいえ数週間に一回アーキテクチャごと変更されていたり、Fission Workflow のような新しいツールが動き始めていたりして、決して停滞しているわけではなさそうです。まあ今後に期待しておきましょう。

なお Fission Workflow についてはもう少し調べた上で記事にまとめるか、あるいはまた別の場所で LT にでも仕立てようと狙っていますが、それはまた別の話。

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 : 空席

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