commit 7c1f92264abf397e76b0339df247b53c20f7ed34
parent 0896fd2d14acf5c75597c778b2685941313c2112
Author: Robert Russell <robert@rr3.xyz>
Date: Sun, 29 Jun 2025 17:34:26 -0700
Rename package from Snats to Naturals
Diffstat:
33 files changed, 549 insertions(+), 549 deletions(-)
diff --git a/package.yaml b/package.yaml
@@ -1,4 +1,4 @@
-name: snats
+name: naturals
author: Robert Russell
ghc-options:
diff --git a/src/Naturals/Nat.hs b/src/Naturals/Nat.hs
@@ -0,0 +1,34 @@
+module Naturals.Nat (
+ Nat,
+ ToNat (..),
+ FromNat (..),
+) where
+
+-- | Word-sized natural numbers.
+newtype Nat = Nat Word deriving newtype (Show, Eq, Ord, Enum, Bounded, Num, Real, Integral)
+
+-- | Types supporting conversion to @Nat@.
+--
+-- If @a@ also implements @FromNat@, then @toNat@ and @fromNat@ should be
+-- inverses.
+class ToNat a where
+ toNat :: a -> Nat
+
+-- | Types supporting conversion from @Nat@.
+--
+-- If @a@ also implements @ToNat@, then @toNat@ and @fromNat@ should be
+-- inverses.
+class FromNat a where
+ fromNat :: Nat -> a
+
+instance ToNat Nat where
+ toNat = id
+
+instance FromNat Nat where
+ fromNat = id
+
+instance ToNat Word where
+ toNat = Nat
+
+instance FromNat Word where
+ fromNat (Nat n) = n
diff --git a/src/Naturals/Natural.hs b/src/Naturals/Natural.hs
@@ -0,0 +1,27 @@
+module Naturals.Natural (
+ Natural,
+ ToNatural (..),
+ FromNatural (..),
+) where
+
+import Numeric.Natural
+
+-- | Types supporting conversion to @Natural@.
+--
+-- If @a@ also implements @FromNatural@, then @toNatural@ and @fromNatural@
+-- should be inverses.
+class ToNatural a where
+ toNatural :: a -> Natural
+
+-- | Types supporting conversion from @Natural@.
+--
+-- If @a@ also implements @ToNatural@, then @toNatural@ and @fromNatural@
+-- should be inverses.
+class FromNatural a where
+ fromNatural :: Natural -> a
+
+instance ToNatural Natural where
+ toNatural = id
+
+instance FromNatural Natural where
+ fromNatural = id
diff --git a/src/Naturals/Peano.hs b/src/Naturals/Peano.hs
@@ -0,0 +1,7 @@
+module Naturals.Peano (
+ module Naturals.Peano.Alias,
+ module Naturals.Peano.Prim,
+) where
+
+import Naturals.Peano.Alias
+import Naturals.Peano.Prim
diff --git a/src/Naturals/Peano/Alias.hs b/src/Naturals/Peano/Alias.hs
@@ -0,0 +1,47 @@
+module Naturals.Peano.Alias where
+
+import Naturals.Peano.Prim
+
+pattern SZ, SSZ, SSSZ, SSSSZ, SSSSSZ, SSSSSSZ, SSSSSSSZ, SSSSSSSSZ, SSSSSSSSSZ :: Peano
+pattern SZ = S Z
+pattern SSZ = S SZ
+pattern SSSZ = S SSZ
+pattern SSSSZ = S SSSZ
+pattern SSSSSZ = S SSSSZ
+pattern SSSSSSZ = S SSSSSZ
+pattern SSSSSSSZ = S SSSSSSZ
+pattern SSSSSSSSZ = S SSSSSSSZ
+pattern SSSSSSSSSZ = S SSSSSSSSZ
+
+type SZ = S Z
+type SSZ = S SZ
+type SSSZ = S SSZ
+type SSSSZ = S SSSZ
+type SSSSSZ = S SSSSZ
+type SSSSSSZ = S SSSSSZ
+type SSSSSSSZ = S SSSSSSZ
+type SSSSSSSSZ = S SSSSSSSZ
+type SSSSSSSSSZ = S SSSSSSSSZ
+
+pattern Peano0, Peano1, Peano2, Peano3, Peano4, Peano5, Peano6, Peano7, Peano8, Peano9 :: Peano
+pattern Peano0 = Z
+pattern Peano1 = SZ
+pattern Peano2 = SSZ
+pattern Peano3 = SSSZ
+pattern Peano4 = SSSSZ
+pattern Peano5 = SSSSSZ
+pattern Peano6 = SSSSSSZ
+pattern Peano7 = SSSSSSSZ
+pattern Peano8 = SSSSSSSSZ
+pattern Peano9 = SSSSSSSSSZ
+
+type Peano0 = Z
+type Peano1 = SZ
+type Peano2 = SSZ
+type Peano3 = SSSZ
+type Peano4 = SSSSZ
+type Peano5 = SSSSSZ
+type Peano6 = SSSSSSZ
+type Peano7 = SSSSSSSZ
+type Peano8 = SSSSSSSSZ
+type Peano9 = SSSSSSSSSZ
diff --git a/src/Naturals/Peano/Prim.hs b/src/Naturals/Peano/Prim.hs
@@ -0,0 +1,76 @@
+module Naturals.Peano.Prim (
+ Peano (..),
+ peanoShow,
+ peano,
+ peanoRec,
+ peanoFold,
+ Add,
+) where
+
+import Control.Exception
+
+import Naturals.Natural
+
+-- | Unary natural numbers.
+-- Intended mainly for use at the type-level via DataKinds.
+data Peano = Z | S Peano deriving (Eq)
+
+instance Show Peano where
+ show = show . toNatural
+
+-- | A variant of @show \@Peano@ that uses unary notation instead of decimal.
+peanoShow :: Peano -> String
+peanoShow Z = "Z"
+peanoShow (S n) = 'S' : peanoShow n
+
+instance Ord Peano where
+ Z `compare` Z = EQ
+ S _ `compare` Z = GT
+ Z `compare` S _ = LT
+ S m `compare` S n = m `compare` n
+
+instance Num Peano where
+ Z + n = n
+ S m + n = S (m + n)
+
+ n - Z = n
+ _ - S _ = throw Underflow
+
+ Z * _ = Z
+ S m * n = m * n + n
+
+ abs n = n
+
+ signum Z = Z
+ signum (S _) = S Z
+
+ fromInteger 0 = Z
+ fromInteger n
+ | n > 0 = S (fromInteger (n - 1))
+ | otherwise = throw Underflow
+
+instance ToNatural Peano where
+ toNatural Z = 0
+ toNatural (S n) = succ (toNatural n)
+
+instance FromNatural Peano where
+ fromNatural 0 = Z
+ fromNatural n = S (fromNatural (pred n))
+
+-- | The (nonrecursive) eliminator for @Peano@ (equivalent to a case expression).
+peano :: a -> (Peano -> a) -> Peano -> a
+peano z _ Z = z
+peano _ s (S m) = s m
+
+-- | The recursor for @Peano@.
+peanoRec :: a -> (Peano -> a -> a) -> Peano -> a
+peanoRec z _ Z = z
+peanoRec z s (S m) = s m (peanoRec z s m)
+
+-- | The catamorphism for @Peano@.
+peanoFold :: a -> (a -> a) -> Peano -> a
+peanoFold z s = peanoRec z (const s)
+
+type family Add (x :: Peano) (y :: Peano) :: Peano where
+ Add Z n = n
+ Add (S m) n = S (Add m n)
diff --git a/src/Naturals/Snat.hs b/src/Naturals/Snat.hs
@@ -0,0 +1,9 @@
+module Naturals.Snat (
+ module Naturals.Peano,
+ module Naturals.Snat.Alias,
+ module Naturals.Snat.Prim,
+) where
+
+import Naturals.Peano
+import Naturals.Snat.Alias
+import Naturals.Snat.Prim
diff --git a/src/Naturals/Snat/Alias.hs b/src/Naturals/Snat/Alias.hs
@@ -0,0 +1,34 @@
+module Naturals.Snat.Alias where
+
+import Naturals.Peano
+import Naturals.Snat.Prim
+
+pattern Snat0 :: Snat Peano0
+pattern Snat0 = Zero
+
+pattern Snat1 :: Snat Peano1
+pattern Snat1 = Succ Snat0
+
+pattern Snat2 :: Snat Peano2
+pattern Snat2 = Succ Snat1
+
+pattern Snat3 :: Snat Peano3
+pattern Snat3 = Succ Snat2
+
+pattern Snat4 :: Snat Peano4
+pattern Snat4 = Succ Snat3
+
+pattern Snat5 :: Snat Peano5
+pattern Snat5 = Succ Snat4
+
+pattern Snat6 :: Snat Peano6
+pattern Snat6 = Succ Snat5
+
+pattern Snat7 :: Snat Peano7
+pattern Snat7 = Succ Snat6
+
+pattern Snat8 :: Snat Peano8
+pattern Snat8 = Succ Snat7
+
+pattern Snat9 :: Snat Peano9
+pattern Snat9 = Succ Snat8
diff --git a/src/Naturals/Snat/Prim.hs b/src/Naturals/Snat/Prim.hs
@@ -0,0 +1,46 @@
+module Naturals.Snat.Prim (
+ Snat,
+ pattern Zero,
+ pattern Succ,
+ snat,
+ snatInd,
+ snatRec,
+ snatFold,
+ snatPred,
+ snatAdd,
+) where
+
+import Data.Coerce
+import Data.Functor.Const
+
+import Naturals.Peano
+import Naturals.Snat.Unsafe (Snat, snatAdd, snatPeel, snatSucc, snatZero)
+import Naturals.Speano hiding (Succ, Zero)
+
+pattern Zero :: () => (n ~ Z) => Snat n
+pattern Zero <- (snatPeel -> ZeroOp) where Zero = snatZero
+pattern Succ :: () => (n ~ S m) => Snat m -> Snat n
+pattern Succ p <- (snatPeel -> SuccOp p) where Succ = snatSucc
+{-# COMPLETE Zero, Succ #-}
+
+-- | The (nonrecursive) eliminator for @Snat@ (equivalent to a case expression
+-- with @Zero@ and @Succ@).
+snat :: ((n ~ Z) => a) -> (forall m. (n ~ S m) => Snat m -> a) -> Snat n -> a
+snat z _ Zero = z
+snat _ s (Succ m) = s m
+
+-- | Induction for @Snat@.
+snatInd :: f Z -> (forall m. Snat m -> f m -> f (S m)) -> Snat n -> f n
+snatInd z _ Zero = z
+snatInd z s (Succ m) = s m (snatInd z s m)
+
+-- | The (nondependent) recursor for @Snat@.
+snatRec :: forall a n. a -> (forall m. Snat m -> a -> a) -> Snat n -> a
+snatRec = coerce $ snatInd @(Const a) @n
+
+-- | The catamorphism for @Snat@.
+snatFold :: a -> (a -> a) -> Snat n -> a
+snatFold z s = snatRec z (const s)
+
+snatPred :: Snat (S n) -> Snat n
+snatPred (Succ n) = n
diff --git a/src/Naturals/Snat/Unsafe.hs b/src/Naturals/Snat/Unsafe.hs
@@ -0,0 +1,35 @@
+module Naturals.Snat.Unsafe where
+
+import GHC.Natural
+import Unsafe.Coerce
+
+import Naturals.Nat
+import Naturals.Natural
+import Naturals.Peano
+import Naturals.Speano
+
+-- | Singleton (@Peano@-indexed) natural numbers represented as a @Nat@.
+newtype Snat (n :: Peano) = SnatUnsafe Nat deriving newtype (Show, Eq)
+
+instance ToNat (Snat n) where
+ toNat (SnatUnsafe n) = n
+
+instance ToNatural (Snat a) where
+ toNatural = wordToNatural . fromNat . toNat
+
+snatZero :: Snat Z
+snatZero = SnatUnsafe 0
+
+snatSucc :: Snat n -> Snat (S n)
+snatSucc (SnatUnsafe n) = SnatUnsafe (succ n)
+
+-- | Peel the outermost unary constructor off a @Snat@, obtaining a result
+-- suitable for shallow pattern matching.
+--
+-- We only use @snatPeel@ to implement pattern synonyms.
+snatPeel :: Snat n -> SpeanoSig Snat n
+snatPeel (SnatUnsafe 0) = unsafeCoerce ZeroOp
+snatPeel (SnatUnsafe n) = unsafeCoerce SuccOp (SnatUnsafe (pred n))
+
+snatAdd :: Snat m -> Snat n -> Snat (Add m n)
+snatAdd (SnatUnsafe m) (SnatUnsafe n) = SnatUnsafe (m + n)
diff --git a/src/Naturals/Snatural.hs b/src/Naturals/Snatural.hs
@@ -0,0 +1,9 @@
+module Naturals.Snatural (
+ module Naturals.Peano,
+ module Naturals.Snatural.Alias,
+ module Naturals.Snatural.Prim,
+) where
+
+import Naturals.Peano
+import Naturals.Snatural.Alias
+import Naturals.Snatural.Prim
diff --git a/src/Naturals/Snatural/Alias.hs b/src/Naturals/Snatural/Alias.hs
@@ -0,0 +1,34 @@
+module Naturals.Snatural.Alias where
+
+import Naturals.Peano
+import Naturals.Snatural.Prim
+
+pattern Snat0 :: Snatural Peano0
+pattern Snat0 = Zero
+
+pattern Snat1 :: Snatural Peano1
+pattern Snat1 = Succ Snat0
+
+pattern Snat2 :: Snatural Peano2
+pattern Snat2 = Succ Snat1
+
+pattern Snat3 :: Snatural Peano3
+pattern Snat3 = Succ Snat2
+
+pattern Snat4 :: Snatural Peano4
+pattern Snat4 = Succ Snat3
+
+pattern Snat5 :: Snatural Peano5
+pattern Snat5 = Succ Snat4
+
+pattern Snat6 :: Snatural Peano6
+pattern Snat6 = Succ Snat5
+
+pattern Snat7 :: Snatural Peano7
+pattern Snat7 = Succ Snat6
+
+pattern Snat8 :: Snatural Peano8
+pattern Snat8 = Succ Snat7
+
+pattern Snat9 :: Snatural Peano9
+pattern Snat9 = Succ Snat8
diff --git a/src/Naturals/Snatural/Prim.hs b/src/Naturals/Snatural/Prim.hs
@@ -0,0 +1,46 @@
+module Naturals.Snatural.Prim (
+ Snatural,
+ pattern Zero,
+ pattern Succ,
+ snatural,
+ snaturalInd,
+ snaturalRec,
+ snaturalFold,
+ snaturalPred,
+ snaturalAdd,
+) where
+
+import Data.Coerce
+import Data.Functor.Const
+
+import Naturals.Peano
+import Naturals.Snatural.Unsafe (Snatural, snaturalAdd, snaturalPeel, snaturalSucc, snaturalZero)
+import Naturals.Speano hiding (Succ, Zero)
+
+pattern Zero :: () => (n ~ Z) => Snatural n
+pattern Zero <- (snaturalPeel -> ZeroOp) where Zero = snaturalZero
+pattern Succ :: () => (n ~ S m) => Snatural m -> Snatural n
+pattern Succ p <- (snaturalPeel -> SuccOp p) where Succ = snaturalSucc
+{-# COMPLETE Zero, Succ #-}
+
+-- | The (nonrecursive) eliminator for @Snatural@ (equivalent to a case
+-- expression with @Zero@ and @Succ@).
+snatural :: ((n ~ Z) => a) -> (forall m. (n ~ S m) => Snatural m -> a) -> Snatural n -> a
+snatural z _ Zero = z
+snatural _ s (Succ m) = s m
+
+-- | Induction for @Snatural@.
+snaturalInd :: f Z -> (forall m. Snatural m -> f m -> f (S m)) -> Snatural n -> f n
+snaturalInd z _ Zero = z
+snaturalInd z s (Succ m) = s m (snaturalInd z s m)
+
+-- | The (nondependent) recursor for @Snatural@.
+snaturalRec :: forall a n. a -> (forall m. Snatural m -> a -> a) -> Snatural n -> a
+snaturalRec = coerce $ snaturalInd @(Const a) @n
+
+-- | The catamorphism for @Snatural@.
+snaturalFold :: a -> (a -> a) -> Snatural n -> a
+snaturalFold z s = snaturalRec z (const s)
+
+snaturalPred :: Snatural (S n) -> Snatural n
+snaturalPred (Succ n) = n
diff --git a/src/Naturals/Snatural/Unsafe.hs b/src/Naturals/Snatural/Unsafe.hs
@@ -0,0 +1,30 @@
+module Naturals.Snatural.Unsafe where
+
+import Unsafe.Coerce
+
+import Naturals.Natural
+import Naturals.Peano
+import Naturals.Speano
+
+-- | Singleton (@Peano@-indexed) natural numbers represented as a @Natural@.
+newtype Snatural (n :: Peano) = SnaturalUnsafe Natural deriving (Show, Eq)
+
+instance ToNatural (Snatural n) where
+ toNatural (SnaturalUnsafe n) = n
+
+snaturalZero :: Snatural Z
+snaturalZero = SnaturalUnsafe 0
+
+snaturalSucc :: Snatural n -> Snatural (S n)
+snaturalSucc (SnaturalUnsafe n) = SnaturalUnsafe (succ n)
+
+-- | Peel the outermost unary constructor off a @Snatural@, obtaining a result
+-- suitable for shallow pattern matching.
+--
+-- We only use @snaturalPeel@ to implement pattern synonyms.
+snaturalPeel :: Snatural n -> SpeanoSig Snatural n
+snaturalPeel (SnaturalUnsafe 0) = unsafeCoerce ZeroOp
+snaturalPeel (SnaturalUnsafe n) = unsafeCoerce SuccOp (SnaturalUnsafe (pred n))
+
+snaturalAdd :: Snatural m -> Snatural n -> Snatural (Add m n)
+snaturalAdd (SnaturalUnsafe m) (SnaturalUnsafe n) = SnaturalUnsafe (m + n)
diff --git a/src/Naturals/Speano.hs b/src/Naturals/Speano.hs
@@ -0,0 +1,9 @@
+module Naturals.Speano (
+ module Naturals.Peano,
+ module Naturals.Speano.Alias,
+ module Naturals.Speano.Prim,
+) where
+
+import Naturals.Peano
+import Naturals.Speano.Alias
+import Naturals.Speano.Prim
diff --git a/src/Naturals/Speano/Alias.hs b/src/Naturals/Speano/Alias.hs
@@ -0,0 +1,34 @@
+module Naturals.Speano.Alias where
+
+import Naturals.Peano
+import Naturals.Speano.Prim
+
+pattern Speano0 :: Speano Peano0
+pattern Speano0 = Zero
+
+pattern Speano1 :: Speano Peano1
+pattern Speano1 = Succ Speano0
+
+pattern Speano2 :: Speano Peano2
+pattern Speano2 = Succ Speano1
+
+pattern Speano3 :: Speano Peano3
+pattern Speano3 = Succ Speano2
+
+pattern Speano4 :: Speano Peano4
+pattern Speano4 = Succ Speano3
+
+pattern Speano5 :: Speano Peano5
+pattern Speano5 = Succ Speano4
+
+pattern Speano6 :: Speano Peano6
+pattern Speano6 = Succ Speano5
+
+pattern Speano7 :: Speano Peano7
+pattern Speano7 = Succ Speano6
+
+pattern Speano8 :: Speano Peano8
+pattern Speano8 = Succ Speano7
+
+pattern Speano9 :: Speano Peano9
+pattern Speano9 = Succ Speano8
diff --git a/src/Naturals/Speano/Prim.hs b/src/Naturals/Speano/Prim.hs
@@ -0,0 +1,71 @@
+module Naturals.Speano.Prim (
+ SpeanoSig (..),
+ Speano (..),
+ speanoShow,
+ speano,
+ speanoInd,
+ speanoRec,
+ speanoFold,
+ speanoPred,
+ speanoAdd,
+) where
+
+import Data.Coerce
+import Data.Functor.Const
+
+import Naturals.Natural
+import Naturals.Peano
+
+-- | The "signature" of singleton (@Peano@-indexed) natural numbers:
+-- @SpeanoSig@ is to @Speano@ as @Maybe@ is to @Peano@.
+data SpeanoSig f n where
+ ZeroOp :: SpeanoSig f Z
+ SuccOp :: f n -> SpeanoSig f (S n)
+
+-- | Singleton (@Peano@-indexed) unary natural numbers.
+--
+-- @Speano@ is implemented as a GADT, and hence is inefficient.
+-- See @Snat@ and @Snatural@ for efficient alternatives.
+data Speano n where
+ Zero :: Speano Z
+ Succ :: Speano n -> Speano (S n)
+
+deriving instance Eq (Speano n)
+
+instance Show (Speano n) where
+ show = show . toNatural
+
+-- | A variant of @show \@(Speano n)@ that uses unary notation instead of decimal.
+speanoShow :: Speano n -> String
+speanoShow Zero = "Z"
+speanoShow (Succ n) = 'S' : speanoShow n
+
+instance ToNatural (Speano n) where
+ toNatural Zero = 0
+ toNatural (Succ n) = succ (toNatural n)
+
+-- | The (nonrecursive) eliminator for @Speano@ (equivalent to a case
+-- expression).
+speano :: ((n ~ Z) => a) -> (forall m. (n ~ S m) => Speano m -> a) -> Speano n -> a
+speano z _ Zero = z
+speano _ s (Succ m) = s m
+
+-- | Induction for @Speano@.
+speanoInd :: f Z -> (forall m. Speano m -> f m -> f (S m)) -> Speano n -> f n
+speanoInd z _ Zero = z
+speanoInd z s (Succ m) = s m (speanoInd z s m)
+
+-- | The (nondependent) recursor for @Speano@.
+speanoRec :: forall a n. a -> (forall m. Speano m -> a -> a) -> Speano n -> a
+speanoRec = coerce $ speanoInd @(Const a) @n
+
+-- | The catamorphism for @Speano@.
+speanoFold :: a -> (a -> a) -> Speano n -> a
+speanoFold z s = speanoRec z (const s)
+
+speanoPred :: Speano (S n) -> Speano n
+speanoPred (Succ n) = n
+
+speanoAdd :: Speano m -> Speano n -> Speano (Add m n)
+speanoAdd Zero n = n
+speanoAdd (Succ m) n = Succ (speanoAdd m n)
diff --git a/src/Snats/Nat.hs b/src/Snats/Nat.hs
@@ -1,34 +0,0 @@
-module Snats.Nat (
- Nat,
- ToNat (..),
- FromNat (..),
-) where
-
--- | Word-sized natural numbers.
-newtype Nat = Nat Word deriving newtype (Show, Eq, Ord, Enum, Bounded, Num, Real, Integral)
-
--- | Types supporting conversion to @Nat@.
---
--- If @a@ also implements @FromNat@, then @toNat@ and @fromNat@ should be
--- inverses.
-class ToNat a where
- toNat :: a -> Nat
-
--- | Types supporting conversion from @Nat@.
---
--- If @a@ also implements @ToNat@, then @toNat@ and @fromNat@ should be
--- inverses.
-class FromNat a where
- fromNat :: Nat -> a
-
-instance ToNat Nat where
- toNat = id
-
-instance FromNat Nat where
- fromNat = id
-
-instance ToNat Word where
- toNat = Nat
-
-instance FromNat Word where
- fromNat (Nat n) = n
diff --git a/src/Snats/Natural.hs b/src/Snats/Natural.hs
@@ -1,27 +0,0 @@
-module Snats.Natural (
- Natural,
- ToNatural (..),
- FromNatural (..),
-) where
-
-import Numeric.Natural
-
--- | Types supporting conversion to @Natural@.
---
--- If @a@ also implements @FromNatural@, then @toNatural@ and @fromNatural@
--- should be inverses.
-class ToNatural a where
- toNatural :: a -> Natural
-
--- | Types supporting conversion from @Natural@.
---
--- If @a@ also implements @ToNatural@, then @toNatural@ and @fromNatural@
--- should be inverses.
-class FromNatural a where
- fromNatural :: Natural -> a
-
-instance ToNatural Natural where
- toNatural = id
-
-instance FromNatural Natural where
- fromNatural = id
diff --git a/src/Snats/Peano.hs b/src/Snats/Peano.hs
@@ -1,7 +0,0 @@
-module Snats.Peano (
- module Snats.Peano.Alias,
- module Snats.Peano.Prim,
-) where
-
-import Snats.Peano.Alias
-import Snats.Peano.Prim
diff --git a/src/Snats/Peano/Alias.hs b/src/Snats/Peano/Alias.hs
@@ -1,47 +0,0 @@
-module Snats.Peano.Alias where
-
-import Snats.Peano.Prim
-
-pattern SZ, SSZ, SSSZ, SSSSZ, SSSSSZ, SSSSSSZ, SSSSSSSZ, SSSSSSSSZ, SSSSSSSSSZ :: Peano
-pattern SZ = S Z
-pattern SSZ = S SZ
-pattern SSSZ = S SSZ
-pattern SSSSZ = S SSSZ
-pattern SSSSSZ = S SSSSZ
-pattern SSSSSSZ = S SSSSSZ
-pattern SSSSSSSZ = S SSSSSSZ
-pattern SSSSSSSSZ = S SSSSSSSZ
-pattern SSSSSSSSSZ = S SSSSSSSSZ
-
-type SZ = S Z
-type SSZ = S SZ
-type SSSZ = S SSZ
-type SSSSZ = S SSSZ
-type SSSSSZ = S SSSSZ
-type SSSSSSZ = S SSSSSZ
-type SSSSSSSZ = S SSSSSSZ
-type SSSSSSSSZ = S SSSSSSSZ
-type SSSSSSSSSZ = S SSSSSSSSZ
-
-pattern Peano0, Peano1, Peano2, Peano3, Peano4, Peano5, Peano6, Peano7, Peano8, Peano9 :: Peano
-pattern Peano0 = Z
-pattern Peano1 = SZ
-pattern Peano2 = SSZ
-pattern Peano3 = SSSZ
-pattern Peano4 = SSSSZ
-pattern Peano5 = SSSSSZ
-pattern Peano6 = SSSSSSZ
-pattern Peano7 = SSSSSSSZ
-pattern Peano8 = SSSSSSSSZ
-pattern Peano9 = SSSSSSSSSZ
-
-type Peano0 = Z
-type Peano1 = SZ
-type Peano2 = SSZ
-type Peano3 = SSSZ
-type Peano4 = SSSSZ
-type Peano5 = SSSSSZ
-type Peano6 = SSSSSSZ
-type Peano7 = SSSSSSSZ
-type Peano8 = SSSSSSSSZ
-type Peano9 = SSSSSSSSSZ
diff --git a/src/Snats/Peano/Prim.hs b/src/Snats/Peano/Prim.hs
@@ -1,76 +0,0 @@
-module Snats.Peano.Prim (
- Peano (..),
- peanoShow,
- peano,
- peanoRec,
- peanoFold,
- Add,
-) where
-
-import Control.Exception
-
-import Snats.Natural
-
--- | Unary natural numbers.
--- Intended mainly for use at the type-level via DataKinds.
-data Peano = Z | S Peano deriving (Eq)
-
-instance Show Peano where
- show = show . toNatural
-
--- | A variant of @show \@Peano@ that uses unary notation instead of decimal.
-peanoShow :: Peano -> String
-peanoShow Z = "Z"
-peanoShow (S n) = 'S' : peanoShow n
-
-instance Ord Peano where
- Z `compare` Z = EQ
- S _ `compare` Z = GT
- Z `compare` S _ = LT
- S m `compare` S n = m `compare` n
-
-instance Num Peano where
- Z + n = n
- S m + n = S (m + n)
-
- n - Z = n
- _ - S _ = throw Underflow
-
- Z * _ = Z
- S m * n = m * n + n
-
- abs n = n
-
- signum Z = Z
- signum (S _) = S Z
-
- fromInteger 0 = Z
- fromInteger n
- | n > 0 = S (fromInteger (n - 1))
- | otherwise = throw Underflow
-
-instance ToNatural Peano where
- toNatural Z = 0
- toNatural (S n) = succ (toNatural n)
-
-instance FromNatural Peano where
- fromNatural 0 = Z
- fromNatural n = S (fromNatural (pred n))
-
--- | The (nonrecursive) eliminator for @Peano@ (equivalent to a case expression).
-peano :: a -> (Peano -> a) -> Peano -> a
-peano z _ Z = z
-peano _ s (S m) = s m
-
--- | The recursor for @Peano@.
-peanoRec :: a -> (Peano -> a -> a) -> Peano -> a
-peanoRec z _ Z = z
-peanoRec z s (S m) = s m (peanoRec z s m)
-
--- | The catamorphism for @Peano@.
-peanoFold :: a -> (a -> a) -> Peano -> a
-peanoFold z s = peanoRec z (const s)
-
-type family Add (x :: Peano) (y :: Peano) :: Peano where
- Add Z n = n
- Add (S m) n = S (Add m n)
diff --git a/src/Snats/Snat.hs b/src/Snats/Snat.hs
@@ -1,9 +0,0 @@
-module Snats.Snat (
- module Snats.Peano,
- module Snats.Snat.Alias,
- module Snats.Snat.Prim,
-) where
-
-import Snats.Peano
-import Snats.Snat.Alias
-import Snats.Snat.Prim
diff --git a/src/Snats/Snat/Alias.hs b/src/Snats/Snat/Alias.hs
@@ -1,34 +0,0 @@
-module Snats.Snat.Alias where
-
-import Snats.Peano
-import Snats.Snat.Prim
-
-pattern Snat0 :: Snat Peano0
-pattern Snat0 = Zero
-
-pattern Snat1 :: Snat Peano1
-pattern Snat1 = Succ Snat0
-
-pattern Snat2 :: Snat Peano2
-pattern Snat2 = Succ Snat1
-
-pattern Snat3 :: Snat Peano3
-pattern Snat3 = Succ Snat2
-
-pattern Snat4 :: Snat Peano4
-pattern Snat4 = Succ Snat3
-
-pattern Snat5 :: Snat Peano5
-pattern Snat5 = Succ Snat4
-
-pattern Snat6 :: Snat Peano6
-pattern Snat6 = Succ Snat5
-
-pattern Snat7 :: Snat Peano7
-pattern Snat7 = Succ Snat6
-
-pattern Snat8 :: Snat Peano8
-pattern Snat8 = Succ Snat7
-
-pattern Snat9 :: Snat Peano9
-pattern Snat9 = Succ Snat8
diff --git a/src/Snats/Snat/Prim.hs b/src/Snats/Snat/Prim.hs
@@ -1,46 +0,0 @@
-module Snats.Snat.Prim (
- Snat,
- pattern Zero,
- pattern Succ,
- snat,
- snatInd,
- snatRec,
- snatFold,
- snatPred,
- snatAdd,
-) where
-
-import Data.Coerce
-import Data.Functor.Const
-
-import Snats.Peano
-import Snats.Snat.Unsafe (Snat, snatAdd, snatPeel, snatSucc, snatZero)
-import Snats.Speano hiding (Succ, Zero)
-
-pattern Zero :: () => (n ~ Z) => Snat n
-pattern Zero <- (snatPeel -> ZeroOp) where Zero = snatZero
-pattern Succ :: () => (n ~ S m) => Snat m -> Snat n
-pattern Succ p <- (snatPeel -> SuccOp p) where Succ = snatSucc
-{-# COMPLETE Zero, Succ #-}
-
--- | The (nonrecursive) eliminator for @Snat@ (equivalent to a case expression
--- with @Zero@ and @Succ@).
-snat :: ((n ~ Z) => a) -> (forall m. (n ~ S m) => Snat m -> a) -> Snat n -> a
-snat z _ Zero = z
-snat _ s (Succ m) = s m
-
--- | Induction for @Snat@.
-snatInd :: f Z -> (forall m. Snat m -> f m -> f (S m)) -> Snat n -> f n
-snatInd z _ Zero = z
-snatInd z s (Succ m) = s m (snatInd z s m)
-
--- | The (nondependent) recursor for @Snat@.
-snatRec :: forall a n. a -> (forall m. Snat m -> a -> a) -> Snat n -> a
-snatRec = coerce $ snatInd @(Const a) @n
-
--- | The catamorphism for @Snat@.
-snatFold :: a -> (a -> a) -> Snat n -> a
-snatFold z s = snatRec z (const s)
-
-snatPred :: Snat (S n) -> Snat n
-snatPred (Succ n) = n
diff --git a/src/Snats/Snat/Unsafe.hs b/src/Snats/Snat/Unsafe.hs
@@ -1,35 +0,0 @@
-module Snats.Snat.Unsafe where
-
-import GHC.Natural
-import Unsafe.Coerce
-
-import Snats.Nat
-import Snats.Natural
-import Snats.Peano
-import Snats.Speano
-
--- | Singleton (@Peano@-indexed) natural numbers represented as a @Nat@.
-newtype Snat (n :: Peano) = SnatUnsafe Nat deriving newtype (Show, Eq)
-
-instance ToNat (Snat n) where
- toNat (SnatUnsafe n) = n
-
-instance ToNatural (Snat a) where
- toNatural = wordToNatural . fromNat . toNat
-
-snatZero :: Snat Z
-snatZero = SnatUnsafe 0
-
-snatSucc :: Snat n -> Snat (S n)
-snatSucc (SnatUnsafe n) = SnatUnsafe (succ n)
-
--- | Peel the outermost unary constructor off a @Snat@, obtaining a result
--- suitable for shallow pattern matching.
---
--- We only use @snatPeel@ to implement pattern synonyms.
-snatPeel :: Snat n -> SpeanoSig Snat n
-snatPeel (SnatUnsafe 0) = unsafeCoerce ZeroOp
-snatPeel (SnatUnsafe n) = unsafeCoerce SuccOp (SnatUnsafe (pred n))
-
-snatAdd :: Snat m -> Snat n -> Snat (Add m n)
-snatAdd (SnatUnsafe m) (SnatUnsafe n) = SnatUnsafe (m + n)
diff --git a/src/Snats/Snatural.hs b/src/Snats/Snatural.hs
@@ -1,9 +0,0 @@
-module Snats.Snatural (
- module Snats.Peano,
- module Snats.Snatural.Alias,
- module Snats.Snatural.Prim,
-) where
-
-import Snats.Peano
-import Snats.Snatural.Alias
-import Snats.Snatural.Prim
diff --git a/src/Snats/Snatural/Alias.hs b/src/Snats/Snatural/Alias.hs
@@ -1,34 +0,0 @@
-module Snats.Snatural.Alias where
-
-import Snats.Peano
-import Snats.Snatural.Prim
-
-pattern Snat0 :: Snatural Peano0
-pattern Snat0 = Zero
-
-pattern Snat1 :: Snatural Peano1
-pattern Snat1 = Succ Snat0
-
-pattern Snat2 :: Snatural Peano2
-pattern Snat2 = Succ Snat1
-
-pattern Snat3 :: Snatural Peano3
-pattern Snat3 = Succ Snat2
-
-pattern Snat4 :: Snatural Peano4
-pattern Snat4 = Succ Snat3
-
-pattern Snat5 :: Snatural Peano5
-pattern Snat5 = Succ Snat4
-
-pattern Snat6 :: Snatural Peano6
-pattern Snat6 = Succ Snat5
-
-pattern Snat7 :: Snatural Peano7
-pattern Snat7 = Succ Snat6
-
-pattern Snat8 :: Snatural Peano8
-pattern Snat8 = Succ Snat7
-
-pattern Snat9 :: Snatural Peano9
-pattern Snat9 = Succ Snat8
diff --git a/src/Snats/Snatural/Prim.hs b/src/Snats/Snatural/Prim.hs
@@ -1,46 +0,0 @@
-module Snats.Snatural.Prim (
- Snatural,
- pattern Zero,
- pattern Succ,
- snatural,
- snaturalInd,
- snaturalRec,
- snaturalFold,
- snaturalPred,
- snaturalAdd,
-) where
-
-import Data.Coerce
-import Data.Functor.Const
-
-import Snats.Peano
-import Snats.Snatural.Unsafe (Snatural, snaturalAdd, snaturalPeel, snaturalSucc, snaturalZero)
-import Snats.Speano hiding (Succ, Zero)
-
-pattern Zero :: () => (n ~ Z) => Snatural n
-pattern Zero <- (snaturalPeel -> ZeroOp) where Zero = snaturalZero
-pattern Succ :: () => (n ~ S m) => Snatural m -> Snatural n
-pattern Succ p <- (snaturalPeel -> SuccOp p) where Succ = snaturalSucc
-{-# COMPLETE Zero, Succ #-}
-
--- | The (nonrecursive) eliminator for @Snatural@ (equivalent to a case
--- expression with @Zero@ and @Succ@).
-snatural :: ((n ~ Z) => a) -> (forall m. (n ~ S m) => Snatural m -> a) -> Snatural n -> a
-snatural z _ Zero = z
-snatural _ s (Succ m) = s m
-
--- | Induction for @Snatural@.
-snaturalInd :: f Z -> (forall m. Snatural m -> f m -> f (S m)) -> Snatural n -> f n
-snaturalInd z _ Zero = z
-snaturalInd z s (Succ m) = s m (snaturalInd z s m)
-
--- | The (nondependent) recursor for @Snatural@.
-snaturalRec :: forall a n. a -> (forall m. Snatural m -> a -> a) -> Snatural n -> a
-snaturalRec = coerce $ snaturalInd @(Const a) @n
-
--- | The catamorphism for @Snatural@.
-snaturalFold :: a -> (a -> a) -> Snatural n -> a
-snaturalFold z s = snaturalRec z (const s)
-
-snaturalPred :: Snatural (S n) -> Snatural n
-snaturalPred (Succ n) = n
diff --git a/src/Snats/Snatural/Unsafe.hs b/src/Snats/Snatural/Unsafe.hs
@@ -1,30 +0,0 @@
-module Snats.Snatural.Unsafe where
-
-import Unsafe.Coerce
-
-import Snats.Natural
-import Snats.Peano
-import Snats.Speano
-
--- | Singleton (@Peano@-indexed) natural numbers represented as a @Natural@.
-newtype Snatural (n :: Peano) = SnaturalUnsafe Natural deriving (Show, Eq)
-
-instance ToNatural (Snatural n) where
- toNatural (SnaturalUnsafe n) = n
-
-snaturalZero :: Snatural Z
-snaturalZero = SnaturalUnsafe 0
-
-snaturalSucc :: Snatural n -> Snatural (S n)
-snaturalSucc (SnaturalUnsafe n) = SnaturalUnsafe (succ n)
-
--- | Peel the outermost unary constructor off a @Snatural@, obtaining a result
--- suitable for shallow pattern matching.
---
--- We only use @snaturalPeel@ to implement pattern synonyms.
-snaturalPeel :: Snatural n -> SpeanoSig Snatural n
-snaturalPeel (SnaturalUnsafe 0) = unsafeCoerce ZeroOp
-snaturalPeel (SnaturalUnsafe n) = unsafeCoerce SuccOp (SnaturalUnsafe (pred n))
-
-snaturalAdd :: Snatural m -> Snatural n -> Snatural (Add m n)
-snaturalAdd (SnaturalUnsafe m) (SnaturalUnsafe n) = SnaturalUnsafe (m + n)
diff --git a/src/Snats/Speano.hs b/src/Snats/Speano.hs
@@ -1,9 +0,0 @@
-module Snats.Speano (
- module Snats.Peano,
- module Snats.Speano.Alias,
- module Snats.Speano.Prim,
-) where
-
-import Snats.Peano
-import Snats.Speano.Alias
-import Snats.Speano.Prim
diff --git a/src/Snats/Speano/Alias.hs b/src/Snats/Speano/Alias.hs
@@ -1,34 +0,0 @@
-module Snats.Speano.Alias where
-
-import Snats.Peano
-import Snats.Speano.Prim
-
-pattern Speano0 :: Speano Peano0
-pattern Speano0 = Zero
-
-pattern Speano1 :: Speano Peano1
-pattern Speano1 = Succ Speano0
-
-pattern Speano2 :: Speano Peano2
-pattern Speano2 = Succ Speano1
-
-pattern Speano3 :: Speano Peano3
-pattern Speano3 = Succ Speano2
-
-pattern Speano4 :: Speano Peano4
-pattern Speano4 = Succ Speano3
-
-pattern Speano5 :: Speano Peano5
-pattern Speano5 = Succ Speano4
-
-pattern Speano6 :: Speano Peano6
-pattern Speano6 = Succ Speano5
-
-pattern Speano7 :: Speano Peano7
-pattern Speano7 = Succ Speano6
-
-pattern Speano8 :: Speano Peano8
-pattern Speano8 = Succ Speano7
-
-pattern Speano9 :: Speano Peano9
-pattern Speano9 = Succ Speano8
diff --git a/src/Snats/Speano/Prim.hs b/src/Snats/Speano/Prim.hs
@@ -1,71 +0,0 @@
-module Snats.Speano.Prim (
- SpeanoSig (..),
- Speano (..),
- speanoShow,
- speano,
- speanoInd,
- speanoRec,
- speanoFold,
- speanoPred,
- speanoAdd,
-) where
-
-import Data.Coerce
-import Data.Functor.Const
-
-import Snats.Natural
-import Snats.Peano
-
--- | The "signature" of singleton (@Peano@-indexed) natural numbers:
--- @SpeanoSig@ is to @Speano@ as @Maybe@ is to @Peano@.
-data SpeanoSig f n where
- ZeroOp :: SpeanoSig f Z
- SuccOp :: f n -> SpeanoSig f (S n)
-
--- | Singleton (@Peano@-indexed) unary natural numbers.
---
--- @Speano@ is implemented as a GADT, and hence is inefficient.
--- See @Snat@ and @Snatural@ for efficient alternatives.
-data Speano n where
- Zero :: Speano Z
- Succ :: Speano n -> Speano (S n)
-
-deriving instance Eq (Speano n)
-
-instance Show (Speano n) where
- show = show . toNatural
-
--- | A variant of @show \@(Speano n)@ that uses unary notation instead of decimal.
-speanoShow :: Speano n -> String
-speanoShow Zero = "Z"
-speanoShow (Succ n) = 'S' : speanoShow n
-
-instance ToNatural (Speano n) where
- toNatural Zero = 0
- toNatural (Succ n) = succ (toNatural n)
-
--- | The (nonrecursive) eliminator for @Speano@ (equivalent to a case
--- expression).
-speano :: ((n ~ Z) => a) -> (forall m. (n ~ S m) => Speano m -> a) -> Speano n -> a
-speano z _ Zero = z
-speano _ s (Succ m) = s m
-
--- | Induction for @Speano@.
-speanoInd :: f Z -> (forall m. Speano m -> f m -> f (S m)) -> Speano n -> f n
-speanoInd z _ Zero = z
-speanoInd z s (Succ m) = s m (speanoInd z s m)
-
--- | The (nondependent) recursor for @Speano@.
-speanoRec :: forall a n. a -> (forall m. Speano m -> a -> a) -> Speano n -> a
-speanoRec = coerce $ speanoInd @(Const a) @n
-
--- | The catamorphism for @Speano@.
-speanoFold :: a -> (a -> a) -> Speano n -> a
-speanoFold z s = speanoRec z (const s)
-
-speanoPred :: Speano (S n) -> Speano n
-speanoPred (Succ n) = n
-
-speanoAdd :: Speano m -> Speano n -> Speano (Add m n)
-speanoAdd Zero n = n
-speanoAdd (Succ m) n = Succ (speanoAdd m n)
