Skip to content

Instantly share code, notes, and snippets.

@david-christiansen
Last active August 29, 2015 14:04
Show Gist options
  • Save david-christiansen/b0035b232febab542cd2 to your computer and use it in GitHub Desktop.
Save david-christiansen/b0035b232febab542cd2 to your computer and use it in GitHub Desktop.
Dependently typed FizzBuzz, about 5 years late to the party
module FizzBuzz
-- Dependently-typed FizzBuzz, about 5 years late to the party.
-- A specification of the problem. Each constructor tells the conditions
-- under which it can be applied, and the "auto" keyword means that proof
-- search will be used in the context where they are applied to fill them
-- out. For instance, applying `N` to some Nat fails unless there's a proof in
-- scope that the argument meets the criteria.
data FB : Nat -> Type where
N : (n : Nat) -> {auto not3 : Not (n `mod` 3 = 0)} -> {auto not5 : Not (n `mod` 5 = 0)} -> FB n
Fizz : (n : Nat) -> {auto div3 : n `mod` 3 = 0} -> {auto not5 : Not (n `mod` 5 = 0)} -> FB n
Buzz : (n : Nat) -> {auto not3 : Not (n `mod` 3 = 0)} -> {auto div5 : n `mod` 5 = 0} -> FB n
FizzBuzz : (n : Nat) -> {auto div3 : n `mod` 3 = 0} -> {auto div5 : n `mod` 5 = 0} -> FB n
-- A function to calculate what to output for a given number. decEq leaves
-- proofs in scope (the arguments to `Yes` and `No`) that will be found by
-- proof search when applying the constructors.
fb : (n : Nat) -> FB n
fb n with (decEq (n `mod` 3) 0)
fb n | (Yes prf) with (decEq (n `mod` 5) 0)
fb n | (Yes prf) | (Yes x) = FizzBuzz n
fb n | (Yes prf) | (No contra) = Fizz n
fb n | (No contra) with (decEq (n `mod` 5) 0)
fb n | (No contra) | (Yes prf) = Buzz n
fb n | (No contra) | (No f) = N n
-- An infinite stream of the natural numbers, starting at 0 and going up. Z is
-- 0, S is one plus its argument. `iterate` starts a stream with its second
-- argument, then generates each new element by applying its first argument to
-- the previous element.
nats : Stream Nat
nats = iterate S Z
--- A stream of pairs of Nats and their corresponding output. Use `tail`
--- because the problem says to start at 1.
fizzBuzz : Stream (n : Nat ** FB n)
fizzBuzz = map (\n => (n ** (fb n))) (tail nats)
-- Generate output for the screen. The type system can't help us here!
instance Show (n : Nat ** FB n) where
show (x ** N x) = show x
show (x ** Fizz x) = "Fizz"
show (x ** Buzz x) = "Buzz"
show (x ** FizzBuzz x) = "FizzBuzz"
-- Take the first 100 numbers' FizzBuzzes, then print them to the screen.
namespace Main
main : IO ()
main = sequence_ . map (putStrLn . show) . take 100 $ fizzBuzz
@LeifW
Copy link

LeifW commented Jan 22, 2015

Could also write [1..] to get a Stream of Nats.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment