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

claustrophobia

一般λがなんか書くとか

型レベルFizzBuzz(及び、type familyにおけるガードの書き方)

↑みたいなこと呟いたら「そんな難しいか?」という意見が見受けられ、言われてみれば確かにそんな言うほど難しくないのでは、と思い書いてみました。最近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なら……」というガードを書く方法がわかりませんでした。

先駆者を調べると次のような記事がありました。

型レベルで FizzBuzz - hyoneの日記

つまり

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んですが、いつの間に不要になったんですかね?

*1:実は今までこのブログにHaskell記事一切ない

*2:FizzでもBuzzでもなくそのまま数が入る項はもちろんどんどん大きくなるわけですが。

*3:GHCiの表示見る限り内部的に自動で付されるっぽい