From cd9f2ef4c312a865414c628adbc00865e7772282 Mon Sep 17 00:00:00 2001 From: Edsko de Vries Date: Thu, 14 Jan 2021 09:02:05 +0100 Subject: [PATCH] Revive compact representation of NP/NS --- generics-sop/generics-sop.cabal | 2 +- generics-sop/src/Generics/SOP/GGP.hs | 3 +- sop-core/sop-core.cabal | 5 +- sop-core/src/Data/SOP/NP.hs | 64 +++++++++++++--- sop-core/src/Data/SOP/NS.hs | 106 ++++++++++++++++++++++----- 5 files changed, 149 insertions(+), 31 deletions(-) diff --git a/generics-sop/generics-sop.cabal b/generics-sop/generics-sop.cabal index 493b623..7f66f46 100644 --- a/generics-sop/generics-sop.cabal +++ b/generics-sop/generics-sop.cabal @@ -66,7 +66,7 @@ library Generics.SOP.NS Generics.SOP.Sing build-depends: base >= 4.9 && < 4.16, - sop-core == 0.5.0.*, + sop-core == 0.5.1.*, template-haskell >= 2.8 && < 2.18, th-abstraction >= 0.4 && < 0.5, ghc-prim >= 0.3 && < 0.8 diff --git a/generics-sop/src/Generics/SOP/GGP.hs b/generics-sop/src/Generics/SOP/GGP.hs index 7b3e6ff..5bb5aae 100644 --- a/generics-sop/src/Generics/SOP/GGP.hs +++ b/generics-sop/src/Generics/SOP/GGP.hs @@ -222,7 +222,7 @@ gfrom x = gSumFrom (GHC.from x) (Proxy :: Proxy '[]) -- For more info, see 'Generics.SOP.Generic'. -- gto :: forall a. (GTo a, GHC.Generic a) => SOP I (GCode a) -> a -gto x = GHC.to (gSumTo x id ((\y -> case y of {}) :: SOP I '[] -> (GHC.Rep a) x)) +gto x = GHC.to (gSumTo x id ((\y -> case emptySOP y of {}) :: SOP I '[] -> (GHC.Rep a) x)) -- | An automatically computed version of 'Generics.SOP.datatypeInfo'. -- @@ -234,4 +234,3 @@ gto x = GHC.to (gSumTo x id ((\y -> case y of {}) :: SOP I '[] -> (GHC.Rep a) x) -- gdatatypeInfo :: forall proxy a. (GDatatypeInfo a) => proxy a -> DatatypeInfo (GCode a) gdatatypeInfo _ = SOP.T.demoteDatatypeInfo (Proxy :: Proxy (GDatatypeInfoOf a)) - diff --git a/sop-core/sop-core.cabal b/sop-core/sop-core.cabal index a87a8cd..8ac00a5 100644 --- a/sop-core/sop-core.cabal +++ b/sop-core/sop-core.cabal @@ -1,5 +1,5 @@ name: sop-core -version: 0.5.0.1 +version: 0.5.1.0 synopsis: True Sums of Products description: Implementation of n-ary sums and n-ary products. @@ -42,7 +42,8 @@ library Data.SOP.NS Data.SOP.Sing build-depends: base >= 4.9 && < 4.16, - deepseq >= 1.3 && < 1.5 + deepseq >= 1.3 && < 1.5, + vector >= 0.12 && < 0.13 hs-source-dirs: src default-language: Haskell2010 ghc-options: -Wall diff --git a/sop-core/src/Data/SOP/NP.hs b/sop-core/src/Data/SOP/NP.hs index 4d92cfb..d6ce9d2 100644 --- a/sop-core/src/Data/SOP/NP.hs +++ b/sop-core/src/Data/SOP/NP.hs @@ -1,8 +1,13 @@ -{-# LANGUAGE PolyKinds, StandaloneDeriving, UndecidableInstances #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} + -- | n-ary products (and products of products) module Data.SOP.NP ( -- * Datatypes - NP(..) + NP(.., Nil, (:*)) , POP(..) , unPOP -- * Constructing products @@ -90,6 +95,8 @@ module Data.SOP.NP import Data.Coerce import Data.Kind (Type) import Data.Proxy (Proxy(..)) +import qualified Data.Vector as V +import GHC.Exts (Any) import Unsafe.Coerce #if !MIN_VERSION_base(4,11,0) import Data.Semigroup (Semigroup (..)) @@ -110,8 +117,14 @@ import Data.SOP.Sing -- @i@-th element of the list is of type @x@, then the @i@-th -- element of the product is of type @f x@. -- --- The constructor names are chosen to resemble the names of the --- list constructors. +-- The pattern synoyms are chosen to resemble the names of the +-- list constructors. @NP@ is morally equivalent to: +-- +-- > data NP :: (k -> Type) -> [k] -> Type where +-- > Nil :: NP f '[] +-- > (:*) :: f x -> NP f xs -> NP f (x ': xs) +-- +-- The actual representation however is compact, using an array. -- -- Two common instantiations of @f@ are the identity functor 'I' -- and the constant functor 'K'. For 'I', the product becomes a @@ -130,12 +143,40 @@ import Data.SOP.Sing -- > K 0 :* K 1 :* Nil :: NP (K Int) '[ Char, Bool ] -- > Just 'x' :* Nothing :* Nil :: NP Maybe '[ Char, Bool ] -- -data NP :: (k -> Type) -> [k] -> Type where - Nil :: NP f '[] - (:*) :: f x -> NP f xs -> NP f (x ': xs) +newtype NP (f :: k -> *) (xs :: [k]) = NP (V.Vector Any) + +-- | View on NP +-- +-- This is only used internally, for the definition of the pattern synonyms. +data ViewNP (f :: k -> *) (xs :: [k]) where + IsNil :: ViewNP f '[] + IsCons :: f x -> NP f xs -> ViewNP f (x ': xs) + +-- | Construct 'ViewNP' +-- +-- NOTE: 'V.unsafeTail' is O(1). +viewNP :: NP f xs -> ViewNP f xs +viewNP (NP xs) + | null xs = unsafeCoerce $ IsNil + | otherwise = unsafeCoerce $ IsCons (unsafeCoerce (V.unsafeHead xs)) + (NP (V.unsafeTail xs)) +pattern Nil :: forall f xs . () => (xs ~ '[]) => NP f xs +pattern Nil <- (viewNP -> IsNil) + where + Nil = NP V.empty + +pattern (:*) :: forall f xs' . () + => forall x xs . (xs' ~ (x ': xs)) => f x -> NP f xs -> NP f xs' +pattern x :* xs <- (viewNP -> IsCons x xs) + where + x :* NP xs = NP (V.cons (unsafeCoerce x) xs) infixr 5 :* +#if __GLASGOW_HASKELL__ >= 802 +{-# COMPLETE Nil, (:*) #-} +#endif + -- This is written manually, -- because built-in deriving doesn't use associativity information! instance All (Show `Compose` f) xs => Show (NP f xs) where @@ -145,8 +186,13 @@ instance All (Show `Compose` f) xs => Show (NP f xs) where . showString " :* " . showsPrec 5 fs -deriving instance All (Eq `Compose` f) xs => Eq (NP f xs) -deriving instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NP f xs) +instance All (Eq `Compose` f) xs => Eq (NP f xs) where + xs == ys = + and (hcollapse (hczipWith (Proxy :: Proxy (Eq `Compose` f)) (\ x y -> K (x == y)) xs ys)) + +instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NP f xs) where + compare xs ys = + mconcat (hcollapse (hczipWith (Proxy :: Proxy (Ord `Compose` f)) (\ x y -> K (compare x y)) xs ys)) -- | @since 0.4.0.0 instance All (Semigroup `Compose` f) xs => Semigroup (NP f xs) where diff --git a/sop-core/src/Data/SOP/NS.hs b/sop-core/src/Data/SOP/NS.hs index 5424132..7144fe2 100644 --- a/sop-core/src/Data/SOP/NS.hs +++ b/sop-core/src/Data/SOP/NS.hs @@ -1,14 +1,18 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE EmptyCase #-} +{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} + {-# OPTIONS_GHC -fno-warn-deprecations #-} + -- | n-ary sums (and sums of products) module Data.SOP.NS ( -- * Datatypes - NS(..) + NS(.., Z, S) , SOP(..) , unSOP -- * Constructing sums @@ -20,7 +24,11 @@ module Data.SOP.NS , apInjs'_NP , apInjs_POP , apInjs'_POP + -- See also 'emptySOP'. + -- -- * Destructing sums + , emptyNS + , emptySOP , unZ , index_NS , index_SOP @@ -94,6 +102,9 @@ module Data.SOP.NS import Data.Coerce import Data.Kind (Type) import Data.Proxy (Proxy (..)) +import qualified Data.Vector as V +import Data.Void (Void) +import GHC.Exts (Any) import Unsafe.Coerce import Control.DeepSeq (NFData(..)) @@ -114,10 +125,16 @@ import Data.SOP.Sing -- @i@-th element of the list is of type @x@, then the @i@-th -- choice of the sum is of type @f x@. -- --- The constructor names are chosen to resemble Peano-style +-- The pattern synonym names are chosen to resemble Peano-style -- natural numbers, i.e., 'Z' is for "zero", and 'S' is for -- "successor". Chaining 'S' and 'Z' chooses the corresponding --- component of the sum. +-- component of the sum. @NS@ is morally equivalent to +-- +-- > data NS :: (k -> Type) -> [k] -> Type where +-- > Z :: f x -> NS f (x ': xs) +-- > S :: NS f xs -> NS f (x ': xs) +-- +-- The actual representation however is compact, using just an 'Int'. -- -- /Examples:/ -- @@ -146,13 +163,45 @@ import Data.SOP.Sing -- > S (Z (I True)) :: NS I '[ Char, Bool ] -- > S (Z (K 1)) :: NS (K Int) '[ Char, Bool ] -- -data NS :: (k -> Type) -> [k] -> Type where - Z :: f x -> NS f (x ': xs) - S :: NS f xs -> NS f (x ': xs) +data NS (f :: k -> *) (xs :: [k]) = NS !Int Any + +-- | View on NP +-- +-- This is only used internally, for the definition of the pattern synonyms. +data ViewNS (f :: k -> *) (xs :: [k]) where + IsZ :: f x -> ViewNS f (x ': xs) + IsS :: NS f xs -> ViewNS f (x ': xs) + +viewNS :: NS f xs -> ViewNS f xs +viewNS (NS i x) + | i == 0 = unsafeCoerce (IsZ (unsafeCoerce x)) + | otherwise = unsafeCoerce (IsS (NS (i - 1) x)) + +pattern Z :: forall f xs' . () + => forall x xs . (xs' ~ (x ': xs)) => f x -> NS f xs' +pattern Z x <- (viewNS -> IsZ x) + where + Z x = NS 0 (unsafeCoerce x) + +pattern S :: forall f xs' . () + => forall x xs . (xs' ~ (x ': xs)) => NS f xs -> NS f xs' +pattern S p <- (viewNS -> IsS p) + where + S (NS i x) = NS (i + 1) x + +#if __GLASGOW_HASKELL__ >= 802 +{-# COMPLETE Z, S #-} +#endif -deriving instance All (Show `Compose` f) xs => Show (NS f xs) -deriving instance All (Eq `Compose` f) xs => Eq (NS f xs) -deriving instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NS f xs) +instance All (Show `Compose` f) xs => Show (NS f xs) where + show ns @ (NS i _) = + show i ++ " " ++ hcollapse (hcmap (Proxy :: Proxy (Show `Compose` f)) (K . show) ns) + +instance All (Eq `Compose` f) xs => Eq (NS f xs) where + (==) = ccompare_NS (Proxy :: Proxy (Eq `Compose` f)) False (==) False + +instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NS f xs) where + compare = ccompare_NS (Proxy :: Proxy (Ord `Compose` f)) LT compare GT -- | @since 0.2.5.0 instance All (NFData `Compose` f) xs => NFData (NS f xs) where @@ -188,6 +237,34 @@ ejections = case sList :: SList xs of shiftEjection :: forall f x xs a . Ejection f xs a -> Ejection f (x ': xs) a shiftEjection (Fn f) = Fn $ (\ns -> case ns of Z _ -> Comp Nothing; S s -> f (K s)) . unK +-- | An 'NS' cannot be empty. +-- +-- Although the 'Z'/'S' pattern synonyms are marked as @COMPLETE@, older @ghc@ +-- (before 8.10) are not clever enough to deduce from that an empty pattern +-- match in which both @Z@ and @S@ would be type incorrect is not, in fact, +-- incomplete. This function can be used to avoid warnings in such cases; +-- instead of writing +-- +-- > case x of {} +-- +-- (where @x :: NS f '[])@), instead write +-- +-- > case emptyNS x of {} +-- +-- See also 'emptySOP'. +-- +-- @since 0.5.1.0 +emptyNS :: NS f '[] -> Void +emptyNS _ = error "emptyNS: impossible" + +-- | An 'SOP' cannot be empty (beacuse an 'NS' cannot be). +-- +-- See also 'emptyNS'. +-- +-- @since 0.5.1.0 +emptySOP :: SOP f '[] -> Void +emptySOP = emptyNS . unSOP + -- | Extract the payload from a unary sum. -- -- For larger sums, this function would be partial, so it is only @@ -201,8 +278,7 @@ shiftEjection (Fn f) = Fn $ (\ns -> case ns of Z _ -> Comp Nothing; S s -> f (K -- @since 0.2.2.0 -- unZ :: NS f '[x] -> f x -unZ (Z x) = x -unZ (S x) = case x of {} +unZ (NS _ x) = unsafeCoerce x -- | Obtain the index from an n-ary sum. -- @@ -385,18 +461,14 @@ instance HApInjs SOP where -- | Specialization of 'hap'. ap_NS :: NP (f -.-> g) xs -> NS f xs -> NS g xs -ap_NS (Fn f :* _) (Z x) = Z (f x) -ap_NS (_ :* fs) (S xs) = S (ap_NS fs xs) -ap_NS Nil x = case x of {} +ap_NS (NP fs) (NS i x) = NS i (unsafeCoerce (fs V.! i) x) -- | Specialization of 'hap'. ap_SOP :: POP (f -.-> g) xss -> SOP f xss -> SOP g xss ap_SOP (POP fss') (SOP xss') = SOP (go fss' xss') where go :: NP (NP (f -.-> g)) xss -> NS (NP f) xss -> NS (NP g) xss - go (fs :* _ ) (Z xs ) = Z (ap_NP fs xs ) - go (_ :* fss) (S xss) = S (go fss xss) - go Nil x = case x of {} + go (NP nps) (NS i ns) = NS i (unsafeCoerce ap_NS (nps V.! i) ns) -- The definition of 'ap_SOP' is a more direct variant of -- '_ap_SOP_spec'. The direct definition has the advantage