{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# 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#, RuntimeRep (Int32Rep, IntRep, TupleRep), TYPE)
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