Go to Qiita Advent Calendar 2024 Top
LoginSignup
12
8

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 1 year has passed since last update.

@matoruru

PureScriptで型レベルFizzBuzz(Type-level FizzBuzz)

Last updated at Posted at 2019-08-12

はじめに

型レベルでFizzBuzzを書きました。言語はPureScriptです。

もちろん普通に(値レベル?で)書くこともできます。

型レベル自然数を用意する

foreign import kind Nat

foreign import data Zero :: Nat
foreign import data Succ :: Nat -> Nat

data NProxy (n :: Nat) = NProxy

class Nat (n :: Nat) where
  toInt :: NProxy n -> Int

instance natZero ::          Nat Zero     where
  toInt _ = 0

instance natSucc :: Nat n => Nat (Succ n) where
  toInt _ = 1 + toInt (NProxy :: NProxy n)

大きな数を少ないタイプ数で利用できるように、以下のようなクラスも定義しておきます。

class Succ10  (n :: Nat) (n' :: Nat) | n -> n'
instance succ10  :: Succ10 n (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ n))))))))))

class Succ50  (n :: Nat) (n' :: Nat) | n -> n'
instance succ50  :: (Succ10 n n1, Succ10 n1 n2, Succ10 n2 n3, Succ10 n3 n4, Succ10 n4 n5) => Succ50 n n5

class Succ100 (n :: Nat) (n' :: Nat) | n -> n'
instance succ100 :: (Succ50  n n', Succ50  n' n'') => Succ100 n n''

class Succ200 (n :: Nat) (n' :: Nat) | n -> n'
instance succ200 :: (Succ100 n n', Succ100 n' n'') => Succ200 n n''

class Succ300 (n :: Nat) (n' :: Nat) | n -> n'
instance succ300 :: (Succ200 n n', Succ100 n' n'') => Succ300 n n''

class Succ400 (n :: Nat) (n' :: Nat) | n -> n'
instance succ400 :: (Succ300 n n', Succ100 n' n'') => Succ400 n n''

class Succ500 (n :: Nat) (n' :: Nat) | n -> n'
instance succ500 :: (Succ400 n n', Succ100 n' n'') => Succ500 n n''

これで、型レベルの数を表したいときには以下のように書くことができます。

10の場合
NProxy :: forall n. Succ10 Zero n => NProxy n
50の場合
NProxy :: forall n. Succ50 Zero n => NProxy n
100の場合
NProxy :: forall n. Succ100 Zero n => NProxy n

...

500の場合
NProxy :: forall n. Succ500 Zero n => NProxy n

REPLで試してみます。

> toInt (NProxy :: forall n. Succ10 Zero n => NProxy n)
10

> toInt (NProxy :: forall n. Succ50 Zero n => NProxy n)
50

> toInt (NProxy :: forall n. Succ100 Zero n => NProxy n)
100

...

> toInt (NProxy :: forall n. Succ500 Zero n => NProxy n)
500

型レベルBooleanを用意する

foreign import kind Boolean

foreign import data True  :: Boolean
foreign import data False :: Boolean

data BProxy (b :: Boolean) = BProxy

3か5(もしくはその両方)で割り切れるかどうかを調べる

上で用意したBooleanを使います。割り切れたらTrue、割り切れなければFalseを返します。

class IsMod3 (n :: Nat) (b :: Boolean) | n -> b
instance      isMod3    :: IsMod3 n b => IsMod3 (Succ (Succ (Succ n))) b
else instance isMod3'   ::               IsMod3 Zero                   True
else instance isnotMod3 ::               IsMod3 n                      False

class IsMod5 (n :: Nat) (b :: Boolean) | n -> b
instance      isMod5    :: IsMod5 n b => IsMod5 (Succ (Succ (Succ (Succ (Succ n))))) b
else instance isMod5'   ::               IsMod5 Zero                                 True
else instance isnotMod5 ::               IsMod5 n                                    False

5（または3）を減算しながら再帰し、Zeroになったら余りがなかったのでTrueを返します。5（または3）の減算ができずZeroにもならなかった場合、余りが出ているのでFalseを返します。

FizzかBuzzかFizzBuzzか数字かを判定する

上で定義したIsMod3とIsMod5を使います。

foreign import kind Result

foreign import data Fizz     :: Result
foreign import data Buzz     :: Result
foreign import data FizzBuzz :: Result
foreign import data Number   :: Result

data RProxy (r :: Result) = RProxy

class Judge (n :: Nat) (r :: Result) | n -> r
instance judgeByPattern  :: (IsMod3 n b3, IsMod5 n b5, JudgeByPattern b3 b5 r) => Judge n r

judge :: forall n r. Nat n => Judge n r => NProxy n -> RProxy r
judge _ = RProxy

class JudgeByPattern (fb :: Boolean) (bb :: Boolean) (r :: Result) | fb bb -> r
instance judgeFizz     :: JudgeByPattern True  False Fizz
instance judgeBuzz     :: JudgeByPattern False True  Buzz
instance judgeFizzBuzz :: JudgeByPattern True  True  FizzBuzz
instance judgeNumber   :: JudgeByPattern False False Number

入力された自然数を基に、IsMod3とIsMod5のそれぞれから返ってきた値を使ってパターンマッチします。

  • IsMod3のみTrueの場合→Fizz
  • IsMod5のみTrueの場合→Buzz
  • 両方Trueの場合→FizzBuzz
  • 両方Falseの場合→Number

FizzやBuzzを表示できるようにする

型から文字列への変換です。

class ShowFizzBuzz (r :: Result) where
  show :: RProxy r -> Int -> String

instance showFizz     :: ShowFizzBuzz Fizz     where
  show _ _ = "Fizz"

instance showBuzz     :: ShowFizzBuzz Buzz     where
  show _ _ = "Buzz"

instance showFizzBuzz :: ShowFizzBuzz FizzBuzz where
  show _ _ = "Fizz-Buzz"

instance showNumber   :: ShowFizzBuzz Number   where
  show _   = S.show

REPLで試してみます。

> show (RProxy :: (forall r. Judge (Succ Zero) r => RProxy r)) (toInt (NProxy :: NProxy (Succ Zero)))
"1"

> show (RProxy :: (forall r. Judge (Succ (Succ Zero)) r => RProxy r)) (toInt (NProxy :: NProxy (Succ (Succ Zero))))
"2"

> show (RProxy :: (forall r. Judge (Succ (Succ (Succ Zero))) r => RProxy r)) (toInt (NProxy :: NProxy (Succ (Succ (Succ Zero)))))
"Fizz"

> show (RProxy :: (forall n r. Succ10 Zero n => Judge n r => RProxy r)) (toInt (NProxy :: forall n. Succ10 Zero n => NProxy n))
"Buzz"

> show (RProxy :: (forall n r. Succ100 Zero n => Judge n r => RProxy r)) (toInt (NProxy :: forall n. Succ100 Zero n => NProxy n))
"Buzz"

上で定義したSucc100などのクラスのおかげで、大きな数を簡単に書けていることもわかります。

FizzBuzzの配列を得る

これまで定義してきた型やクラス、関数を組み合わせ、再帰でArray Stringを作ります。インスタンスresultByNのパターンマッチ部分の影響で、このFizzBuzzはN-1からスタートすることになるため、Nから1までのFizzBuzzをしたい場合は、(Succ N)を渡す必要があります。

runFizzBuzz :: forall n r. Nat n => Result n r => NProxy n -> Array String
runFizzBuzz n = toResult n RProxy

class Result (n :: Nat) (r :: Result) | n -> r where
  toResult :: NProxy n -> RProxy r -> Array String

instance      resultByZero ::                                                   Result (Succ Zero) r' where
  toResult _ _ = []

else instance resultByN    :: (Nat n, ShowFizzBuzz r, Result n r, Judge n r) => Result (Succ n)    r' where
  toResult _ _ = show (RProxy :: RProxy r) (toInt (NProxy :: NProxy n)) : toResult (NProxy :: NProxy n) (judge (NProxy :: NProxy n))

REPLで試してみます。

> runFizzBuzz (NProxy :: NProxy (Succ (Succ (Succ (Succ Zero)))))
["Fizz","2","1"]

> runFizzBuzz (NProxy :: forall n. Succ10 (Succ Zero) n => NProxy n)
["Buzz","Fizz","8","7","Fizz","Buzz","4","Fizz","2","1"]

> runFizzBuzz (NProxy :: forall n. Succ100 (Succ Zero) n => NProxy n)
["Buzz","Fizz","98","97","Fizz","Buzz","94","Fizz","92","91","Fizz-Buzz","89","88","Fizz","86","Buzz","Fizz","83","82","Fizz","Buzz","79","Fizz","77","76","Fizz-Buzz","74","73","Fizz","71","Buzz","Fizz","68","67","Fizz","Buzz","64","Fizz","62","61","Fizz-Buzz","59","58","Fizz","56","Buzz","Fizz","53","52","Fizz","Buzz","49","Fizz","47","46","Fizz-Buzz","44","43","Fizz","41","Buzz","Fizz","38","37","Fizz","Buzz","34","Fizz","32","31","Fizz-Buzz","29","28","Fizz","26","Buzz","Fizz","23","22","Fizz","Buzz","19","Fizz","17","16","Fizz-Buzz","14","13","Fizz","11","Buzz","Fizz","8","7","Fizz","Buzz","4","Fizz","2","1"]

> runFizzBuzz (NProxy :: forall n. Succ200 (Succ Zero) n => NProxy n)
["Buzz","199","Fizz","197","196","Fizz-Buzz","194","193","Fizz","191","Buzz","Fizz","188","187","Fizz","Buzz","184","Fizz","182","181","Fizz-Buzz","179","178","Fizz","176","Buzz","Fizz","173","172","Fizz","Buzz","169","Fizz","167","166","Fizz-Buzz","164","163","Fizz","161","Buzz","Fizz","158","157","Fizz","Buzz","154","Fizz","152","151","Fizz-Buzz","149","148","Fizz","146","Buzz","Fizz","143","142","Fizz","Buzz","139","Fizz","137","136","Fizz-Buzz","134","133","Fizz","131","Buzz","Fizz","128","127","Fizz","Buzz","124","Fizz","122","121","Fizz-Buzz","119","118","Fizz","116","Buzz","Fizz","113","112","Fizz","Buzz","109","Fizz","107","106","Fizz-Buzz","104","103","Fizz","101","Buzz","Fizz","98","97","Fizz","Buzz","94","Fizz","92","91","Fizz-Buzz","89","88","Fizz","86","Buzz","Fizz","83","82","Fizz","Buzz","79","Fizz","77","76","Fizz-Buzz","74","73","Fizz","71","Buzz","Fizz","68","67","Fizz","Buzz","64","Fizz","62","61","Fizz-Buzz","59","58","Fizz","56","Buzz","Fizz","53","52","Fizz","Buzz","49","Fizz","47","46","Fizz-Buzz","44","43","Fizz","41","Buzz","Fizz","38","37","Fizz","Buzz","34","Fizz","32","31","Fizz-Buzz","29","28","Fizz","26","Buzz","Fizz","23","22","Fizz","Buzz","19","Fizz","17","16","Fizz-Buzz","14","13","Fizz","11","Buzz","Fizz","8","7","Fizz","Buzz","4","Fizz","2","1"]

成功です！

ソースコード全文

FizzBuzz.purs
module FizzBuzz where

import Prelude ((+))

import Prim hiding (Number)

import Data.Array ((:))
import Data.Show (show) as S

runFizzBuzz :: forall n r. Nat n => Result n r => NProxy n -> Array String
runFizzBuzz n = toResult n RProxy

foreign import kind Boolean

foreign import data True  :: Boolean
foreign import data False :: Boolean

data BProxy (b :: Boolean) = BProxy

foreign import kind Result

foreign import data Fizz     :: Result
foreign import data Buzz     :: Result
foreign import data FizzBuzz :: Result
foreign import data Number   :: Result

data RProxy (r :: Result) = RProxy

foreign import kind Nat

foreign import data Zero :: Nat
foreign import data Succ :: Nat -> Nat

data NProxy (n :: Nat) = NProxy

class Nat (n :: Nat) where
  toInt :: NProxy n -> Int

instance natZero ::          Nat Zero     where
  toInt _ = 0

instance natSucc :: Nat n => Nat (Succ n) where
  toInt _ = 1 + toInt (NProxy :: NProxy n)

class Succ10  (n :: Nat) (n' :: Nat) | n -> n'
instance succ10  :: Succ10 n (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ n))))))))))

class Succ50  (n :: Nat) (n' :: Nat) | n -> n'
instance succ50  :: (Succ10 n n1, Succ10 n1 n2, Succ10 n2 n3, Succ10 n3 n4, Succ10 n4 n5) => Succ50 n n5

class Succ100 (n :: Nat) (n' :: Nat) | n -> n'
instance succ100 :: (Succ50  n n', Succ50  n' n'') => Succ100 n n''

class Succ200 (n :: Nat) (n' :: Nat) | n -> n'
instance succ200 :: (Succ100 n n', Succ100 n' n'') => Succ200 n n''

class Succ300 (n :: Nat) (n' :: Nat) | n -> n'
instance succ300 :: (Succ200 n n', Succ100 n' n'') => Succ300 n n''

class Succ400 (n :: Nat) (n' :: Nat) | n -> n'
instance succ400 :: (Succ300 n n', Succ100 n' n'') => Succ400 n n''

class Succ500 (n :: Nat) (n' :: Nat) | n -> n'
instance succ500 :: (Succ400 n n', Succ100 n' n'') => Succ500 n n''

class Result (n :: Nat) (r :: Result) | n -> r where
  toResult :: NProxy n -> RProxy r -> Array String

instance      resultByZero ::                                                   Result (Succ Zero) r' where
  toResult _ _ = []

else instance resultByN    :: (Nat n, ShowFizzBuzz r, Result n r, Judge n r) => Result (Succ n)    r' where
  toResult _ _ = show (RProxy :: RProxy r) (toInt (NProxy :: NProxy n)) : toResult (NProxy :: NProxy n) (judge (NProxy :: NProxy n))

class ShowFizzBuzz (r :: Result) where
  show :: RProxy r -> Int -> String

instance showFizz     :: ShowFizzBuzz Fizz     where
  show _ _ = "Fizz"

instance showBuzz     :: ShowFizzBuzz Buzz     where
  show _ _ = "Buzz"

instance showFizzBuzz :: ShowFizzBuzz FizzBuzz where
  show _ _ = "Fizz-Buzz"

instance showNumber   :: ShowFizzBuzz Number   where
  show _   = S.show

class Judge (n :: Nat) (r :: Result) | n -> r
instance judgeByPattern  :: (IsMod3 n b3, IsMod5 n b5, JudgeByPattern b3 b5 r) => Judge n r

judge :: forall n r. Nat n => Judge n r => NProxy n -> RProxy r
judge _ = RProxy

class JudgeByPattern (fb :: Boolean) (bb :: Boolean) (r :: Result) | fb bb -> r
instance judgeFizz     :: JudgeByPattern True  False Fizz
instance judgeBuzz     :: JudgeByPattern False True  Buzz
instance judgeFizzBuzz :: JudgeByPattern True  True  FizzBuzz
instance judgeNumber   :: JudgeByPattern False False Number

class IsMod3 (n :: Nat) (b :: Boolean) | n -> b
instance      isMod3    :: IsMod3 n b => IsMod3 (Succ (Succ (Succ n))) b
else instance isMod3'   ::               IsMod3 Zero                   True
else instance isnotMod3 ::               IsMod3 n                      False

class IsMod5 (n :: Nat) (b :: Boolean) | n -> b
instance      isMod5    :: IsMod5 n b => IsMod5 (Succ (Succ (Succ (Succ (Succ n))))) b
else instance isMod5'   ::               IsMod5 Zero                                 True
else instance isnotMod5 ::               IsMod5 n                                    False

まとめ

ここまで読んでくださってありがとうございます！

Twitterフォローしていただけると嬉しいです！
https://twitter.com/_matoruru

12
8
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
Sign upLogin
12
8

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?