15
9

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 3 years have passed since last update.

HaskellAdvent Calendar 2019

Day 16

Haskell の 3 つのバナナ

Last updated at Posted at 2019-12-15

この記事は Haskell Advent Calendar 2019 の 16 日目の記事です.

Haskell プログラマとして知っておくべき 3 つのバナナを紹介します.

  • その 1: Arrow のバナナ
  • その 2: FRP のバナナ
  • その 3: F-代数のバナナ

:banana: その 1: Arrow のバナナ

1 つめのバナナは,型クラス Arrow のためのバナナです.

Arrow は,モナドの一般化として Hughes [1] により定義された概念です.
Haskell では型クラス Arrow として定式化されており,GHC では Arrow のための記法を Arrows 言語拡張により利用できます.
この言語拡張で利用できる記法のひとつにバナナ括弧 (| ⋅ |) があります.

ASCII 表現だと (| ⋅ |) はあまりバナナに見えませんが,TeX でそれっぽくレンダリングしてあげると,バナナに見えるようになります.

(\!|\ \cdot\ |\!)

Haskell における Arrow の定式化は,おおよそ Paterson による定式化 [2] がベースとなっています.
Arrows 言語拡張で利用できるバナナ括弧は,[2] における form キーワードに相当する記法です.
つまり,バナナ括弧は以下のように定義されているとみなすことができます.

(\!| e\ c_1 \dots c_n |\!) = {\rm\bf form}\ e\ c_1\ \dots\ c_n

実際にバナナ括弧を使ったプログラムを見てみましょう.
Control.Arrow モジュールに定義されている関数 (&&&) をラッピングしただけの簡単な関数 fanout を,バナナ括弧を使って定義してみます.

{-# LANGUAGE Arrows #-}

import Control.Arrow

fanout :: Arrow a => a b c -> a b c' -> a b (c, c')
fanout f g = proc x -> (| (&&&) (f -< x) (g -< x) |)

実行例は以下の通りです.

% ghci -XArrows
GHCi, version 8.4.4: http://www.haskell.org/ghc/  :? for help
Prelude> :l sample.hs
[1 of 1] Compiling Main             ( sample.hs, interpreted )
Ok, one module loaded.
*Main> fanout length sum [1, 2, 3]
(3,6)

:banana: その 2: FRP のバナナ

2 つめのバナナは,関数型リアクティブプログラミング (FRP) のライブラリである reactive-banana です.

Reactive-banana は Yampa などと同じく FRP 向けのライブラリであり,Apfelmus によって開発されています.wxHaskell との連携による GUI アプリケーションの開発にも対応しています.

なんでバナナなのかな? と思っていろいろ調べてみましたが,名前の由来は見つかりませんでした.特に深い意味はないような気がします.

モジュール Reactive.Banana.Combinators にデータ型 EventBehavior が定義されており,これがこのライブラリの核となっています.

type Event a = [(Time, a)]
type Behavior a = Time -> a

Reactive-banana の開発リポジトリにはサンプルが用意されており,FRP で組んだプログラムの挙動を簡単に確かめることができます.
こちらは,スロットマシンのサンプルを動作させてみたときの様子です.

% git clone https://github.com/HeinrichApfelmus/reactive-banana.git
% cd reactive-banana/reactive-banana/doc/examples
% runghc SlotMachine.hs
-----------------------------
- THE REACTIVE SLOT MACHINE -
------ WIN A BANANA ---------

Commands are:
   coin    - insert a coin
   play    - play one game
   quit    - quit the program

> coin
Credits: 1
> play
Credits: 5
You rolled  322
Wow, a double!
> quit
%

:banana: その 3: F-代数のバナナ

3 つめのバナナは,$F$-代数の圏に関する文脈で登場するバナナです.

$F$-代数とは,自己関手 $F$ によって定義される代数 $(A,\ f : F(A) \to A)$ のことです.
文献によっては関手に違う文字を使うこともあるので,$F$-代数という名前ではなかったりしますね (例えば,Awodey 本 [3] では $P$-代数).

$F$-始代数から $F$-代数 $(A, \varphi)$ への準同型は catamorphism と呼ばれ,しばしばバナナ括弧を使って次のように書かれます.

(\!| \varphi |\!)

このバナナ括弧は,Meijer ら [4] によって導入された記法に由来しています.
Meijer らは,ほかにもレンズ,封筒,有刺鉄線といった名前の括弧も定義しています (面白いので論文をぜひ読んでみてください).
バナナ括弧の使い方は文献によってまちまちですが,ここでは Haskell Wiki にある定式化を採用することにします.

$F$-代数や catamorphism は圏論の言葉で説明されることが多いですが,Haskell にも密接に関係しています.
catamorphism は,Haskell ではfoldr に代表されるようないわゆる畳込み演算を表します.
また,リストや自然数などの代数的データ型を扱ういくつかの関数は,catamorphism を使って表現することができます.

リストの例から見てみましょう.$A$ 型のリストの始代数は以下のように表せます.

(\mathsf{List}(A),\ [\mathsf{nil}, \mathsf{cons}] : 1 + A \times \mathsf{List}(A) \to \mathsf{List}(A))

このとき,リストを扱う関数 map は,catamorphism によって以下のように表現できます.

\mathsf{map}(f) = (\!| [ \mathsf{nil},\ \lambda{}xa.\mathsf{cons} (f(x), a) ] |\!)

次に,自然数 (ここではペアノ数) の例も見てみましょう.自然数の始台数は以下のように表せます.

(\mathsf{Nat},\ [\mathsf{0}, \mathsf{succ}] : 1 + \mathsf{Nat} \to \mathsf{Nat})

このとき,自然数を扱う関数 add は,catamorphism によって以下のように表現できます.

\mathsf{add}(n) = (\!| [ n, \mathsf{succ} ] |\!)

他にも,ブーリアンや木構造などさまざまなデータ型について,catamorphism を得ることができます.

:banana: まとめ

この記事では,Haskell と関わりの深い 3 つのバナナを訪ねてみました.

  • その 1: Arrow のバナナ
  • その 2: FRP のバナナ
  • その 3: F-代数のバナナ

他にも,Haskell の入門書の例題など,至るところでバナナは登場します (例えば,"Learn You a Haskell for Gread Good!" の 12 章 にもバナナを見つけることができます).
もし見かけたら,今日会ったバナナのことも思い出してあげてください.

そして,バナナで Haskell に興味をもったそこのあなたへ.
Haskell を始めるなら,私が昔書いたチュートリアル ウォークスルー Haskell もぜひ読んでみてください (バナナは出てきません).

参考文献

  • [1] John Hughes. Generalising Monads to Arrows. In Science of Computer Programming (37), pp. 67-111, 2000.
  • [2] R. Paterson. A New Notation for Arrows. In Proc. ICFP 2001, pp. 229-240, 2001.
  • [3] S. Awodey. Category Theory (2nd ed.). Oxford University Press, 2010.
  • [4] E. Meijer, M. Fokkinga, and R. Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In Proc. FPCA 1991, pp. 124-144, 1991.
15
9
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
15
9

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?