Go to Qiita Advent Calendar 2024 Top
LoginSignup
24
19

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 5 years have passed since last update.

@myuon_myon(高階 射)

GHC.TypeLitsと型レベルFizzBuzz

Last updated at Posted at 2014-08-10

base-4.7からGHC.TypeLitsモジュールが強化され、型レベル自然数はより扱いやすくなった。
これを使って型レベルFizzBuzzを実装しようという話。

実行例

以下のような挙動を示す函数fizzbuzz(おまけでfizzbuzzListも)を作る。

main = do
  putStrLn $ fizzbuzz (Proxy :: Proxy 15)
  print $ fizzbuzzList (Proxy :: Proxy 16)

{-
> runhaskell TypedFizzBuzz.hs 
FizzBuzz
["1","2","Fizz","4","Buzz","Fizz","7","8","Fizz","Buzz","11","Fizz","13","14","FizzBuzz","16"]
-}

Proxy :: Proxy nのようにして自然数を与えるとその数をfizzbuzzした文字列を返してくれる。__値(数値)には一切触れずにこれをやっている__というのが大切。
ちなみに型レベルで実装しているので負の数を与えるとコンパイルエラーになる。

実装

実装例

はじめに実装を示す。
ghc-7.8とbase-4.7以降でないと動きません。

{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies #-}
{-# LANGUAGE UndecidableInstances, FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables, GADTs, MultiParamTypeClasses, FunctionalDependencies #-}

import GHC.TypeLits
import Data.Type.Equality
import Data.Proxy

type family (a :: Nat) % (b :: Nat) :: Nat where
  a % b = Mod a b (CmpNat a b)
type family Mod (a :: Nat) (b :: Nat) (k :: Ordering) :: Nat where
  Mod a b EQ = 0
  Mod a b LT = a
  Mod a b GT = Mod (a-b) b (CmpNat (a-b) b)

data FizzBuzzFlag = FizzBuzz | Fizz | Buzz | Natural Nat

class ShowFB (f :: FizzBuzzFlag) where
  showFB :: Proxy f -> String

instance ShowFB FizzBuzz where showFB _ = "FizzBuzz"
instance ShowFB Fizz where showFB _ = "Fizz"
instance ShowFB Buzz where showFB _ = "Buzz"
instance (KnownNat n) => ShowFB (Natural n) where showFB _ = show $ natVal $ (Proxy :: Proxy n)

type family ToFizzBuzz (a :: Nat) :: FizzBuzzFlag where
  ToFizzBuzz a = ToFizzBuzz' a (a % 3) (a % 5)
type family ToFizzBuzz' (a :: Nat) (b3 :: Nat) (b5 :: Nat) :: FizzBuzzFlag where
  ToFizzBuzz' a 0 0 = FizzBuzz
  ToFizzBuzz' a 0 b5 = Fizz
  ToFizzBuzz' a b3 0 = Buzz
  ToFizzBuzz' a b3 b5 = Natural a

fizzbuzz :: (ShowFB (ToFizzBuzz n)) => Proxy (n :: Nat) -> String
fizzbuzz (Proxy :: Proxy m) = showFB $ (Proxy :: Proxy (ToFizzBuzz m))

class FizzBuzzList' (b :: Bool) (n :: Nat) where
  fizzbuzzList' :: Proxy b -> Proxy n -> [String] -> [String]

instance FizzBuzzList' True 0 where
  fizzbuzzList' _ _ acc = acc
instance (ShowFB (ToFizzBuzz n), FizzBuzzList' (n == 1) (n-1)) => FizzBuzzList' False n where
  fizzbuzzList' _ k@(Proxy :: Proxy n) acc = fizzbuzzList' (Proxy :: Proxy (n == 1)) (Proxy :: Proxy (n-1)) ((fizzbuzz k) : acc)

fizzbuzzList :: (FizzBuzzList' (n==0) n) => Proxy (n :: Nat) -> [String]
fizzbuzzList x@(Proxy :: Proxy n) = fizzbuzzList' (Proxy :: Proxy (n==0)) x []

main = do
  mapM_ putStrLn $ fizzbuzzList (Proxy :: Proxy 16)

GHC.TypeLits

GHC.TypeLitsには以下のようなものが実装されている。

  • Nat: Natカインドをもつ型レベル自然数。DataKinds拡張が必要。これを使うと型レベル自然数はProxy :: Proxy 10などと書くことができてめっちゃ便利
  • +,-,*,^ :: Nat -> Nat -> Nat: 和・差・積・冪の型レベル演算
  • CmpNat :: Nat -> Nat -> Ordering: 大きさの比較
  • natVal :: forall n proxy. KnownNat n => proxy n -> Integer: 型レベル自然数をIntegerという値に落とす函数

Data.Proxyは型情報のみを持つデータ proxy を提供するモジュール。Natカインドはこれを介して操作するので、natValの引数はproxy nという形になっている。(natVal (Proxy :: Proxy 10)みたいにして使う。)

DataKinds

DataKinds拡張は自作の型をカインドに、データコンストラクタを型に昇格できるという拡張。
以下のようにFizzBuzzFlagを定義すると、FizzBuzzFlagというカインドとそれに属する4つの型FizzBuzz, Fizz, Buzz, Natural (n :: Nat)が生成される。
showFBはFizzBuzzFlagカインドを持つ型を持つ値を実際の文字列に変換する。ShotFBの定義がShowFB (f :: FizzBuzzFlag)になっていることに注意。instance showFB (Natural n)のところで型レベル自然数NatをIntegerという値に変換している。

data FizzBuzzFlag = FizzBuzz | Fizz | Buzz | Natural Nat

class ShowFB (f :: FizzBuzzFlag) where
  showFB :: Proxy f -> String

instance ShowFB FizzBuzz where showFB _ = "FizzBuzz"
instance ShowFB Fizz where showFB _ = "Fizz"
instance ShowFB Buzz where showFB _ = "Buzz"
instance (KnownNat n) => ShowFB (Natural n) where showFB _ = show $ natVal $ (Proxy :: Proxy n)

TypeFamilies

TypeFamiliesとは、簡単に言うと型や値を受け取って型を返すような函数を作るためのGHC拡張。
今回はGHC.TypeLitsにない型レベル剰余と、型レベル自然数をFizzBuzzを表す型へ変換するところで使っている。

type family ... where ...と書くのはClosed family simplicationと言って、ghc-7.8で導入された書き方。これを使うと普通の函数と同様、全てのパターンマッチに失敗したらなんらかの処理をするという書き方ができる。

以下は型レベルの剰余。引けるだけ引くというのをやるだけ。
条件分岐の代わりにパターンマッチを行うのでModという函数を挟んで処理している。

type family (a :: Nat) % (b :: Nat) :: Nat where
  a % b = Mod a b (CmpNat a b)
type family Mod (a :: Nat) (b :: Nat) (k :: Ordering) :: Nat where
  Mod a b EQ = 0
  Mod a b LT = a
  Mod a b GT = Mod (a-b) b (CmpNat (a-b) b)

型レベル自然数をFizzBuzzFlagカインドをもつ型に変換する部分。
剰余のときと同じように、3や5で割った余りで場合分けが発生するのでそこをToFizzBuzz'という新たなtype familyを作っている。

type family ToFizzBuzz (a :: Nat) :: FizzBuzzFlag where
  ToFizzBuzz a = ToFizzBuzz' a (a % 3) (a % 5)
type family ToFizzBuzz' (a :: Nat) (b3 :: Nat) (b5 :: Nat) :: FizzBuzzFlag where
  ToFizzBuzz' a 0 0 = FizzBuzz
  ToFizzBuzz' a 0 b5 = Fizz
  ToFizzBuzz' a b3 0 = Buzz
  ToFizzBuzz' a b3 b5 = Natural a

fizzbuzz

これで必要なものは揃ったので、あとは型レベル自然数をToFizzBuzzしてshowFBすればOK。

fizzbuzz :: (ShowFB (ToFizzBuzz n)) => Proxy (n :: Nat) -> String
fizzbuzz (Proxy :: Proxy m) = showFB $ (Proxy :: Proxy (ToFizzBuzz m))

-- fizzbuzz (Proxy :: Proxy 15) == "FizzBuzz"

fizzbuzzList

ついでに型レベルFizzBuzzの結果をリストにして返すfizzbuzzListも作ってみる。
Overlapping instances errorを回避するためにFizzBuzzList' (b::Bool) (n::Nat)のところで「nが0であるかを判定する」フラグ用のBoolカインドの型を受け取っているのがミソ。
詳しくはAdvancedOverlapの手法を参照。

これによって、上で作ったfizzbuzzの結果をリストにして返すfizzbuzzListが動くようになる。

class FizzBuzzList' (b :: Bool) (n :: Nat) where
  fizzbuzzList' :: Proxy b -> Proxy n -> [String] -> [String]

instance FizzBuzzList' True 0 where
  fizzbuzzList' _ _ acc = acc
instance (ShowFB (ToFizzBuzz n), FizzBuzzList' (n == 1) (n-1)) => FizzBuzzList' False n where
  fizzbuzzList' _ k@(Proxy :: Proxy n) acc = fizzbuzzList' (Proxy :: Proxy (n == 1)) (Proxy :: Proxy (n-1)) ((fizzbuzz k) : acc)

fizzbuzzList :: (FizzBuzzList' (n==0) n) => Proxy (n :: Nat) -> [String]
fizzbuzzList x@(Proxy :: Proxy n) = fizzbuzzList' (Proxy :: Proxy (n==0)) x []

コンパイル！

実際に型レベルの処理はコンパイル時に計算されることを確認しよう。

> ghc -O2 -ddump-simpl TypedFizzBuzz.hs

とするとGHCが出力するコア言語を見ることができる。下の方に

-- 型は省略、読みやすいように適当に改変してあります

Main.main20 = __integer 1
Main.main19 = (main20の値を出力)
Main.main18 = __integer 2
Main.main17 = (main18の値を出力)
Main.main16 = __integer 4
Main.main15 = (main16の値を出力)

(中略)

Main.main6 =
  GHC.Types.: @ GHC.Base.String Main.$fShowFBFizz1 Main.main7 -- "Fizz" : main7
Main.main5 =
  GHC.Types.: @ GHC.Base.String Main.$fShowFBBuzz1 Main.main6 -- "Buzz" : main6
Main.main4 = GHC.Types.: @ GHC.Base.String Main.main15 Main.main5 -- main15 : main5
Main.main3 =
  GHC.Types.: @ GHC.Base.String Main.$fShowFBFizz1 Main.main4 -- "Fizz" : main4
Main.main2 = GHC.Types.: @ GHC.Base.String Main.main17 Main.main3 -- main17 : main3

となっていることから、コンパイル時にFizzBuzzの計算が行われていることが分かる。

問題点とまとめ

  • コンパイル時のスタック制限があるので少し入力が大きくなるとすぐコンパイルエラーになる。(-ftype-function-depth=Nとしてスタックを増やすことはできる。)
  • ghc-7.8とbase-4.7で型レベルプログラミングの機能はかなり強化された
  • GHCかわいい
  • GHCかわいい！

以上。

24
19
1

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
Sign upLogin
24
19

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?