{-# LANGUAGE TemplateHaskell, ConstraintKinds, TypeFamilies, DataKinds, MultiParamTypeClasses #-}
module Acme.NumberSystem where
import GHC.TypeLits
import Language.Haskell.TH
type Less = (<=)
type family Sub (m :: Nat) (n :: Nat) :: Nat
-- | Define the less than relation for numbers up to a number using Template Haskell.
-- | Also define subtraction.
-- | E.g. numberSystem 100
numberSystem :: Integer -> Q [Dec]
numberSystem theBiggestNumber = return . concat $ lessThan ++ subs
where
lessThan = map (\i -> map (\j ->
InstanceD [] (AppT (AppT (ConT (''Less)) (LitT (NumTyLit i))) (LitT (NumTyLit j))) []
) [i..theBiggestNumber]) [0..theBiggestNumber]
subs = map (\i -> map (\j ->
TySynInstD ''Sub [LitT (NumTyLit j), LitT (NumTyLit i)] (LitT (NumTyLit (j - i)))
) [i..theBiggestNumber]) [0..theBiggestNumber]