Reorganise, documentation

1 files changed, 70 insertions, 0 deletions

diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs
new file mode 100644
index 0000000..5dacc8a
--- /dev/null
+++ b/src/Data/Nat.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
+module Data.Nat where
+
+import Data.Proxy
+import Numeric.Natural
+import qualified GHC.TypeLits as G
+
+
+-- | Evidence for the constraint @c a@.
+data Dict c a where
+  Dict :: c a => Dict c a
+
+-- | A peano natural number. Intended to be used at the type level.
+data Nat = Z | S Nat
+  deriving (Show)
+
+-- | Singleton for a 'Nat'.
+data SNat n where
+  SZ :: SNat Z
+  SS :: SNat n -> SNat (S n)
+deriving instance Show (SNat n)
+
+-- | A singleton 'SNat' corresponding to @n@.
+class KnownNat n where knownNat :: SNat n
+instance KnownNat Z where knownNat = SZ
+instance KnownNat n => KnownNat (S n) where knownNat = SS knownNat
+
+-- | Convert a 'Nat' to a normal number.
+unNat :: Nat -> Natural
+unNat Z = 0
+unNat (S n) = 1 + unNat n
+
+-- | Convert an 'SNat' to a normal number.
+unSNat :: SNat n -> Natural
+unSNat SZ = 0
+unSNat (SS n) = 1 + unSNat n
+
+-- | A 'KnownNat' dictionary is just a singleton natural, so we can create
+-- evidence of 'KnownNat' given an 'SNat'.
+snatKnown :: SNat n -> Dict KnownNat n
+snatKnown SZ = Dict
+snatKnown (SS n) | Dict <- snatKnown n = Dict
+
+-- | Add two 'Nat's
+type family n + m where
+  Z + m = m
+  S n + m = S (n + m)
+
+-- | Convert a 'Nat' to a "GHC.TypeLits" 'G.Nat'.
+type family GNat n where
+  GNat Z = 0
+  GNat (S n) = 1 G.+ GNat n
+
+-- | If an inductive 'Nat' is known, then the corresponding "GHC.TypeLits"
+-- 'G.Nat' is also known.
+gknownNat :: KnownNat n => Proxy n -> Dict G.KnownNat (GNat n)
+gknownNat (Proxy @n) = go (knownNat @n)
+  where
+    go :: SNat m -> Dict G.KnownNat (GNat m)
+    go SZ = Dict
+    go (SS n) | Dict <- go n = Dict