Add EitherFin#

src/Arithmetic/Types.hs

@@ -22,6 +22,11 @@ module Arithmetic.Types
   , pattern MaybeFinJust#
   , pattern MaybeFinNothing#
 
+    -- * Either Fin
+  , EitherFin#
+  , pattern EitherFinLeft#
+  , pattern EitherFinRight#
+
     -- * Infix Operators
   , type (<)
   , type (<=)
@@ -31,8 +36,9 @@ module Arithmetic.Types
   , type (:=:#)
   ) where
 
-import Arithmetic.Unsafe (Fin# (Fin#), Fin32#, MaybeFin# (..), Nat (getNat), Nat#, (:=:#), type (:=:), type (<), type (<#), type (<=), type (<=#))
+import Arithmetic.Unsafe (EitherFin# (..), Fin# (Fin#), Fin32#, MaybeFin# (..), Nat (getNat), Nat#, (:=:#), type (:=:), type (<), type (<#), type (<=), type (<=#))
 import Data.Kind (type Type)
+import GHC.Exts ((-#), (<#))
 import GHC.TypeNats (type (+))
 
 import qualified GHC.TypeNats as GHC
@@ -70,6 +76,21 @@ instance Eq (Fin n) where
 instance Ord (Fin n) where
   Fin x _ `compare` Fin y _ = compare (getNat x) (getNat y)
 
+pattern EitherFinLeft# :: Fin# m -> EitherFin# m n
+pattern EitherFinLeft# f <- (eitherFinToSum# -> (# f | #))
+  where
+    EitherFinLeft# (Fin# i) = EitherFin# (1# -# i)
+
+pattern EitherFinRight# :: Fin# n -> EitherFin# m n
+pattern EitherFinRight# f <- (eitherFinToSum# -> (# | f #))
+  where
+    EitherFinRight# (Fin# i) = EitherFin# i
+
+eitherFinToSum# :: EitherFin# m n -> (# Fin# m | Fin# n #)
+eitherFinToSum# (EitherFin# i) = case i <# 0# of
+  1# -> (# Fin# ((-1#) -# i) | #)
+  _ -> (# | Fin# i #)
+
 pattern MaybeFinJust# :: Fin# n -> MaybeFin# n
 pattern MaybeFinJust# f <- (maybeFinToFin# -> (# | f #))
   where

src/Arithmetic/Unsafe.hs

@@ -15,6 +15,7 @@ module Arithmetic.Unsafe
   , Nat# (..)
   , Fin# (..)
   , MaybeFin# (..)
+  , EitherFin# (..)
   , Fin32# (..)
   , type (<#) (Lt#)
   , type (<=#) (Lte#)
@@ -73,6 +74,16 @@ newtype MaybeFin# :: GHC.Nat -> TYPE 'IntRep where
 
 type role MaybeFin# nominal
 
+{- | Either a @Fin#@ bounded by the left natural or one bounded
+by the right natural.
+-}
+newtype EitherFin# :: GHC.Nat -> GHC.Nat -> TYPE 'IntRep where
+  -- Implementation note: Left is represented by (-m + 1), and
+  -- right is represented by n.
+  EitherFin# :: Int# -> EitherFin# m n
+
+type role EitherFin# nominal nominal
+
 -- | Variant of 'Fin#' that only allows 32-bit integers.
 newtype Fin32# :: GHC.Nat -> TYPE 'Int32Rep where
   Fin32# :: Int32# -> Fin32# n