1 files changed, 25 insertions, 0 deletions
diff --git a/src/Data.hs b/src/Data.hs
index bd7f3af..728dafe 100644
--- a/src/Data.hs
+++ b/src/Data.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DeriveTraversable #-}
 module Data where
 
 
@@ -17,3 +18,27 @@ infixr `SCons`
 slistMap :: (forall t. f t -> g t) -> SList f list -> SList g list
 slistMap _ SNil = SNil
 slistMap f (SCons x list) = SCons (f x) (slistMap f list)
+
+data Nat = Z | S Nat
+  deriving (Show, Eq, Ord)
+
+data SNat n where
+  SZ :: SNat Z
+  SS :: SNat n -> SNat (S n)
+deriving instance Show (SNat n)
+
+fromSNat :: SNat n -> Int
+fromSNat SZ = 0
+fromSNat (SS n) = succ (fromSNat n)
+
+data Vec n t where
+  VNil :: Vec Z t
+  (:<) :: t -> Vec n t -> Vec (S n) t
+deriving instance Show t => Show (Vec n t)
+deriving instance Functor (Vec n)
+deriving instance Foldable (Vec n)
+deriving instance Traversable (Vec n)
+
+vecLength :: Vec n t -> SNat n
+vecLength VNil = SZ
+vecLength (_ :< v) = SS (vecLength v)