commit 0896fd2d14acf5c75597c778b2685941313c2112
parent 3da4f50ce0b62a10d2c8c6d0216350639b45d1ec
Author: Robert Russell <robert@rr3.xyz>
Date: Sun, 29 Jun 2025 17:27:57 -0700
Rename, clean up, extend, and improve
Diffstat:
17 files changed, 535 insertions(+), 121 deletions(-)
diff --git a/TODO b/TODO
@@ -0,0 +1,2 @@
+"Prim" does not contain primitives in the case of Snat and Snatural.
+Rename these files to something more appropriate.
diff --git a/src/Snats/Nat.hs b/src/Snats/Nat.hs
@@ -1,48 +1,34 @@
module Snats.Nat (
- Nat (..),
- CaseDecision (..),
- Pred,
- Add,
+ Nat,
+ ToNat (..),
+ FromNat (..),
) where
-import Control.Exception
+-- | Word-sized natural numbers.
+newtype Nat = Nat Word deriving newtype (Show, Eq, Ord, Enum, Bounded, Num, Real, Integral)
--- | Unary natural numbers. Intended mainly for use at the type-level.
-data Nat = Z | S Nat deriving (Show, Eq)
+-- | Types supporting conversion to @Nat@.
+--
+-- If @a@ also implements @FromNat@, then @toNat@ and @fromNat@ should be
+-- inverses.
+class ToNat a where
+ toNat :: a -> Nat
-instance Ord Nat where
- Z `compare` Z = EQ
- S _ `compare` Z = GT
- Z `compare` S _ = LT
- S m `compare` S n = m `compare` n
+-- | 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 Num Nat where
- Z + n = n
- S m + n = S (m + n)
+instance ToNat Nat where
+ toNat = id
- n - Z = n
- _ - S _ = throw Underflow
+instance FromNat Nat where
+ fromNat = id
- Z * _ = Z
- S m * n = m * n + n
+instance ToNat Word where
+ toNat = Nat
- abs n = n
-
- signum Z = Z
- signum (S _) = S Z
-
- fromInteger 0 = Z
- fromInteger n
- | n > 0 = S (fromInteger (n - 1))
- | otherwise = throw Underflow
-
-data CaseDecision f n where
- IsZ :: CaseDecision f Z
- IsS :: f n -> CaseDecision f (S n)
-
-type family Pred (n :: Nat) :: Nat where
- Pred (S n) = n
-
-type family Add (x :: Nat) (y :: Nat) :: Nat where
- Add Z n = n
- Add (S m) n = S (Add m n)
+instance FromNat Word where
+ fromNat (Nat n) = n
diff --git a/src/Snats/Natural.hs b/src/Snats/Natural.hs
@@ -0,0 +1,27 @@
+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
@@ -0,0 +1,7 @@
+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
@@ -0,0 +1,47 @@
+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
@@ -0,0 +1,76 @@
+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,45 +1,9 @@
module Snats.Snat (
- module Snats.Nat,
- Snat, -- Don't export the constructor!
- pattern Zero,
- pattern Succ,
- toWord,
- decideCase,
- snat,
- pred,
- add,
+ module Snats.Peano,
+ module Snats.Snat.Alias,
+ module Snats.Snat.Prim,
) where
-import Unsafe.Coerce
-import Prelude hiding (pred, succ)
-
-import Snats.Nat
-
--- | Singleton natural numbers represented as a @Word@.
-newtype Snat (n :: Nat) = SnatUnsafe Word deriving (Show, Eq)
-
-pattern Zero :: () => (n ~ Z) => Snat n
-pattern Zero <- (decideCase -> IsZ) where Zero = SnatUnsafe 0
-pattern Succ :: () => (n ~ S m) => Snat m -> Snat n
-pattern Succ p <- (decideCase -> IsS p) where Succ (SnatUnsafe n) = SnatUnsafe (n + 1)
-{-# COMPLETE Zero, Succ #-}
-
-toWord :: Snat n -> Word
-toWord (SnatUnsafe n) = n
-
-decideCase :: Snat n -> CaseDecision Snat n
-decideCase (SnatUnsafe 0) = unsafeCoerce IsZ
-decideCase (SnatUnsafe n) = unsafeCoerce IsS (SnatUnsafe (n - 1))
-
-snat :: ((n ~ Z) => a) -> (forall m. (n ~ S m) => Snat m -> a) -> Snat n -> a
-snat z _ Zero = z
-snat _ s (Succ n) = s n
-
-pred :: Snat (S n) -> Snat n
-pred (Succ n) = n
-
-add :: Snat m -> Snat n -> Snat (Add m n)
-add (SnatUnsafe m) (SnatUnsafe n) = SnatUnsafe (m + n)
-
--- maybePred :: Snat n -> Maybe (Snat (Pred n))
--- maybePred = snat Nothing Just
+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
@@ -0,0 +1,34 @@
+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
@@ -0,0 +1,46 @@
+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
@@ -0,0 +1,35 @@
+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,43 +1,9 @@
module Snats.Snatural (
- module Snats.Nat,
- Snatural, -- Don't export the constructor!
- pattern Zero,
- pattern Succ,
- toNatural,
- decideCase,
- snatural,
- pred,
- add,
+ module Snats.Peano,
+ module Snats.Snatural.Alias,
+ module Snats.Snatural.Prim,
) where
-import Numeric.Natural
-import Unsafe.Coerce
-import Prelude hiding (pred, succ)
-
-import Snats.Nat
-
--- | Singleton natural numbers represented as a @Natural@.
-newtype Snatural (n :: Nat) = SnaturalUnsafe Natural deriving (Show, Eq)
-
-pattern Zero :: () => (n ~ Z) => Snatural n
-pattern Zero <- (decideCase -> IsZ) where Zero = SnaturalUnsafe 0
-pattern Succ :: () => (n ~ S m) => Snatural m -> Snatural n
-pattern Succ p <- (decideCase -> IsS p) where Succ (SnaturalUnsafe n) = SnaturalUnsafe (n + 1)
-{-# COMPLETE Zero, Succ #-}
-
-toNatural :: Snatural n -> Natural
-toNatural (SnaturalUnsafe n) = n
-
-decideCase :: Snatural n -> CaseDecision Snatural n
-decideCase (SnaturalUnsafe 0) = unsafeCoerce IsZ
-decideCase (SnaturalUnsafe n) = unsafeCoerce IsS (SnaturalUnsafe (n - 1))
-
-snatural :: ((n ~ Z) => a) -> (forall m. (n ~ S m) => Snatural m -> a) -> Snatural n -> a
-snatural z _ Zero = z
-snatural _ s (Succ n) = s n
-
-pred :: Snatural (S n) -> Snatural n
-pred (Succ n) = n
-
-add :: Snatural m -> Snatural n -> Snatural (Add m n)
-add (SnaturalUnsafe m) (SnaturalUnsafe n) = SnaturalUnsafe (m + n)
+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
@@ -0,0 +1,34 @@
+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
@@ -0,0 +1,46 @@
+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
@@ -0,0 +1,30 @@
+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
@@ -0,0 +1,9 @@
+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
@@ -0,0 +1,34 @@
+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
@@ -0,0 +1,71 @@
+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)
