メリー F#%$ing クリスマス、青春謳歌、してますか?
逃げるリア充は敵です。
逃げないリア充は訓練された敵です。
今宵も全国各地で有志による正拳突きが行われていることでしょう。
ネテロ会長は正拳付きで武道への感謝を捧げましたが、私達はプログラマーなので、FizzBuzzで性なる夜のルサンチマンを発散することにしましょう。
FizzBuzz入門
よくあるFizzBuzzの例として以下のようなものがあります。
fizzbuzz n
| n `mod` 15 == 0 = "FizzBuzz"
| n `mod` 3 == 0 = "Fizz"
| n `mod` 5 == 0 = "Buzz"
| otherwise = show n
しかしたとえばこれが、FizzBuzzではなくてFizzBuzzWoofであったとしたらどうでしょうか?
以下のように多数の条件分岐をすることになってしまい、あまりよろしくありません。
fizzbuzzwoof n
| n `mod` 105 == 0 = "FizzBuzzWoof"
| n `mod` 15 == 0 = "FizzBuzz"
| n `mod` 21 == 0 = "FizzWoof"
| n `mod` 35 == 0 = "BuzzWoof"
| n `mod` 3 == 0 = "Fizz"
| n `mod` 5 == 0 = "Buzz"
| n `mod` 7 == 0 = "Woof"
| otherwise = show n
変更に対して開かれた、美しいFizzBuzzとは何でしょうか。
以下、FizzBuzzの性質に迫りつつ、その謎を紐解いていきたいと思います。
FizzBuzzとは何ぞや
そもそもFizzBuzzとは何なのでしょうか?
少し一般化してみましょう。
- ある自然数Nが与えられた時、Nを別の自然数[X1..Xi..]で順次割る
- N mod Xiの結果Siを全て結合したものが最終的な文字列RNとなる
- 文字列Siは N mod X1が0であった場合、文字列S1に、そうでない場合は空文字列S0になる
- RN == S0の場合においてのみ、RNはNの文字列表現となる
これをコードで表現すると以下のようになります。
fizzbuzz n = let res = fizz ++ buzz in
if res == "" then show n else res where
fizz = if n `mod` 3 == 0 then "Fizz" else ""
buzz = if n `mod` 5 == 0 then "Buzz" else ""
恐らくこれが、FizzBuzzWoofなども含めて一般化されたFizzBuzzの形式だと思います。
文字列とはモノイドである
ここで、上記の空文字列S0に注目してみましょう。
文字列結合の演算子を|+|とした時に、S0は以下の様な性質を持ちます。
- S0 |+| Si = Si
- Si |+| S0 = Si
これは、空文字列というのが左右の結合に対して恒等的であるということを意味します。
ここで、所謂「文字列」のように
- (a |+| b) |+| c = a |+| (b |+| c) となる二項演算 |+|
- e |+| a = a |+| e = a となる単位元 e
を持つものをモノイドといいます。
実際、文字列をモノイドとして扱うと以下のようなコードになります。
import Data.Monoid
import Data.Foldable
fizzbuzz n = let res = fizz `mappend` buzz in
if res == mempty then show n else res where
fizz = if n `mod` 3 == 0 then "Fizz" else mempty
buzz = if n `mod` 5 == 0 then "Buzz" else mempty
FizzBuzzもモノイドである
ここで、もう少し抽象度を上げて考えてみましょう。
上記のコードにおける"Fizz"や"Buzz"は文字列ですが、そうではなくて1つのデータ型であるとします。
その場合、空文字列に相当する単位元Zeroは以下のような性質を満たすものになります。
- Zero |+| Fizz = Fizz
- Fizz |+| Zero = Fizz
実際にこれをコードで表現すると以下のようになります。
import Data.Monoid
import Data.Foldable
data FizzBuzz = Fizz | Buzz | Zero | Cons FizzBuzz FizzBuzz deriving Eq
instance Monoid FizzBuzz where
mempty = Zero
mappend Zero a = a
mappend a Zero = a
mappend a b = Cons a b
instance Show FizzBuzz where
show Fizz = "Fizz"
show Buzz = "Buzz"
show (Cons a b) = (show a) ++ (show b)
fizzbuzz n = let res = fizz `mappend` buzz in
if res == mempty then show n else show res where
fizz = if n `mod` 3 == 0 then Fizz else mempty
buzz = if n `mod` 5 == 0 then Buzz else mempty
自然数Nごとにモノイド圏を生成する
しかし、上記のコードではどうしても最終的に結果が単位元かどうかを判定し、そうであった場合にはNの文字列表現を返すという処理が必要になってきます。
これは、FizzBuzzの単位元が共通のZeroという値で表現されているためです。
逆に言えば、ある自然数Nごとに違う単位元を持ったモノイド圏を生成することができれば、全てをFizzBuzz型で扱うことが可能になります。
つまり、型FizzBuzzはその基になった自然数Nを「値として持つ」ということです。
依存型で考えるモノイド
「型が値を持つ」というのはどういうことかというと、FizzBuzz(1)とFizzBuzz(2)は「違う型である」ということです。
データが値を持つのではなく、型が値を持つのです。
このような型のことを、依存型(dependent type)といいます。
Idrisによる実装
残念ながらhaskellには依存型がありませんので、ここから先はIdrisという言語を使って実装していきます。
Idrisの詳細は省きますが、シンタックス的にはhaskellとよく似た言語ですので、それほど違和感なく読めると思います。
まず、FizzBuzz型を定義します。
data FizzBuzz : (n:Nat) -> Type where
Zero : FizzBuzz n
Fizz : FizzBuzz n
Buzz : FizzBuzz n
Comb : FizzBuzz n -> FizzBuzz n -> FizzBuzz n
ここで、(n:Nat) -> Typeの部分はこのデータ型がNat(自然数)型の値nに依存していることを表しています。
次に、FizzBuzzをモノイドとして定義していきますが、Idrisにおいてモノイドは半群(Semigroup)である必要があります。
この辺の詳細は省きますが、IdrisのAlgebraなどのモジュールはこの辺のデータ型が数学上の定義に沿った形で定義されており非常に美しくできていますので、一読をおすすめします。
instance Semigroup (FizzBuzz n) where
(<+>) a Zero = a
(<+>) Zero b = b
(<+>) a b = Comb a b
instance Monoid (FizzBuzz n) where
neutral = Zero
そして、FizzBuzzの文字列表現であるShowインスタンスを実装していきます。
instance Show (FizzBuzz n) where
show Zero = show n
show Fizz = "Fizz"
show Buzz = "Buzz"
show (Comb a b) = show a ++ show b
ここで、Show Zeroがアリティ0であるにも関わらずnに依存した文字列を返しているのがポイントです。
このnは「型が持つ値」ですので、必然的に依存型でないと実装できないことになります。
ちなみにZeroが値を持てばいいじゃないかという話もありますが、それだとモノイドにならないのです。(別にモノイドじゃなくていいじゃないかと言われてしまうとまあその通りなんですが。。。)
最後にこれらを使ったfizzbuzz関数を定義して完成です。
fizzbuzz : (n:Nat) -> FizzBuzz n
fizzbuzz n = fizz <+> buzz <+> woof where
fizz = if mod n 3 == 0 then Fizz else neutral
buzz = if mod n 5 == 0 then Buzz else neutral
自然数nごとにFizzBuzz型が定義されるので、FizzBuzz(2)型のZeroをshowするとちゃんと"2"になります。
FizzBuzzとは心の所作
いかがでしたでしょうか。
普段何気なく接しているはずのFizzBuzzですが、そこに感謝の意を込めれば、様々なものが見えてきます。
心が正しく形を成せば 想いとなり 想いこそが 実を結びます。
FizzBuzzとはすなわち心の所作なのです。
ちなみにネテロ会長にあやかって手元のマシンで感謝のFizzBuzzを100万まで回したら1時間を切るどころか全然返ってこなくなってむしろコンソールが私を置き去りにしましたかなしい。
PS
明日25日目に最後を飾るのは先日結婚したばかりの@y-kenさんです(ｸｿが)。
そしてこの記事はあえて21:00過ぎに公開しています。
