11{-# LANGUAGE  BangPatterns #-}
22{-# LANGUAGE  EmptyCase #-}
3+ {-# LANGUAGE  PatternSynonyms #-}
34{-# LANGUAGE  PolyKinds #-}
45{-# LANGUAGE  ScopedTypeVariables #-}
56{-# LANGUAGE  StandaloneDeriving #-}
67{-# LANGUAGE  UndecidableInstances #-}
8+ {-# LANGUAGE  ViewPatterns #-}
9+ 
710{-# OPTIONS_GHC  -fno-warn-deprecations #-}
11+ 
812--  |  n-ary sums (and sums of products) 
913module  Data.SOP.NS 
1014  ( --  * Datatypes
11-     NS (.. )
15+     NS (.. ,  Z ,  S )
1216  , SOP (.. )
1317  , unSOP 
1418    --  * Constructing sums
@@ -94,6 +98,8 @@ module Data.SOP.NS
9498import  Data.Coerce 
9599import  Data.Kind  (Type )
96100import  Data.Proxy  (Proxy  (.. ))
101+ import  qualified  Data.Vector  as  V 
102+ import  GHC.Exts  (Any )
97103import  Unsafe.Coerce 
98104
99105import  Control.DeepSeq  (NFData (.. ))
@@ -114,10 +120,16 @@ import Data.SOP.Sing
114120--  @i@-th element of the list is of type @x@, then the @i@-th 
115121--  choice of the sum is of type @f x@. 
116122-- 
117- --  The constructor  names are chosen to resemble Peano-style 
123+ --  The pattern synonym  names are chosen to resemble Peano-style 
118124--  natural numbers, i.e., 'Z' is for "zero", and 'S' is for 
119125--  "successor". Chaining 'S' and 'Z' chooses the corresponding 
120- --  component of the sum. 
126+ --  component of the sum. @NS@ is morally equivalent to 
127+ -- 
128+ --  > data NS :: (k -> Type) -> [k] -> Type where 
129+ --  >   Z :: f x -> NS f (x ': xs) 
130+ --  >   S :: NS f xs -> NS f (x ': xs) 
131+ -- 
132+ --  The actual representation however is compact, using just an 'Int'. 
121133-- 
122134--  /Examples:/ 
123135-- 
@@ -146,13 +158,45 @@ import Data.SOP.Sing
146158--  > S (Z (I True)) :: NS I       '[ Char, Bool ] 
147159--  > S (Z (K 1))    :: NS (K Int) '[ Char, Bool ] 
148160-- 
149- data  NS  ::  (k  ->  Type ) ->  [k ] ->  Type  where 
150-   Z  ::  f  x  ->  NS  f  (x  ':  xs )
151-   S  ::  NS  f  xs  ->  NS  f  (x  ':  xs )
161+ data  NS  (f  ::  k  ->  * ) (xs  ::  [k ]) =  NS  ! Int   Any 
162+ 
163+ --  |  View on NP 
164+ -- 
165+ --  This is only used internally, for the definition of the pattern synonyms. 
166+ data  ViewNS  (f  ::  k  ->  * ) (xs  ::  [k ]) where 
167+   IsZ  ::  f  x      ->  ViewNS  f  (x  ':  xs )
168+   IsS  ::  NS  f  xs  ->  ViewNS  f  (x  ':  xs )
169+ 
170+ viewNS  ::  NS  f  xs  ->  ViewNS  f  xs 
171+ viewNS (NS  i x)
172+   |  i ==  0     =  unsafeCoerce (IsZ  (unsafeCoerce x))
173+   |  otherwise  =  unsafeCoerce (IsS  (NS  (i -  1 ) x))
174+ 
175+ pattern  Z  ::  forall  f  xs'  .  () 
176+           =>  forall x xs .  (xs' ~  (x ':  xs)) =>  f x ->  NS  f xs'
177+ pattern  Z  x <-  (viewNS ->  IsZ  x)
178+   where 
179+     Z  x =  NS  0  (unsafeCoerce x)
180+ 
181+ pattern  S  ::  forall  f  xs'  .  () 
182+           =>  forall x xs .  (xs' ~  (x ':  xs)) =>  NS  f xs ->  NS  f xs'
183+ pattern  S  p <-  (viewNS ->  IsS  p)
184+   where 
185+     S  (NS  i x) =  NS  (i +  1 ) x
186+ 
187+ #if  __GLASGOW_HASKELL__ >= 802
188+ {-# COMPLETE  Z, S #-}
189+ #endif 
190+ 
191+ instance  All  (Show   `Compose ` f ) xs  =>  Show   (NS  f  xs ) where 
192+   show  ns @  (NS  i _) = 
193+     show  i ++  "  "   ++  hcollapse (hcmap (Proxy  ::  Proxy  (Show   `Compose ` f )) (K  .  show ) ns)
194+ 
195+ instance  All  (Eq   `Compose ` f ) xs  =>  Eq   (NS  f  xs ) where 
196+   (==)  =  ccompare_NS (Proxy  ::  Proxy  (Eq   `Compose ` f )) False   (==)  False 
152197
153- deriving  instance  All  (Show   `Compose ` f ) xs  =>  Show   (NS  f  xs )
154- deriving  instance  All  (Eq     `Compose ` f ) xs  =>  Eq     (NS  f  xs )
155- deriving  instance  (All  (Eq   `Compose ` f ) xs , All  (Ord   `Compose ` f ) xs ) =>  Ord   (NS  f  xs )
198+ instance  (All  (Eq   `Compose ` f ) xs , All  (Ord   `Compose ` f ) xs ) =>  Ord   (NS  f  xs ) where 
199+   compare  =  ccompare_NS (Proxy  ::  Proxy  (Ord   `Compose ` f )) LT   compare  GT 
156200
157201--  |  @since 0.2.5.0 
158202instance  All  (NFData  `Compose ` f ) xs  =>  NFData  (NS  f  xs ) where 
@@ -201,8 +245,7 @@ shiftEjection (Fn f) = Fn $ (\ns -> case ns of Z _ -> Comp Nothing; S s -> f (K
201245--  @since 0.2.2.0 
202246-- 
203247unZ  ::  NS  f  '[x ] ->  f  x 
204- unZ (Z  x) =  x
205- unZ (S  x) =  case  x of  {}
248+ unZ (NS  _ x) =  unsafeCoerce x
206249
207250--  |  Obtain the index from an n-ary sum. 
208251-- 
@@ -385,18 +428,14 @@ instance HApInjs SOP where
385428
386429--  |  Specialization of 'hap'. 
387430ap_NS  ::  NP  (f  -.->  g ) xs  ->  NS  f  xs  ->  NS  g  xs 
388- ap_NS (Fn  f  :*  _)   (Z  x)   =  Z  (f x)
389- ap_NS (_     :*  fs)  (S  xs)  =  S  (ap_NS fs xs)
390- ap_NS Nil             x       =  case  x of  {}
431+ ap_NS (NP  fs) (NS  i x) =  NS  i (unsafeCoerce (fs V. !  i) x)
391432
392433--  |  Specialization of 'hap'. 
393434ap_SOP   ::  POP  (f  -.->  g ) xss  ->  SOP  f  xss  ->  SOP  g  xss 
394435ap_SOP (POP  fss') (SOP  xss') =  SOP  (go fss' xss')
395436  where 
396437    go  ::  NP  (NP  (f  -.->  g )) xss  ->  NS  (NP  f ) xss  ->  NS  (NP  g ) xss 
397-     go (fs :*  _  ) (Z  xs ) =  Z  (ap_NP fs  xs )
398-     go (_  :*  fss) (S  xss) =  S  (go    fss xss)
399-     go Nil          x       =  case  x of  {}
438+     go (NP  nps) (NS  i ns) =  NS  i (unsafeCoerce ap_NS (nps V. !  i) ns)
400439
401440--  The definition of 'ap_SOP' is a more direct variant of
402441--  '_ap_SOP_spec'. The direct definition has the advantage
0 commit comments