From f29e8a37daf2ed55ea849c286e1bfb1025b67329 Mon Sep 17 00:00:00 2001
From: Mikolaj Konarski <mikolaj.konarski@gmail.com>
Date: Sun, 21 Apr 2024 23:07:33 +0200
Subject: Swap arguments of sized lists to derive Functor, etc.

---
 src/Data/Array/Mixed.hs           |  16 +++---
 src/Data/Array/Nested/Internal.hs | 116 +++++++++++++++++++++++++-------------
 2 files changed, 86 insertions(+), 46 deletions(-)

(limited to 'src/Data/Array')

diff --git a/src/Data/Array/Mixed.hs b/src/Data/Array/Mixed.hs
index d2765b6..8b90547 100644
--- a/src/Data/Array/Mixed.hs
+++ b/src/Data/Array/Mixed.hs
@@ -47,17 +47,17 @@ lemAppAssoc _ _ _ = unsafeCoerce Refl
 -- TODO: ListX? But if so, why is StaticShapeX not defined as a newtype
 -- over IxX (so that we can make IxX and StaticShapeX a newtype over ListX)?
 
-type IxX :: Type -> [Maybe Nat] -> Type
-data IxX i sh where
-  ZIX :: IxX i '[]
-  (:.@) :: forall n sh i. i -> IxX i sh -> IxX i (Just n : sh)
-  (:.?) :: forall sh i. i -> IxX i sh -> IxX i (Nothing : sh)
-deriving instance Show i => Show (IxX i sh)
-deriving instance Eq i => Eq (IxX i sh)
+type IxX :: [Maybe Nat] -> Type -> Type
+data IxX sh i where
+  ZIX :: IxX '[] i
+  (:.@) :: forall n sh i. i -> IxX sh i -> IxX (Just n : sh) i
+  (:.?) :: forall sh i. i -> IxX sh i -> IxX (Nothing : sh) i
+deriving instance Show i => Show (IxX sh i)
+deriving instance Eq i => Eq (IxX sh i)
 infixr 3 :.@
 infixr 3 :.?
 
-type IIxX = IxX Int
+type IIxX sh = IxX sh Int
 
 -- | The part of a shape that is statically known.
 type StaticShapeX :: [Maybe Nat] -> Type
diff --git a/src/Data/Array/Nested/Internal.hs b/src/Data/Array/Nested/Internal.hs
index 9cabdc6..b758e55 100644
--- a/src/Data/Array/Nested/Internal.hs
+++ b/src/Data/Array/Nested/Internal.hs
@@ -1,8 +1,10 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE DerivingVia #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
@@ -850,59 +852,78 @@ instance (KnownINat n, Storable a, Num a) => Num (Ranked n (Primitive a)) where
 deriving via Ranked n (Primitive Int) instance KnownINat n => Num (Ranked n Int)
 deriving via Ranked n (Primitive Double) instance KnownINat n => Num (Ranked n Double)
 
-type ListR :: Type -> INat -> Type
-data ListR i n where
-  ZR :: ListR i Z
-  (:::) :: forall n i. i -> ListR i n -> ListR i (S n)
-deriving instance Show i => Show (ListR i n)
-deriving instance Eq i => Eq (ListR i n)
+type ListR :: INat -> Type -> Type
+data ListR n i where
+  ZR :: ListR Z i
+  (:::) :: forall n i. i -> ListR n i -> ListR (S n) i
+deriving instance Show i => Show (ListR n i)
+deriving instance Eq i => Eq (ListR n i)
 infixr 3 :::
 
+deriving stock instance Functor (ListR n)
+
+instance Foldable (ListR n) where
+  foldr f z l = foldr f z (listRToList l)
+
+listRToList :: ListR n i -> [i]
+listRToList ZR = []
+listRToList (i ::: is) = i : listRToList is
+
 -- | An index into a rank-typed array.
-type IxR :: Type -> INat -> Type
-newtype IxR i n = IxR (ListR i n)
+type IxR :: INat -> Type -> Type
+newtype IxR n i = IxR (ListR n i)
   deriving (Show, Eq)
 
-pattern ZIR :: forall n i. () => n ~ Z => IxR i n
+deriving newtype instance Functor (IxR n)
+
+instance Foldable (IxR n) where
+  foldr f z (IxR l) = foldr f z l
+
+pattern ZIR :: forall n i. () => n ~ Z => IxR n i
 pattern ZIR = IxR ZR
 
 pattern (:.:)
   :: forall {n1} {i}.
      forall n. ((S n) ~ n1)
-  => i -> IxR i n -> IxR i n1
+  => i -> IxR n i -> IxR n1 i
 pattern i :.: sh <- (unconsIxR -> Just (UnconsIxRRes sh i))
   where i :.: (IxR sh) = IxR (i ::: sh)
 {-# COMPLETE ZIR, (:.:) #-}
 infixr 3 :.:
 
 data UnconsIxRRes i n1 =
-  forall n. ((S n) ~ n1) => UnconsIxRRes (IxR i n) i
-unconsIxR :: IxR i n1 -> Maybe (UnconsIxRRes i n1)
+  forall n. ((S n) ~ n1) => UnconsIxRRes (IxR n i) i
+unconsIxR :: IxR n1 i -> Maybe (UnconsIxRRes i n1)
 unconsIxR (IxR sh) = case sh of
   i ::: sh' -> Just (UnconsIxRRes (IxR sh') i)
   ZR -> Nothing
 
-type IIxR = IxR Int
+type IIxR n = IxR n Int
 
-type StaticShapeR :: Type -> INat -> Type
-newtype StaticShapeR i n = StaticShapeR (ListR i n)
+type StaticShapeR :: INat -> Type -> Type
+newtype StaticShapeR n i = StaticShapeR (ListR n i)
   deriving (Show, Eq)
 
-pattern ZSR :: forall n i. () => n ~ Z => StaticShapeR i n
+deriving newtype instance Functor (StaticShapeR n)
+
+instance Foldable (StaticShapeR n) where
+  foldr f z (StaticShapeR l) = foldr f z l
+
+pattern ZSR :: forall n i. () => n ~ Z => StaticShapeR n i
 pattern ZSR = StaticShapeR ZR
 
 pattern (:$:)
   :: forall {n1} {i}.
      forall n. ((S n) ~ n1)
-  => i -> StaticShapeR i n -> StaticShapeR i n1
+  => i -> StaticShapeR n i -> StaticShapeR n1 i
 pattern i :$: sh <- (unconsStaticShapeR -> Just (UnconsStaticShapeRRes sh i))
   where i :$: (StaticShapeR sh) = StaticShapeR (i ::: sh)
 {-# COMPLETE ZSR, (:$:) #-}
 infixr 3 :$:
 
 data UnconsStaticShapeRRes i n1 =
-  forall n. ((S n) ~ n1) => UnconsStaticShapeRRes (StaticShapeR i n) i
-unconsStaticShapeR :: StaticShapeR i n1 -> Maybe (UnconsStaticShapeRRes i n1)
+  forall n. ((S n) ~ n1) => UnconsStaticShapeRRes (StaticShapeR n i) i
+unconsStaticShapeR :: StaticShapeR n1 i -> Maybe (UnconsStaticShapeRRes i n1)
 unconsStaticShapeR (StaticShapeR sh) = case sh of
   i ::: sh' -> Just (UnconsStaticShapeRRes (StaticShapeR sh') i)
   ZR -> Nothing
@@ -1043,64 +1064,83 @@ instance (KnownShape sh, Storable a, Num a) => Num (Shaped sh (Primitive a)) whe
 deriving via Shaped sh (Primitive Int) instance KnownShape sh => Num (Shaped sh Int)
 deriving via Shaped sh (Primitive Double) instance KnownShape sh => Num (Shaped sh Double)
 
-type ListS :: Type -> [Nat] -> Type
-data ListS i n where
-  ZS :: ListS i '[]
-  (::$) :: forall n sh i. i -> ListS i sh -> ListS i (n : sh)
-deriving instance Show i => Show (ListS i n)
-deriving instance Eq i => Eq (ListS i n)
+type ListS :: [Nat] -> Type -> Type
+data ListS sh i where
+  ZS :: ListS '[] i
+  (::$) :: forall n sh i. i -> ListS sh i -> ListS (n : sh) i
+deriving instance Show i => Show (ListS sh i)
+deriving instance Eq i => Eq (ListS sh i)
 infixr 3 ::$
 
+deriving stock instance Functor (ListS sh)
+
+instance Foldable (ListS sh) where
+  foldr f z l = foldr f z (listSToList l)
+
+listSToList :: ListS sh i -> [i]
+listSToList ZS = []
+listSToList (i ::$ is) = i : listSToList is
+
 -- | An index into a shape-typed array.
 --
 -- For convenience, this contains regular 'Int's instead of bounded integers
 -- (traditionally called \"@Fin@\"). Note that because the shape of a
 -- shape-typed array is known statically, you can also retrieve the array shape
 -- from a 'KnownShape' dictionary.
-type IxS :: Type -> [Nat] -> Type
-newtype IxS i sh = IxS (ListS i sh)
+type IxS :: [Nat] -> Type -> Type
+newtype IxS sh i = IxS (ListS sh i)
   deriving (Show, Eq)
 
-pattern ZIS :: forall sh i. () => sh ~ '[] => IxS i sh
+deriving newtype instance Functor (IxS sh)
+
+instance Foldable (IxS sh) where
+  foldr f z (IxS l) = foldr f z l
+
+pattern ZIS :: forall sh i. () => sh ~ '[] => IxS sh i
 pattern ZIS = IxS ZS
 
 pattern (:.$)
   :: forall {sh1} {i}.
      forall n sh. (n : sh ~ sh1)
-  => i -> IxS i sh -> IxS i sh1
+  => i -> IxS sh i -> IxS sh1 i
 pattern i :.$ shl <- (unconsIxS -> Just (UnconsIxSRes shl i))
   where i :.$ (IxS shl) = IxS (i ::$ shl)
 {-# COMPLETE ZIS, (:.$) #-}
 infixr 3 :.$
 
 data UnconsIxSRes i sh1 =
-  forall n sh. (n : sh ~ sh1) => UnconsIxSRes (IxS i sh) i
-unconsIxS :: IxS i sh1 -> Maybe (UnconsIxSRes i sh1)
+  forall n sh. (n : sh ~ sh1) => UnconsIxSRes (IxS sh i) i
+unconsIxS :: IxS sh1 i -> Maybe (UnconsIxSRes i sh1)
 unconsIxS (IxS shl) = case shl of
   i ::$ shl' -> Just (UnconsIxSRes (IxS shl') i)
   ZS -> Nothing
 
-type IIxS = IxS Int
+type IIxS sh = IxS sh Int
 
-type StaticShapeS :: Type -> [Nat] -> Type
-newtype StaticShapeS i sh = StaticShapeS (ListS i sh)
+type StaticShapeS :: [Nat] -> Type -> Type
+newtype StaticShapeS sh i = StaticShapeS (ListS sh i)
   deriving (Show, Eq)
 
-pattern ZSS :: forall sh i. () => sh ~ '[] => StaticShapeS i sh
+deriving newtype instance Functor (StaticShapeS sh)
+
+instance Foldable (StaticShapeS sh) where
+  foldr f z (StaticShapeS l) = foldr f z l
+
+pattern ZSS :: forall sh i. () => sh ~ '[] => StaticShapeS sh i
 pattern ZSS = StaticShapeS ZS
 
 pattern (:$$)
   :: forall {sh1} {i}.
      forall n sh. (n : sh ~ sh1)
-  => i -> StaticShapeS i sh -> StaticShapeS i sh1
+  => i -> StaticShapeS sh i -> StaticShapeS sh1 i
 pattern i :$$ shl <- (unconsStaticShapeS -> Just (UnconsStaticShapeSRes shl i))
   where i :$$ (StaticShapeS shl) = StaticShapeS (i ::$ shl)
 {-# COMPLETE ZSS, (:$$) #-}
 infixr 3 :$$
 
 data UnconsStaticShapeSRes i sh1 =
-  forall n sh. (n : sh ~ sh1) => UnconsStaticShapeSRes (StaticShapeS i sh) i
-unconsStaticShapeS :: StaticShapeS i sh1 -> Maybe (UnconsStaticShapeSRes i sh1)
+  forall n sh. (n : sh ~ sh1) => UnconsStaticShapeSRes (StaticShapeS sh i) i
+unconsStaticShapeS :: StaticShapeS sh1 i -> Maybe (UnconsStaticShapeSRes i sh1)
 unconsStaticShapeS (StaticShapeS shl) = case shl of
   i ::$ shl' -> Just (UnconsStaticShapeSRes (StaticShapeS shl') i)
   ZS -> Nothing
-- 
cgit v1.2.3-70-g09d2