naturals

commit d749985de2efd24f0d2e892e4a51a8575078aa53
parent 197dab3b229815a74a8098b672a1d2eb1a491806
Author: Robert Russell <robert@rr3.xyz>
Date:   Sat,  5 Jul 2025 16:36:39 -0700

Add FinatSeq, Peano-indexed Seqs indexable with Finats

Diffstat:
A
TODO
 | 
1
+
M
package.yaml
 | 
1
+
M
src/Naturals.hs
 | 
1
+
A
src/Naturals/FinatSeq.hs
 | 
5
+++++
A
src/Naturals/FinatSeq/Unsafe.hs
 | 
98
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

5 files changed, 106 insertions(+), 0 deletions(-)
diff --git a/TODO b/TODO
@@ -0,0 +1 @@
+FinaturalSeq, or somehow generalize FinatSeq to support other IsFin types
diff --git a/package.yaml b/package.yaml
@@ -32,6 +32,7 @@ default-extensions:
 
 dependencies:
     - base
+    - containers
 
 library:
     source-dirs: src
diff --git a/src/Naturals.hs b/src/Naturals.hs
@@ -4,6 +4,7 @@ module Naturals (
 
 import Naturals.Fin as X hiding (FSucc, FZero)
 import Naturals.Finat as X
+import Naturals.FinatSeq as X
 import Naturals.Finatural as X
 import Naturals.IsFin as X
 import Naturals.IsSpeano as X
diff --git a/src/Naturals/FinatSeq.hs b/src/Naturals/FinatSeq.hs
@@ -0,0 +1,5 @@
+module Naturals.FinatSeq (
+    module Naturals.FinatSeq.Unsafe,
+) where
+
+import Naturals.FinatSeq.Unsafe hiding (FinatSeqUnsafe)
diff --git a/src/Naturals/FinatSeq/Unsafe.hs b/src/Naturals/FinatSeq/Unsafe.hs
@@ -0,0 +1,98 @@
+module Naturals.FinatSeq.Unsafe (
+    FinatSeq (..),
+    pattern Empty,
+    pattern (:<),
+    pattern (:>),
+    showsPrecl,
+    showl,
+    showsPrecr,
+    showr,
+    singleton,
+    length,
+    lookup,
+    adjust,
+    replace,
+) where
+
+import Data.Coerce
+import Data.Sequence (Seq)
+import Data.Sequence qualified as Seq
+import Unsafe.Coerce
+import Prelude hiding (length, lookup)
+
+import Naturals.Finat.Unsafe
+import Naturals.Peano
+import Naturals.Snat.Unsafe
+
+newtype FinatSeq (n :: Peano) a = FinatSeqUnsafe (Seq a)
+    deriving (Eq, Functor, Foldable, Traversable)
+
+--------------------------------------------------------------------------------
+-- Patterns
+
+data ViewL n a where
+    EmptyL :: ViewL Z a
+    ConsL :: a -> FinatSeq n a -> ViewL (S n) a
+
+viewl :: FinatSeq n a -> ViewL n a
+viewl (FinatSeqUnsafe Seq.Empty) = unsafeCoerce EmptyL
+viewl (FinatSeqUnsafe (x Seq.:<| xs)) = unsafeCoerce ConsL x (FinatSeqUnsafe xs)
+
+data ViewR n a where
+    EmptyR :: ViewR Z a
+    ConsR :: FinatSeq n a -> a -> ViewR (S n) a
+
+viewr :: FinatSeq n a -> ViewR n a
+viewr (FinatSeqUnsafe Seq.Empty) = unsafeCoerce EmptyR
+viewr (FinatSeqUnsafe (xs Seq.:|> x)) = unsafeCoerce ConsR (FinatSeqUnsafe xs) x
+
+pattern Empty :: () => (n ~ Z) => FinatSeq n a
+pattern Empty <- (viewl -> EmptyL) where Empty = FinatSeqUnsafe Seq.Empty
+
+infixr 5 :< -- Keep in sync with showsPrecl.
+pattern (:<) :: () => (n ~ S m) => a -> FinatSeq m a -> FinatSeq n a
+pattern x :< xs <- (viewl -> ConsL x xs) where x :< FinatSeqUnsafe xs = FinatSeqUnsafe (x Seq.:<| xs)
+{-# COMPLETE Empty, (:<) #-}
+
+infixl 5 :> -- Keep in sync with showsPrecr.
+pattern (:>) :: () => (n ~ S m) => FinatSeq m a -> a -> FinatSeq n a
+pattern xs :> x <- (viewr -> ConsR xs x) where FinatSeqUnsafe xs :> x = FinatSeqUnsafe (xs Seq.:|> x)
+{-# COMPLETE Empty, (:>) #-}
+
+--------------------------------------------------------------------------------
+-- Show
+
+showsPrecl :: (Show a) => Int -> FinatSeq n a -> ShowS
+showsPrecl _ Empty = showString "Empty"
+showsPrecl p (x :< xs) = showParen (p > 5) $ showsPrec 6 x . showString " :< " . showsPrecl 5 xs
+
+showl :: (Show a) => FinatSeq n a -> String
+showl xs = showsPrecl 0 xs ""
+
+showsPrecr :: (Show a) => Int -> FinatSeq n a -> ShowS
+showsPrecr _ Empty = showString "Empty"
+showsPrecr p (xs :> x) = showParen (p > 5) $ showsPrecr 5 xs . showString " :> " . showsPrec 6 x
+
+showr :: (Show a) => FinatSeq n a -> String
+showr xs = showsPrecr 0 xs ""
+
+instance (Show a) => Show (FinatSeq n a) where
+    showsPrec = showsPrecl
+
+--------------------------------------------------------------------------------
+-- Common operations
+
+singleton :: a -> FinatSeq SZ a
+singleton = FinatSeqUnsafe . Seq.singleton
+
+length :: FinatSeq n a -> Snat n
+length (FinatSeqUnsafe s) = SnatUnsafe . fromIntegral . Seq.length $ s
+
+lookup :: Finat n -> FinatSeq n a -> a
+lookup (FinatUnsafe i) (FinatSeqUnsafe s) = Seq.index s (fromIntegral i)
+
+adjust :: (a -> a) -> Finat n -> FinatSeq n a -> FinatSeq n a
+adjust f (FinatUnsafe i) = coerce $ Seq.adjust' f (fromIntegral i)
+
+replace :: Finat n -> a -> FinatSeq n a -> FinatSeq n a
+replace k v = adjust (const v) k