module TypeLevel.Singletons
(The(Truey, Falsy, Nily, (:-))
,KnownSing(..)
,(*.)
,(+.)
,(^.)
,(-.)
,(<=.)
,totalOrder
,type (<=)
,type (Lit.+)
,type (Lit.*)
,type (Lit.^)
,Lit.Nat)
where
import Data.Kind
import qualified GHC.TypeLits as Lit
import Data.Proxy
import Data.Type.Equality
import Data.Coerce
import Unsafe.Coerce
data family The k :: k -> *
data instance The Bool x where
Falsy :: The Bool 'False
Truey :: The Bool 'True
infixr 5 :-
data instance The [k] xs where
Nily :: The [k] '[]
(:-) :: The k x -> The [k] xs -> The [k] (x ': xs)
class KnownSing (x :: k) where
sing :: The k x
instance KnownSing 'True where
sing = Truey
instance KnownSing 'False where
sing = Falsy
instance KnownSing '[] where
sing = Nily
instance (KnownSing xs, KnownSing x) =>
KnownSing (x ': xs) where
sing = sing :- sing
newtype instance The Lit.Nat n where
NatSing :: Integer -> The Lit.Nat n
instance Lit.KnownNat n => KnownSing n where
sing = NatSing $ Prelude.fromInteger $ Lit.natVal (Proxy :: Proxy n)
infixl 6 +.
(+.) :: The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.+ m)
(+.) =
(coerce :: (Integer -> Integer -> Integer) -> The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.+ m))
(Prelude.+)
infixl 7 *.
(*.) :: The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.* m)
(*.) =
(coerce :: (Integer -> Integer -> Integer) -> The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.* m))
(Prelude.*)
infixr 8 ^.
(^.) :: The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.^ m)
(^.) =
(coerce :: (Integer -> Integer -> Integer) -> The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.^ m))
(Prelude.^)
infixl 6 -.
(-.) :: (m Lit.<= n) => The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.- m)
(-.) =
(coerce :: (Integer -> Integer -> Integer) -> The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.- m))
(Prelude.-)
infix 4 <=.
(<=.) :: The Lit.Nat n -> The Lit.Nat m -> The Bool (n Lit.<=? m)
(<=.) (NatSing x :: The Lit.Nat n) (NatSing y :: The Lit.Nat m)
| x <= y = case (unsafeCoerce (Refl :: 'True :~: 'True) :: (n Lit.<=? m) :~: 'True) of
Refl -> Truey
| otherwise = case (unsafeCoerce (Refl :: 'True :~: 'True) :: (n Lit.<=? m) :~: 'False) of
Refl -> Falsy
totalOrder :: p n -> q m -> (n Lit.<=? m) :~: 'False -> (m Lit.<=? n) :~: 'True
totalOrder (_ :: p n) (_ :: q m) Refl = unsafeCoerce Refl :: (m Lit.<=? n) :~: 'True
type x <= y = (x Lit.<=? y) :~: 'True