commit 3da4f50ce0b62a10d2c8c6d0216350639b45d1ec
Author: Robert Russell <robert@rr3.xyz>
Date: Thu, 26 Jun 2025 22:35:14 -0700
Initial commit
Diffstat:
6 files changed, 177 insertions(+), 0 deletions(-)
diff --git a/.gitignore b/.gitignore
@@ -0,0 +1,3 @@
+*.cabal
+stack.yaml.lock
+.stack-work
diff --git a/package.yaml b/package.yaml
@@ -0,0 +1,37 @@
+name: snats
+author: Robert Russell
+
+ghc-options:
+ - -Wall
+ - -Wno-name-shadowing
+ - -Wno-unused-top-binds
+
+language: GHC2021
+
+default-extensions:
+ - BlockArguments
+ - DataKinds
+ - DefaultSignatures
+ - DerivingVia
+ - FunctionalDependencies
+ - GADTs
+ - LambdaCase
+ - MagicHash
+ - OverloadedStrings
+ - PartialTypeSignatures
+ - PatternSynonyms
+ - QuantifiedConstraints
+ - RecursiveDo
+ - TypeData
+ - TypeFamilies
+ - UnboxedTuples
+ - UnicodeSyntax
+ - UnliftedNewtypes
+ - UnliftedDatatypes
+ - ViewPatterns
+
+dependencies:
+ - base
+
+library:
+ source-dirs: src
diff --git a/src/Snats/Nat.hs b/src/Snats/Nat.hs
@@ -0,0 +1,48 @@
+module Snats.Nat (
+ Nat (..),
+ CaseDecision (..),
+ Pred,
+ Add,
+) where
+
+import Control.Exception
+
+-- | Unary natural numbers. Intended mainly for use at the type-level.
+data Nat = Z | S Nat deriving (Show, Eq)
+
+instance Ord Nat where
+ Z `compare` Z = EQ
+ S _ `compare` Z = GT
+ Z `compare` S _ = LT
+ S m `compare` S n = m `compare` n
+
+instance Num Nat 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
+
+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)
diff --git a/src/Snats/Snat.hs b/src/Snats/Snat.hs
@@ -0,0 +1,45 @@
+module Snats.Snat (
+ module Snats.Nat,
+ Snat, -- Don't export the constructor!
+ pattern Zero,
+ pattern Succ,
+ toWord,
+ decideCase,
+ snat,
+ pred,
+ add,
+) 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
diff --git a/src/Snats/Snatural.hs b/src/Snats/Snatural.hs
@@ -0,0 +1,43 @@
+module Snats.Snatural (
+ module Snats.Nat,
+ Snatural, -- Don't export the constructor!
+ pattern Zero,
+ pattern Succ,
+ toNatural,
+ decideCase,
+ snatural,
+ pred,
+ add,
+) 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)
diff --git a/stack.yaml b/stack.yaml
@@ -0,0 +1 @@
+resolver: lts-23.23
