読者です 読者をやめる 読者になる 読者になる

チェシャ猫の消滅定理

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

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

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 を使用します。残念なことに現状 安全性の低いアプリからのアクセスを許可 しておく必要がありますが、いずれは対応したい。

コードはこんな感じになります。yourusernameyourpassword は手持ちの 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 連携に興味がある人は、次のスライドが役に立つはずです。

www.slideshare.net

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

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

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

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 がありますね? 自分はここ数年連続して色々なモデル検査ツールの発表をしているのですが、それはまた別の話。

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

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

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

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

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

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

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

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.javaTarai.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 上で再現するために語るべきことは尽きません。いずれこのブログのネタにでもしますが、それはまた別の話。

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

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

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

www.slideshare.net

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

話さなかったこと

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

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

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

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

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

また、開発環境周りでは

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

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

すごい JVM 言語 Frege をたのしく学ぼう!

言わずと知れた Haskell の定番教科書『すごい Haskell たのしく学ぼう!』に登場するサンプルコードを、プログラミング言語 Frege に翻訳してみました。

github.com

Frege について

Frege は、JVM 上で動く純粋関数型プログラミング言語です。

github.com

最近、JVMLisp である Clojure の存在感を増してきている気がしますが、Frege はいわばその Haskell 版ですね。

文法的には Haskell + Javaメソッドを呼び出すための追加構文、といった感じ。細かな違いはありますが、Haskell が読める人間であれば理解に苦労することはないでしょう。実際『すごい Haskell』に登場するコードは、大部分が変更なく Frege に「丸写し」することが可能でした。

逆に、Java 方面から入って初めて関数型に挑戦したい人にとってはかなり敷居が高く感じられるはずです。動機として悪くはないと思いますが、良くも悪くも、先に(あるいは同時進行的に)Haskell のさわりを学んでおく必要があるでしょう。

Frege を試すには

Online REPL で実行

環境構築の手間さえ惜しむ怠惰なあなたのために、Web 上で Frege を実行できるデモサイトが用意されています。

右ペインにソースコード、左ペインが REPL で、compile ボタンを押すと REPL にモジュールがロードされた状態になります。GHCi と同じノリで使えるのでいろいろ試してみましょう。

コンパイルして実行

前提として JDK 7 もしくは JDK 8 が必要です。JDK 9 は問題が確認されている ので避けましょう。

まず Frege のリリースページ から jar ファイルで提供されているコンパイラをダウンロードします。 この記事を書いている時点での最新バージョンは 3.23.422 です。

$ wget -O fregec.jar https://github.com/Frege/frege/releases/download/3.23.288/frege3.23.422-ga05a487.jar
$ chmod +x fregec.jar

次に、Frege が生成するファイルの書き出し先ディレクトリを準備しておきます。

$ mkdir build

そしてビルドする サンプルコード をダウンロードします。

$ wget https://raw.githubusercontent.com/Frege/frege/release22/examples/SimpleIO.fr

ここまでで、ディレクトリ構造はこんな感じ。

$ tree
.
+--- SimpleIO.fr
+--- build
`--- fregec.jar

以下のコマンドでコンパイルできます。

$ java -Xss1m -jar fregec.jar -d build SimpleIO.fr
$ tree
.
+--- SimpleIO.fr
+--- build
|    `--- examples
|         +--- SimpleIO$1$1.class
|         +--- SimpleIO$1.class
|         +--- SimpleIO$1Fprompt_28850$1.class
|         +--- SimpleIO$1Fprompt_28850.class
|         +--- SimpleIO$2$1.class
|         +--- SimpleIO$2.class
|         +--- SimpleIO$IJ$$mainƒ52393afc.class
|         +--- SimpleIO$IJ$eofƒ5207be3f.class
|         +--- SimpleIO$IJ.class
|         +--- SimpleIO.class
|         `--- SimpleIO.java
`--- fregec.jar

コンパイルされた .class ファイルは以下のコマンドで実行できます。ちなみに SimpleIO の中身は、標準入力から数字を受け取って偶数か奇数かを判定するというものです。

$ java -Xss1m -cp build:fregec.jar examples.SimpleIO

もう少し知りたい人のために

現状、入手できる Frege の情報は残念ながらそれほど多くありません。とりあえず 公式 Wiki を読みましょう。またほぼ全ての関連情報は README 内のリンク集にまとまっています。

文法要素などでわからないところがあるときは、GitHub の Frege リポジトリ内を検索するとヒントが見つかるかもしれません。また、幸か不幸か Frege のコミュニティはとても小さいので、Twitter で #frege タグをつけて英語でツイートすると意外と中の人がアドバイスをくれたりします。

まとめ

今回は、HaskellJVM 言語である Frege について紹介しました。良くも悪くも Haskell に対する理解が必要ではありますが、そこさえ乗り越えてしまえばほぼ Haskell を書きながら Java エコシステムの肩に乗れるという意味でなかなか面白い言語です。

なおこの記事では触れませんでしたが、JVM 言語の例に漏れず Frege から Javaメソッドを呼び出すことが可能で、しかもその方法はかなり巧妙に設計されています。具体的には副作用を持つメソッドST モナドにマップするのですが、それはまた別の話。