型レベルFizzBuzz（及び、type familyにおけるガードの書き方）
型レベルFizzBuzzどっかで見た気がするが、今書けるかというと絶対無理
— xenophobia (@xenophobia__) 2014, 5月 2
↑みたいなこと呟いたら「そんな難しいか？」という意見が見受けられ、言われてみれば確かにそんな言うほど難しくないのでは、と思い書いてみました。最近Haskell書いていない気がするし。*1
なんですが、そもそも"型レベルFizzBuzz"って何でしょうか。初めに想像したのは
(N1, N2, ...は型レベル自然数として)
*Main> :t Proxy :: Proxy (XFizzBuzz N1)
Proxy :: Proxy (XFizzBuzz N1) :: Proxy ('Number ('S Zero))
*Main> :t Proxy :: Proxy (XFizzBuzz N3)
Proxy :: Proxy (XFizzBuzz N3) :: Proxy 'Fizz
*Main> :t Proxy :: Proxy (XFizzBuzz N5)
Proxy :: Proxy (XFizzBuzz N5) :: Proxy 'Buzz
*Main> :t Proxy :: Proxy (XFizzBuzz N15)
Proxy :: Proxy (XFizzBuzz N15) :: Proxy 'FizzBuzz
*Main> :t Proxy :: Proxy (XFizzBuzz N20)
Proxy :: Proxy (XFizzBuzz N20) :: Proxy 'Buzz
のような挙動をする何かなので、そういうものを作ってみました。
type familyで型から型への関数を書けばいいので、めっちゃ愚直にまずこんなコードを書きました。
FizzBuzzの列が基本的には15周期の列なので*2、15以上の数が来たら再帰、というコードです。いくらなんでもな気がしますが一応
*Main> main "1" "2" "Fizz" "4" "Buzz" "Fizz" "7" "8" "Fizz" "Buzz" "11" "Fizz" "13" "14" "FizzBuzz" "16" "17" "Fizz" "19" "Buzz"
という感じでちゃんと動いてくれます。もちろんREPLで次のような挙動を確認することもできます。
*Main> :t Proxy :: Proxy (XFizzBuzz N1)
Proxy :: Proxy (XFizzBuzz N1) :: Proxy FB ('Number ('S Zero))
*Main> :t Proxy :: Proxy (XFizzBuzz N3)
Proxy :: Proxy (XFizzBuzz N3) :: Proxy FB 'Fizz
*Main> :t Proxy :: Proxy (XFizzBuzz N5)
Proxy :: Proxy (XFizzBuzz N5) :: Proxy FB 'Buzz
*Main> :t Proxy :: Proxy (XFizzBuzz N15)
Proxy :: Proxy (XFizzBuzz N15) :: Proxy FB 'FizzBuzz
*Main> :t Proxy :: Proxy (XFizzBuzz N20)
Proxy :: Proxy (XFizzBuzz N20) :: Proxy FB 'Buzz
で、とりあえず一応できたんですが、やっぱり普通に3で割れたらhogehoge、5で割れたらhugahuga的なコードを書きたい欲が出てきます。
なんで最初からそうしなかったかというと、type familyの場合分けで「nを3で割った余りが0なら……」というガードを書く方法がわかりませんでした。
先駆者を調べると次のような記事がありました。
つまり
type family F x :: *
type family F x = F' x (x :>>= N0)
type family F' x (guard :: Bool) :: *
type instance F' x True = ...
type instance F' x False = ...
のように書けばガードっぽいことができるということです。
最終的に次のようなコードができました。いいんじゃないでしょうか。
githubリポジトリです。: xenophobia/TypeLevelFizzBuzz · GitHub
以下蛇足。
書いていて初めてProxyの意義を理解しました。カインドが*でない型は対応する値が存在しないので、代わりに引数にProxy (n :: Nat)型みたいな値を渡せばいける、ということなんですね。
あと、これは最初のバージョン書いていたときに気づいたんですが、DataKindsで型に昇格させた値のデータコンストラクタってシングルクォートを"付けなきゃいけなかった"記憶がある*3んですが、いつの間に不要になったんですかね？
