2 files changed, 16 insertions, 0 deletions
diff --git a/src/Data/Array/Mixed/Shape.hs b/src/Data/Array/Mixed/Shape.hs
index 99a137d..b49e005 100644
--- a/src/Data/Array/Mixed/Shape.hs
+++ b/src/Data/Array/Mixed/Shape.hs
@@ -130,6 +130,9 @@ listxToList :: ListX sh' (Const i) -> [i]
 listxToList ZX = []
 listxToList (Const i ::% is) = i : listxToList is
 
+listxHead :: ListX (mn ': sh) f -> f mn
+listxHead (i ::% _) = i
+
 listxTail :: ListX (n : sh) i -> ListX sh i
 listxTail (_ ::% sh) = sh
 
@@ -201,6 +204,9 @@ ixxZero' (_ :$% sh) = 0 :.% ixxZero' sh
 ixxFromList :: forall sh i. StaticShX sh -> [i] -> IxX sh i
 ixxFromList = coerce (listxFromList @_ @i)
 
+ixxHead :: IxX (n : sh) i -> i
+ixxHead (IxX list) = getConst (listxHead list)
+
 ixxTail :: IxX (n : sh) i -> IxX sh i
 ixxTail (IxX list) = IxX (listxTail list)
 
@@ -372,6 +378,9 @@ shxToList (smn :$% sh) = fromSMayNat' smn : shxToList sh
 shxAppend :: forall sh sh' i. ShX sh i -> ShX sh' i -> ShX (sh ++ sh') i
 shxAppend = coerce (listxAppend @_ @(SMayNat i SNat))
 
+shxHead :: ShX (n : sh) i -> SMayNat i SNat n
+shxHead (ShX list) = listxHead list
+
 shxTail :: ShX (n : sh) i -> ShX sh i
 shxTail (ShX list) = ShX (listxTail list)
 
@@ -474,6 +483,9 @@ ssxAppend :: StaticShX sh -> StaticShX sh' -> StaticShX (sh ++ sh')
 ssxAppend ZKX sh' = sh'
 ssxAppend (n :!% sh) sh' = n :!% ssxAppend sh sh'
 
+ssxHead :: StaticShX (n : sh) -> SMayNat () SNat n
+ssxHead (StaticShX list) = listxHead list
+
 ssxTail :: StaticShX (n : sh) -> StaticShX sh
 ssxTail (_ :!% ssh) = ssh
 
diff --git a/src/Data/Array/Mixed/Types.hs b/src/Data/Array/Mixed/Types.hs
index 13675d0..736ced6 100644
--- a/src/Data/Array/Mixed/Types.hs
+++ b/src/Data/Array/Mixed/Types.hs
@@ -27,6 +27,7 @@ module Data.Array.Mixed.Types (
   Replicate,
   lemReplicateSucc,
   MapJust,
+  Head,
   Tail,
   Init,
   Last,
@@ -103,6 +104,9 @@ type family MapJust l where
   MapJust '[] = '[]
   MapJust (x : xs) = Just x : MapJust xs
 
+type family Head l where
+  Head (x : _) = x
+
 type family Tail l where
   Tail (_ : xs) = xs