module Data.Singletons.Prelude.Num (
PNum(..), SNum(..), Subtract, sSubtract,
(:+$), (:+$$), (:+$$$),
(:-$), (:-$$), (:-$$$),
(:*$), (:*$$), (:*$$$),
NegateSym0, NegateSym1,
AbsSym0, AbsSym1,
SignumSym0, SignumSym1,
FromIntegerSym0, FromIntegerSym1,
SubtractSym0, SubtractSym1, SubtractSym2
) where
import Data.Singletons.Single
import Data.Singletons
import Data.Singletons.TypeLits.Internal
import Data.Singletons.Decide
import GHC.TypeLits
import Data.Proxy
import Unsafe.Coerce
$(singletonsOnly [d|
class Num a where
(+), (), (*) :: a -> a -> a
infixl 6 +
infixl 6
infixl 6 *
negate :: a -> a
abs :: a -> a
signum :: a -> a
fromInteger :: Nat -> a
x y = x + negate y
negate x = 0 x
|])
type family SignumNat (a :: Nat) :: Nat where
SignumNat 0 = 0
SignumNat x = 1
instance PNum ('KProxy :: KProxy Nat) where
type a :+ b = a + b
type a :- b = a b
type a :* b = a * b
type Negate (a :: Nat) = Error "Cannot negate a natural number"
type Abs (a :: Nat) = a
type Signum a = SignumNat a
type FromInteger a = a
instance SNum ('KProxy :: KProxy Nat) where
sa %:+ sb =
let a = fromSing sa
b = fromSing sb
ex = someNatVal (a + b)
in
case ex of
Just (SomeNat (_ :: Proxy ab)) -> unsafeCoerce (SNat :: Sing ab)
Nothing -> error "Two naturals added to a negative?"
sa %:- sb =
let a = fromSing sa
b = fromSing sb
ex = someNatVal (a b)
in
case ex of
Just (SomeNat (_ :: Proxy ab)) -> unsafeCoerce (SNat :: Sing ab)
Nothing ->
error "Negative natural-number singletons are naturally not allowed."
sa %:* sb =
let a = fromSing sa
b = fromSing sb
ex = someNatVal (a * b)
in
case ex of
Just (SomeNat (_ :: Proxy ab)) -> unsafeCoerce (SNat :: Sing ab)
Nothing ->
error "Two naturals multiplied to a negative?"
sNegate _ = error "Cannot call sNegate on a natural number singleton."
sAbs x = x
sSignum sx =
case sx %~ (sing :: Sing 0) of
Proved Refl -> sing :: Sing 0
Disproved _ -> unsafeCoerce (sing :: Sing 1)
sFromInteger x = x
$(singletonsOnly [d|
subtract :: Num a => a -> a -> a
subtract x y = y x
|])