-
Notifications
You must be signed in to change notification settings - Fork 48
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
WIP: Revive compact representation for NP/NS #129
base: master
Are you sure you want to change the base?
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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, (:*)) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Do we want to export the There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Moving it would make sense to me, otherwise there are bound to be uses of There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I would definitely want to be able to access the NP constructor as a developer, but putting it in a |
||
, 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) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I'm still unconvinced that There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I started out with just There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. (Well, maybe not concrete concrete, but at least we know something about the structure.) |
||
|
||
-- | 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) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The should be a documentation warning here that the complexity of this for construction is O(n). |
||
infixr 5 :* | ||
|
||
#if __GLASGOW_HASKELL__ >= 802 | ||
{-# COMPLETE Nil, (:*) #-} | ||
#endif | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. We don't need this CPP anymore, as 8.0 is the oldest GHC version we support even now, but in practice, we're probably going to shift the lower bound to 8.6 soon. |
||
|
||
-- 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 | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Same remark as for |
||
, 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 | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Same remark as before. Why not There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. We probably should add an |
||
|
||
-- | 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 _) = | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Add TODO to implement this properly. To be backward compatible this needs to print BTW. The space between
(Otherwise this patch is GHC-9.0 friendly) |
||
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. | ||
-- | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Commenting here for the index_NS :: forall f xs . NS f xs -> Int
index_NS (NS i _) = i |
||
|
@@ -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) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why not inline |
||
|
||
-- The definition of 'ap_SOP' is a more direct variant of | ||
-- '_ap_SOP_spec'. The direct definition has the advantage | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
FWIW, this is definitely not a non-breaking change.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
OTOH,
staged-streams
compiles fine. (Plenty of warnings about non-exhautive pattern matches onNS
, but those are not fatal).There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, my hope was that with the pattern synonym it would be backwards compatible; and those warnings should even be absent from 8.10.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The data structure is now stricter (spine strict?). This is contrived example, but still, the behavior changes observably:
Currently,
With this patch
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, fair enough. Hadn't thought terribly hard about strictness just yet :)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is there a good reason why someone might rely on the construction of the NP being lazy? the idea of writing code which might only look at the first N elements of a NP seems pretty odd to me.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
FWIW, I think that
NP
andNS
should be spine-strict, and not making them so from the beginning was a mistake. Beforesop-core
, I'd have said there's basically no reason not to make the change. Now, it's theoretically possible there are uses that aren't generic programming related which might have other requirements. But it may be worth just doing it.