{-# language DataKinds #-}
{-# language DerivingStrategies #-}
{-# language ExplicitNamespaces #-}
{-# language GADTSyntax #-}
{-# language GeneralizedNewtypeDeriving #-}
{-# language KindSignatures #-}
{-# language MagicHash #-}
{-# language RoleAnnotations #-}
{-# language StandaloneDeriving #-}
{-# language TypeOperators #-}
{-# language UnboxedTuples #-}
{-# language UnliftedNewtypes #-}
module Arithmetic.Unsafe
( Nat(..)
, Nat#(..)
, Fin#(..)
, MaybeFin#(..)
, Fin32#(..)
, type (<#)(Lt#)
, type (<=#)(Lte#)
, type (<)(Lt)
, type (<=)(Lte)
, type (:=:)(Eq)
, type (:=:#)(Eq#)
) where
import Prelude hiding ((>=),(<=))
import Control.Category (Category)
import Data.Kind (Type)
import GHC.Exts (Int#,Int32#,TYPE,RuntimeRep(IntRep,Int32Rep,TupleRep))
import qualified Control.Category
import qualified GHC.TypeNats as GHC
infix 4 <
infix 4 <=
infix 4 <#
infix 4 <=#
infix 4 :=:
infix 4 :=:#
newtype Nat (n :: GHC.Nat) = Nat { forall (n :: Nat). Nat n -> Int
getNat :: Int }
type role Nat nominal
deriving newtype instance Show (Nat n)
newtype Nat# :: GHC.Nat -> TYPE 'IntRep where
Nat# :: Int# -> Nat# n
type role Nat# nominal
newtype Fin# :: GHC.Nat -> TYPE 'IntRep where
Fin# :: Int# -> Fin# n
type role Fin# nominal
newtype MaybeFin# :: GHC.Nat -> TYPE 'IntRep where
MaybeFin# :: Int# -> MaybeFin# n
type role MaybeFin# nominal
newtype Fin32# :: GHC.Nat -> TYPE 'Int32Rep where
Fin32# :: Int32# -> Fin32# n
type role Fin32# nominal
data (<) :: GHC.Nat -> GHC.Nat -> Type where
Lt :: a < b
newtype (<#) :: GHC.Nat -> GHC.Nat -> TYPE ('TupleRep '[]) where
Lt# :: (# #) -> a <# b
data (<=) :: GHC.Nat -> GHC.Nat -> Type where
Lte :: a <= b
newtype (<=#) :: GHC.Nat -> GHC.Nat -> TYPE ('TupleRep '[]) where
Lte# :: (# #) -> a <=# b
data (:=:) :: GHC.Nat -> GHC.Nat -> Type where
Eq :: a :=: b
newtype (:=:#) :: GHC.Nat -> GHC.Nat -> TYPE ('TupleRep '[]) where
Eq# :: (# #) -> a :=:# b
instance Category (<=) where
id :: forall (a :: Nat). a <= a
id = a <= a
forall (a :: Nat) (b :: Nat). a <= b
Lte
b <= c
Lte . :: forall (b :: Nat) (c :: Nat) (a :: Nat).
(b <= c) -> (a <= b) -> a <= c
. a <= b
Lte = a <= c
forall (a :: Nat) (b :: Nat). a <= b
Lte
instance Category (:=:) where
id :: forall (a :: Nat). a :=: a
id = a :=: a
forall (a :: Nat) (b :: Nat). a :=: b
Eq
b :=: c
Eq . :: forall (b :: Nat) (c :: Nat) (a :: Nat).
(b :=: c) -> (a :=: b) -> a :=: c
. a :=: b
Eq = a :=: c
forall (a :: Nat) (b :: Nat). a :=: b
Eq