diff options
| author | Mikolaj Konarski <mikolaj.konarski@gmail.com> | 2024-04-21 23:07:33 +0200 | 
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@gmail.com> | 2024-04-21 23:07:33 +0200 | 
| commit | f29e8a37daf2ed55ea849c286e1bfb1025b67329 (patch) | |
| tree | 2f5a7b7b08b85c7f610014807a0611a89585e7a4 /src | |
| parent | 676ec5132670f6fd94302f9487ee6366d12ba70f (diff) | |
Swap arguments of sized lists to derive Functor, etc.
Diffstat (limited to 'src')
| -rw-r--r-- | src/Data/Array/Mixed.hs | 16 | ||||
| -rw-r--r-- | src/Data/Array/Nested/Internal.hs | 116 | 
2 files changed, 86 insertions, 46 deletions
| 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 | 
