Last active
June 13, 2019 08:46
-
-
Save tdietert/adc974324fa910841f98bd386f9bc880 to your computer and use it in GitHub Desktop.
A translation of i-am-tom's type-level Fizz Buzz solution using (Xia Li-yao's) First-class type families
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE KindSignatures #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE TypeOperators #-} | |
{-# LANGUAGE UndecidableInstances #-} | |
module FizzBuzz where | |
import Data.Kind (Type) | |
import GHC.TypeLits | |
import Prelude hiding (Functor, Semigroup) | |
type Main = Eval (MapM (Both Fizz Buzz) (0 `To` 100)) | |
--- | |
type Expr k = k -> Type | |
type family Eval (e :: Expr k) :: k | |
data MapM :: (a -> Expr b) -> [a] -> Expr [b] | |
type instance Eval (MapM f '[]) = '[] | |
type instance Eval (MapM f (x ': xs)) = Eval (f x) ': Eval (MapM f xs) | |
--- | |
data (<>) :: k -> k -> Expr k | |
-- instance Semigroup a -> Semigroup (Either e a) | |
type instance Eval ('Left x <> 'Left _) = 'Left x | |
type instance Eval ('Right x <> 'Left _) = 'Right x | |
type instance Eval ('Left _ <> 'Right y) = 'Right y | |
type instance Eval ('Right x <> 'Right y) = 'Right (Eval (x <> y)) | |
type instance Eval ((x :: Symbol) <> (y :: Symbol)) = AppendSymbol x y | |
data Both :: (a -> Expr b) -> (a -> Expr b) -> a -> Expr b | |
type instance Eval (Both f g x) = Eval (Eval (f x) <> Eval (g x)) | |
type family IfZero (p :: Nat) (t :: k) (f :: k) :: k where | |
IfZero 0 t _ = t | |
IfZero _ _ f = f | |
data Fizz :: Nat -> Expr (Either Nat Symbol) | |
type instance Eval (Fizz x) | |
= IfZero (x `Mod` 3) ('Right "Fizz") ('Left x) | |
data Buzz :: Nat -> Expr (Either Nat Symbol) | |
type instance Eval (Buzz x) | |
= IfZero (x `Mod` 5) ('Right "Buzz") ('Left x) | |
type family (x :: Nat) `To` (y :: Nat) :: [Nat] where | |
x `To` x = '[] | |
x `To` y = x ': (x + 1) `To` y |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment