commit 52cf94bf434c0fdb662380ab05a8c66463d76713
parent 352e84123d2868a1d303fb75377a1e84dce3c07e
Author: Robert Russell <robert@rr3.xyz>
Date: Fri, 4 Jul 2025 22:39:48 -0700
Add stuff for working with finite prefixes of the natural numbers
Diffstat:
9 files changed, 243 insertions(+), 3 deletions(-)
diff --git a/src/Naturals.hs b/src/Naturals.hs
@@ -2,6 +2,10 @@ module Naturals (
module X,
) where
+import Naturals.Fin as X hiding (FSucc, FZero)
+import Naturals.Finat as X
+import Naturals.Finatural as X
+import Naturals.IsFin as X
import Naturals.IsSpeano as X
import Naturals.Nat as X
import Naturals.Natural as X
diff --git a/src/Naturals/Fin.hs b/src/Naturals/Fin.hs
@@ -0,0 +1,32 @@
+module Naturals.Fin (
+ Fin (..),
+) where
+
+import Naturals.IsFin hiding (FSucc, FZero)
+import Naturals.Natural
+import Naturals.Peano
+
+-- | Finite (@Peano@-indexed) prefixes of the unary natural numbers.
+--
+-- @Fin@ is implemented as a "correct-by-construction" GADT, making it
+-- inefficient. See @Finat@ and @Finatural@ for efficient alternatives.
+data Fin n where
+ FZero :: Fin (S n)
+ FSucc :: Fin n -> Fin (S n)
+
+deriving instance Eq (Fin n)
+
+instance Show (Fin n) where
+ show = show . toNatural
+
+instance ToNatural (Fin n) where
+ toNatural FZero = 0
+ toNatural (FSucc n) = succ (toNatural n)
+
+instance IsFin Fin where
+ finZero = FZero
+
+ finSucc = FSucc
+
+ finPeel FZero = FZeroOp
+ finPeel (FSucc m) = FSuccOp m
diff --git a/src/Naturals/Finat.hs b/src/Naturals/Finat.hs
@@ -0,0 +1,32 @@
+module Naturals.Finat (
+ Finat (..),
+) where
+
+import GHC.Natural
+import Unsafe.Coerce
+
+import Naturals.IsFin
+import Naturals.Nat
+import Naturals.Natural
+import Naturals.Peano
+
+-- | Finite (@Peano@-indexed) prefixes of @Nat@.
+newtype Finat (n :: Peano) = FinatUnsafe Nat deriving newtype (Show, Eq)
+
+instance ToNat (Finat n) where
+ toNat (FinatUnsafe n) = n
+
+instance ToNatural (Finat n) where
+ toNatural = wordToNatural . fromNat . toNat
+
+instance IsFin Finat where
+ finZero = FinatUnsafe 0
+
+ finSucc = FinatUnsafe . succ . toNat
+
+ finPeel (FinatUnsafe 0) = unsafeCoerce FZeroOp
+ finPeel (FinatUnsafe n) = unsafeCoerce FSuccOp . FinatUnsafe . pred $ n
+
+ finWeaken (FinatUnsafe n) = FinatUnsafe n
+
+-- TODO: Special functions (e.g., mirror) for working with Snats and Finats together.
diff --git a/src/Naturals/Finatural.hs b/src/Naturals/Finatural.hs
@@ -0,0 +1,28 @@
+module Naturals.Finatural (
+ Finatural (..),
+) where
+
+import GHC.Natural
+import Unsafe.Coerce
+
+import Naturals.IsFin
+import Naturals.Natural
+import Naturals.Peano
+
+-- | Finite (@Peano@-indexed) prefixes of @Natural@.
+newtype Finatural (n :: Peano) = FinaturalUnsafe Natural deriving newtype (Show, Eq)
+
+instance ToNatural (Finatural n) where
+ toNatural (FinaturalUnsafe n) = n
+
+instance IsFin Finatural where
+ finZero = FinaturalUnsafe 0
+
+ finSucc = FinaturalUnsafe . succ . toNatural
+
+ finPeel (FinaturalUnsafe 0) = unsafeCoerce FZeroOp
+ finPeel (FinaturalUnsafe n) = unsafeCoerce FSuccOp . FinaturalUnsafe . pred $ n
+
+ finWeaken (FinaturalUnsafe n) = FinaturalUnsafe n
+
+-- TODO: Special functions (e.g., mirror) for working with Snaturals and Finaturals together.
diff --git a/src/Naturals/IsFin.hs b/src/Naturals/IsFin.hs
@@ -0,0 +1,130 @@
+module Naturals.IsFin (
+ FinSig (..),
+ IsFin (..),
+ pattern FZero,
+ pattern FSucc,
+ pattern Fin0,
+ pattern Fin1,
+ pattern Fin2,
+ pattern Fin3,
+ pattern Fin4,
+ pattern Fin5,
+ pattern Fin6,
+ pattern Fin7,
+ pattern Fin8,
+ pattern Fin9,
+ finFromSpeano,
+ finShow,
+ fin,
+ finAbsurd,
+ finRec,
+ finFold,
+ finMirror,
+) where
+
+import Naturals.IsSpeano
+import Naturals.Natural
+import Naturals.Peano
+
+-- | The "signature" of finite (@Peano@-indexed) prefixes of the natural
+-- numbers.
+data FinSig f n where
+ FZeroOp :: FinSig f (S n)
+ FSuccOp :: f n -> FinSig f (S n)
+
+-- | Types that behave like finite (@Peano@-indexed) prefixes of the natural
+-- numbers.
+--
+-- Laws:
+-- - @finPeel finZero = FZeroOp@
+-- - @finPeel (finSucc n) = FSuccOp n@
+-- - @toNatural finZero = 0@
+-- - @toNatural (finSucc n) = succ (toNatural n)@
+class (forall n. ToNatural (f n)) => IsFin f where
+ {-# MINIMAL finZero, finSucc, finPeel #-}
+
+ finZero :: f (S n)
+ finSucc :: f n -> f (S n)
+
+ -- | Peel off the outermost operation (@FZeroOp@ or @FSuccOp@) from the
+ -- argument, obtaining a result suitable for shallow pattern matching.
+ finPeel :: f n -> FinSig f n
+
+ finWeaken :: (IsFin f) => f n -> f (S n)
+ finWeaken FZero = FZero
+ finWeaken (FSucc n) = FSucc (finWeaken n)
+
+pattern FZero :: (IsFin f) => (n ~ S m) => f n
+pattern FZero <- (finPeel -> FZeroOp) where FZero = finZero
+pattern FSucc :: (IsFin f) => (n ~ S m) => f m -> f n
+pattern FSucc p <- (finPeel -> FSuccOp p) where FSucc = finSucc
+{-# COMPLETE FZero, FSucc #-}
+
+pattern Fin0 :: (IsFin f) => f (Add Peano0 (S n))
+pattern Fin0 = FZero
+
+pattern Fin1 :: (IsFin f) => f (Add Peano1 (S n))
+pattern Fin1 = FSucc Fin0
+
+pattern Fin2 :: (IsFin f) => f (Add Peano2 (S n))
+pattern Fin2 = FSucc Fin1
+
+pattern Fin3 :: (IsFin f) => f (Add Peano3 (S n))
+pattern Fin3 = FSucc Fin2
+
+pattern Fin4 :: (IsFin f) => f (Add Peano4 (S n))
+pattern Fin4 = FSucc Fin3
+
+pattern Fin5 :: (IsFin f) => f (Add Peano5 (S n))
+pattern Fin5 = FSucc Fin4
+
+pattern Fin6 :: (IsFin f) => f (Add Peano6 (S n))
+pattern Fin6 = FSucc Fin5
+
+pattern Fin7 :: (IsFin f) => f (Add Peano7 (S n))
+pattern Fin7 = FSucc Fin6
+
+pattern Fin8 :: (IsFin f) => f (Add Peano8 (S n))
+pattern Fin8 = FSucc Fin7
+
+pattern Fin9 :: (IsFin f) => f (Add Peano9 (S n))
+pattern Fin9 = FSucc Fin8
+
+finFromSpeano :: (IsSpeano s, IsFin f) => s n -> f (S n)
+finFromSpeano Zero = FZero
+finFromSpeano (Succ n) = FSucc (finFromSpeano n)
+
+-- | Show with unary notation.
+finShow :: (IsFin f) => f n -> String
+finShow FZero = "Z"
+finShow (FSucc n) = 'S' : finShow n
+
+-- | The (nonrecursive) eliminator for types implementing @IsFin@.
+fin :: (IsFin f) => (forall m. (n ~ S m) => a) -> (forall m. (n ~ S m) => f m -> a) -> f n -> a
+fin z _ FZero = z
+fin _ s (FSucc m) = s m
+
+finAbsurd :: (IsFin f) => f Z -> a
+finAbsurd = \case {}
+
+-- | The recursor for types implementing @IsFin@.
+finRec :: (IsFin f) => a -> (forall m. f m -> a -> a) -> f n -> a
+finRec z _ FZero = z
+finRec z s (FSucc m) = s m (finRec z s m)
+
+-- | The "catamorphism" for types implementing @IsFin@.
+finFold :: (IsFin f) => a -> (a -> a) -> f n -> a
+finFold z s = finRec z (const s)
+
+newtype FinMirror f n = FinMirror {unFinMirror :: f n -> f n}
+
+-- | Informally, @finMirror n i = n - i - 1@.
+finMirror :: forall s f n. (IsSpeano s, IsFin f) => s n -> f n -> f n
+finMirror =
+ let z :: FinMirror f Z
+ z = FinMirror finAbsurd
+ s :: s m -> FinMirror f m -> FinMirror f (S m)
+ s m (FinMirror f) = FinMirror \case
+ FZero -> finFromSpeano m
+ FSucc i -> finWeaken (f i)
+ in unFinMirror . speanoInd z s
diff --git a/src/Naturals/IsSpeano.hs b/src/Naturals/IsSpeano.hs
@@ -13,6 +13,7 @@ module Naturals.IsSpeano (
pattern Speano7,
pattern Speano8,
pattern Speano9,
+ speanoShow,
speano,
speanoInd,
speanoRec,
@@ -23,6 +24,7 @@ module Naturals.IsSpeano (
import Data.Coerce
import Data.Functor.Const
+import Naturals.Natural
import Naturals.Peano
-- | The signature of singleton (@Peano@-indexed) natural numbers.
@@ -35,7 +37,9 @@ data SpeanoSig f n where
-- Laws:
-- - @speanoPeel speanoZero = ZeroOp@
-- - @speanoPeel (speanoSucc n) = SuccOp n@
-class IsSpeano f where
+-- - @toNatural speanoZero = 0@
+-- - @toNatural (speanoSucc n) = succ (toNatural n)@
+class (forall n. ToNatural (f n)) => IsSpeano f where
{-# MINIMAL speanoZero, speanoSucc, speanoPeel #-}
speanoZero :: f Z
diff --git a/src/Naturals/Snat.hs b/src/Naturals/Snat.hs
@@ -19,11 +19,15 @@ instance Eq (Snat n) where
instance ToNat (Snat n) where
toNat (SnatUnsafe n) = n
-instance ToNatural (Snat a) where
+instance ToNatural (Snat n) 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
+
+ speanoAdd (SnatUnsafe m) (SnatUnsafe n) = SnatUnsafe (m + n)
diff --git a/src/Naturals/Snatural.hs b/src/Naturals/Snatural.hs
@@ -19,6 +19,10 @@ instance ToNatural (Snatural n) where
instance IsSpeano Snatural where
speanoZero = SnaturalUnsafe 0
+
speanoSucc = SnaturalUnsafe . succ . toNatural
+
speanoPeel (SnaturalUnsafe 0) = unsafeCoerce ZeroOp
speanoPeel (SnaturalUnsafe n) = unsafeCoerce SuccOp . SnaturalUnsafe . pred $ n
+
+ speanoAdd (SnaturalUnsafe m) (SnaturalUnsafe n) = SnaturalUnsafe (m + n)
diff --git a/src/Naturals/Speano.hs b/src/Naturals/Speano.hs
@@ -22,10 +22,12 @@ instance Show (Speano n) where
instance ToNatural (Speano n) where
toNatural Zero = 0
- toNatural (Succ n) = Prelude.succ (toNatural n)
+ toNatural (Succ n) = succ (toNatural n)
instance IsSpeano Speano where
speanoZero = Zero
+
speanoSucc = Succ
+
speanoPeel Zero = ZeroOp
speanoPeel (Succ m) = SuccOp m
