Officially describe the data invariant for ListX and the punched holes

1 files changed, 15 insertions, 5 deletions

diff --git a/src/Data/Array/Nested/Mixed/ListX.hs b/src/Data/Array/Nested/Mixed/ListX.hs
index e89d1c8..ae3c89f 100644
--- a/src/Data/Array/Nested/Mixed/ListX.hs
+++ b/src/Data/Array/Nested/Mixed/ListX.hs
@@ -42,10 +42,10 @@ import Data.Array.Nested.Types
 
 -- * Mixed lists implementation
 
+-- | Data invariant: each element is in WHNF (the spine may be be not forced).
 type role ListX nominal representational
 type ListX :: [Maybe Nat] -> Type -> Type
 newtype ListX sh i = ListX [i]
-  -- data invariant: each element is in WHNF; the spine maybe be not forced
   deriving (Eq, Ord, NFData, Foldable)
 
 pattern ZX :: forall sh i. () => sh ~ '[] => ListX sh i
@@ -62,28 +62,38 @@ pattern (::%)
   :: forall {sh1} {i}.
      forall n sh. (n : sh ~ sh1)
   => i -> ListX sh i -> ListX sh1 i
-pattern i ::% sh <- (listxUncons -> Just (UnconsListXRes sh i))
-  where !i ::% ListX !sh = ListX (i : sh)
+pattern i ::% l <- (listxUncons -> Just (UnconsListXRes l i))
+  where !i ::% ListX !l = ListX (i : l)
 infixr 3 ::%
 
 data UnconsListXRes i sh1 =
   forall n sh. (n : sh ~ sh1) => UnconsListXRes (ListX sh i) i
 {-# INLINE listxUncons #-}
 listxUncons :: forall sh1 i. ListX sh1 i -> Maybe (UnconsListXRes i sh1)
-listxUncons (ListX (i : sh')) = gcastWith (unsafeCoerceRefl :: Head sh1 ': Tail sh1 :~: sh1) $
-                                Just (UnconsListXRes (ListX @(Tail sh1) sh') i)
+listxUncons (ListX (i : l)) = gcastWith (unsafeCoerceRefl :: Head sh1 ': Tail sh1 :~: sh1) $
+                              Just (UnconsListXRes (ListX @(Tail sh1) l) i)
 listxUncons (ListX []) = Nothing
 
 {-# COMPLETE ZX, (::%) #-}
 
+-- | This operation may not preserve the data invariant for ListX,
+-- regardless whether the invariant holds for the argument list.
+-- It's the user's obligation to honor the data invariant,
+-- e.g., by forcing all new elements of the resulting list at the end.
 {-# INLINE lazily #-}
 lazily :: ([a] -> [b]) -> ListX sh a -> ListX sh b
 lazily f (ListX l) = ListX $ f l
 
+-- | This operation may not preserve the data invariant for ListX,
+-- regardless whether the invariant holds for the argument lists.
+-- It's the user's obligation to honor the data invariant,
+-- e.g., by forcing all new elements of the resulting list at the end.
 {-# INLINE lazilyConcat #-}
 lazilyConcat :: ([a] -> [b] -> [c]) -> ListX sh a -> ListX sh' b -> ListX (sh ++ sh') c
 lazilyConcat f (ListX l) (ListX k) = ListX $ f l k
 
+-- | This operation honours the data invariant for @ListX@ by forcing
+-- all elements of the resulting list at the end.
 {-# INLINE lazilyForce #-}
 lazilyForce :: ([a] -> [b]) -> ListX sh a -> ListX sh b
 lazilyForce f (ListX l) = let res = f l