commit 352e84123d2868a1d303fb75377a1e84dce3c07e
parent 7c1f92264abf397e76b0339df247b53c20f7ed34
Author: Robert Russell <robert@rr3.xyz>
Date: Fri, 4 Jul 2025 17:03:47 -0700
Add IsSpeano type class for Speano, Snat, and Snatural
Diffstat:
14 files changed, 195 insertions(+), 347 deletions(-)
diff --git a/TODO b/TODO
@@ -1,2 +0,0 @@
-"Prim" does not contain primitives in the case of Snat and Snatural.
-Rename these files to something more appropriate.
diff --git a/src/Naturals.hs b/src/Naturals.hs
@@ -0,0 +1,11 @@
+module Naturals (
+ module X,
+) where
+
+import Naturals.IsSpeano as X
+import Naturals.Nat as X
+import Naturals.Natural as X
+import Naturals.Peano as X
+import Naturals.Snat as X
+import Naturals.Snatural as X
+import Naturals.Speano as X hiding (Succ, Zero)
diff --git a/src/Naturals/IsSpeano.hs b/src/Naturals/IsSpeano.hs
@@ -0,0 +1,112 @@
+module Naturals.IsSpeano (
+ SpeanoSig (..),
+ IsSpeano (..),
+ pattern Zero,
+ pattern Succ,
+ pattern Speano0,
+ pattern Speano1,
+ pattern Speano2,
+ pattern Speano3,
+ pattern Speano4,
+ pattern Speano5,
+ pattern Speano6,
+ pattern Speano7,
+ pattern Speano8,
+ pattern Speano9,
+ speano,
+ speanoInd,
+ speanoRec,
+ speanoFold,
+ speanoPred,
+) where
+
+import Data.Coerce
+import Data.Functor.Const
+
+import Naturals.Peano
+
+-- | The signature of singleton (@Peano@-indexed) natural numbers.
+data SpeanoSig f n where
+ ZeroOp :: SpeanoSig f Z
+ SuccOp :: f n -> SpeanoSig f (S n)
+
+-- | Types that behave like singleton (@Peano@-indexed) natural numbers.
+--
+-- Laws:
+-- - @speanoPeel speanoZero = ZeroOp@
+-- - @speanoPeel (speanoSucc n) = SuccOp n@
+class IsSpeano f where
+ {-# MINIMAL speanoZero, speanoSucc, speanoPeel #-}
+
+ speanoZero :: f Z
+ speanoSucc :: f n -> f (S n)
+
+ -- | Peel off the outermost operation (@ZeroOp@ or @SuccOp@) from the
+ -- argument, obtaining a result suitable for shallow pattern matching.
+ speanoPeel :: f n -> SpeanoSig f n
+
+ speanoAdd :: (IsSpeano f) => f m -> f n -> f (Add m n)
+ speanoAdd Zero n = n
+ speanoAdd (Succ m) n = Succ (speanoAdd m n)
+
+pattern Zero :: (IsSpeano f) => (n ~ Z) => f n
+pattern Zero <- (speanoPeel -> ZeroOp) where Zero = speanoZero
+pattern Succ :: (IsSpeano f) => (n ~ S m) => f m -> f n
+pattern Succ p <- (speanoPeel -> SuccOp p) where Succ = speanoSucc
+{-# COMPLETE Zero, Succ #-}
+
+pattern Speano0 :: (IsSpeano f) => f Peano0
+pattern Speano0 = Zero
+
+pattern Speano1 :: (IsSpeano f) => f Peano1
+pattern Speano1 = Succ Speano0
+
+pattern Speano2 :: (IsSpeano f) => f Peano2
+pattern Speano2 = Succ Speano1
+
+pattern Speano3 :: (IsSpeano f) => f Peano3
+pattern Speano3 = Succ Speano2
+
+pattern Speano4 :: (IsSpeano f) => f Peano4
+pattern Speano4 = Succ Speano3
+
+pattern Speano5 :: (IsSpeano f) => f Peano5
+pattern Speano5 = Succ Speano4
+
+pattern Speano6 :: (IsSpeano f) => f Peano6
+pattern Speano6 = Succ Speano5
+
+pattern Speano7 :: (IsSpeano f) => f Peano7
+pattern Speano7 = Succ Speano6
+
+pattern Speano8 :: (IsSpeano f) => f Peano8
+pattern Speano8 = Succ Speano7
+
+pattern Speano9 :: (IsSpeano f) => f Peano9
+pattern Speano9 = Succ Speano8
+
+-- | Show with unary notation.
+speanoShow :: (IsSpeano f) => f n -> String
+speanoShow Zero = "Z"
+speanoShow (Succ n) = 'S' : speanoShow n
+
+-- | The (nonrecursive) eliminator for types implementing @IsSpeano@.
+speano :: (IsSpeano f) => ((n ~ Z) => a) -> (forall m. (n ~ S m) => f m -> a) -> f n -> a
+speano z _ Zero = z
+speano _ s (Succ m) = s m
+
+-- | Induction for types implementing @IsSpeano@.
+speanoInd :: forall f n p. (IsSpeano f) => p Z -> (forall m. f m -> p m -> p (S m)) -> f n -> p n
+speanoInd z _ Zero = z
+speanoInd z s (Succ m) = s m (speanoInd z s m)
+
+-- | The (nondependent) recursor for types implementing @IsSpeano@.
+speanoRec :: forall f n a. (IsSpeano f) => a -> (forall m. f m -> a -> a) -> f n -> a
+speanoRec = coerce $ speanoInd @f @n @(Const a)
+
+-- | The catamorphism for types implementing @IsSpeano@.
+speanoFold :: (IsSpeano f) => a -> (a -> a) -> f n -> a
+speanoFold z s = speanoRec z (const s)
+
+speanoPred :: (IsSpeano f) => f (S n) -> f n
+speanoPred (Succ m) = m
diff --git a/src/Naturals/Snat.hs b/src/Naturals/Snat.hs
@@ -1,9 +1,29 @@
module Naturals.Snat (
- module Naturals.Peano,
- module Naturals.Snat.Alias,
- module Naturals.Snat.Prim,
+ Snat (..),
) where
+import GHC.Natural
+import Unsafe.Coerce
+
+import Naturals.IsSpeano
+import Naturals.Nat
+import Naturals.Natural
import Naturals.Peano
-import Naturals.Snat.Alias
-import Naturals.Snat.Prim
+
+-- | Singleton (@Peano@-indexed) natural numbers represented as a @Nat@.
+newtype Snat (n :: Peano) = SnatUnsafe Nat deriving newtype (Show)
+
+instance Eq (Snat n) where
+ _ == _ = True
+
+instance ToNat (Snat n) where
+ toNat (SnatUnsafe n) = n
+
+instance ToNatural (Snat a) where
+ toNatural = wordToNatural . fromNat . toNat
+
+instance IsSpeano Snat where
+ speanoZero = SnatUnsafe 0
+ speanoSucc = SnatUnsafe . succ . toNat
+ speanoPeel (SnatUnsafe 0) = unsafeCoerce ZeroOp
+ speanoPeel (SnatUnsafe n) = unsafeCoerce SuccOp . SnatUnsafe . pred $ n
diff --git a/src/Naturals/Snat/Alias.hs b/src/Naturals/Snat/Alias.hs
@@ -1,34 +0,0 @@
-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
@@ -1,46 +0,0 @@
-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
@@ -1,35 +0,0 @@
-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
@@ -1,9 +1,24 @@
module Naturals.Snatural (
- module Naturals.Peano,
- module Naturals.Snatural.Alias,
- module Naturals.Snatural.Prim,
+ Snatural (..),
) where
+import Unsafe.Coerce
+
+import Naturals.IsSpeano
+import Naturals.Natural
import Naturals.Peano
-import Naturals.Snatural.Alias
-import Naturals.Snatural.Prim
+
+-- | Singleton (@Peano@-indexed) natural numbers represented as a @Natural@.
+newtype Snatural (n :: Peano) = SnaturalUnsafe Natural deriving newtype (Show)
+
+instance Eq (Snatural n) where
+ _ == _ = True
+
+instance ToNatural (Snatural n) where
+ toNatural (SnaturalUnsafe n) = n
+
+instance IsSpeano Snatural where
+ speanoZero = SnaturalUnsafe 0
+ speanoSucc = SnaturalUnsafe . succ . toNatural
+ speanoPeel (SnaturalUnsafe 0) = unsafeCoerce ZeroOp
+ speanoPeel (SnaturalUnsafe n) = unsafeCoerce SuccOp . SnaturalUnsafe . pred $ n
diff --git a/src/Naturals/Snatural/Alias.hs b/src/Naturals/Snatural/Alias.hs
@@ -1,34 +0,0 @@
-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
@@ -1,46 +0,0 @@
-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
@@ -1,30 +0,0 @@
-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
@@ -1,9 +1,31 @@
module Naturals.Speano (
- module Naturals.Peano,
- module Naturals.Speano.Alias,
- module Naturals.Speano.Prim,
+ Speano (..),
) where
+import Naturals.IsSpeano hiding (Succ, Zero)
+import Naturals.Natural
import Naturals.Peano
-import Naturals.Speano.Alias
-import Naturals.Speano.Prim
+
+-- | Singleton (@Peano@-indexed) unary natural numbers.
+--
+-- @Speano@ is implemented as a "correct-by-construction" GADT, making it
+-- inefficient. See @Snat@ and @Snatural@ for efficient alternatives.
+data Speano n where
+ Zero :: Speano Z
+ Succ :: Speano n -> Speano (S n)
+
+instance Eq (Speano n) where
+ _ == _ = True
+
+instance Show (Speano n) where
+ show = show . toNatural
+
+instance ToNatural (Speano n) where
+ toNatural Zero = 0
+ toNatural (Succ n) = Prelude.succ (toNatural n)
+
+instance IsSpeano Speano where
+ speanoZero = Zero
+ speanoSucc = Succ
+ speanoPeel Zero = ZeroOp
+ speanoPeel (Succ m) = SuccOp m
diff --git a/src/Naturals/Speano/Alias.hs b/src/Naturals/Speano/Alias.hs
@@ -1,34 +0,0 @@
-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
@@ -1,71 +0,0 @@
-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)
