type-level fizzbuzz in Haskell with singletons

FizzBuzzOne.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

module FizzBuzzOne where

import GHC.TypeLits.Singletons (Mod, SNat, sMod, Symbol, KnownNat)
import Data.Eq.Singletons (PEq(type (==)), SEq ((%==)))
import Data.Bool.Singletons (SBool (STrue, SFalse), (%&&), sIf)
import Data.Singletons (sing, SingKind (fromSing), SomeSing (SomeSing), withSomeSing, SingI, withSingI, Sing)
import Text.Show.Singletons (SShow(sShow_))
import Data.Text (Text, unpack)
import Numeric.Natural (Natural)
import Data.Proxy (Proxy (Proxy))
import GHC.TypeNats (natVal)

type IsMultipleOf n m = 0 == Mod n m

tMod3 :: SNat n -> SBool (IsMultipleOf n 3)
tMod3 sNatN = (sing @0) %== sMod sNatN (sing @3)

tMod5 :: SNat n -> SBool (IsMultipleOf n 5)
tMod5 sNatN = (sing @0) %== sMod sNatN (sing @5)

class FizzBuzz (isMultipleOf3 :: Bool) (isMultipleOf5 :: Bool) where
  fizzBuzz :: String -> String

instance FizzBuzz 'True  'False where fizzBuzz _ = "fizz"
instance FizzBuzz 'False 'True  where fizzBuzz _ = "buzz"
instance FizzBuzz 'True  'True  where fizzBuzz _ = "fizzbuzz"
instance FizzBuzz 'False 'False where fizzBuzz s = s

fizzBuzz' :: forall n. SNat n -> String
fizzBuzz' sNatN =
  case (tMod3 sNatN, tMod5 sNatN) of
    (STrue  :: SBool b1, STrue  :: SBool b2) -> fizzBuzz @b1 @b2 $ showSNat sNatN
    (SFalse :: SBool b1, STrue  :: SBool b2) -> fizzBuzz @b1 @b2 $ showSNat sNatN
    (STrue  :: SBool b1, SFalse :: SBool b2) -> fizzBuzz @b1 @b2 $ showSNat sNatN
    (SFalse :: SBool b1, SFalse :: SBool b2) -> fizzBuzz @b1 @b2 $ showSNat sNatN
  where
  showSNat :: SNat n -> String
  showSNat = unpack . fromSing . sShow_

fizzBuzzVal :: Natural -> String
fizzBuzzVal n = withSomeSing n fizzBuzz'

example :: String
example = fizzBuzz' $ sing @15

FizzBuzzSimple.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NoCUSKs #-}
{-# LANGUAGE NoNamedWildCards #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module FizzBuzzSimple where

import Data.Singletons.Base.TH
import GHC.TypeLits.Singletons
import Prelude.Singletons

$(singletonsOnly [d|
  fizzBuzz :: Nat -> Symbol
  fizzBuzz i
    | 0 == mod i 3 && 0 == mod i 5 = "fizzbuzz"
    | 0 == mod i 3 = "fizz"
    | 0 == mod i 5 = "buzz"
    | otherwise = show_ i
  |])

This is with GHC-9.0.2 and singletons-base-3.0.

Here's an example of using FizzBuzzSimple.hs in GHCi.

Here's the FizzBuzz type-family that is generated:

> :i FizzBuzz
type FizzBuzz :: Nat -> Symbol
type family FizzBuzz a where
  ...
> :k! FizzBuzz 21
FizzBuzz 21 :: Symbol
= "fizz"

and a lifted fizzBuzz function:

> :i sFizzBuzz
sFizzBuzz :: Sing t -> Sing (Apply FizzBuzzSym0 t)
> sFizzBuzz (sing @15)
SSym @"fizzbuzz"