1{-# LANGUAGE AllowAmbiguousTypes    #-}
2{-# LANGUAGE ConstraintKinds        #-}
3{-# LANGUAGE FlexibleInstances      #-}
4{-# LANGUAGE FunctionalDependencies #-}
5{-# LANGUAGE GADTs                  #-}
6{-# LANGUAGE ScopedTypeVariables    #-}
7{-# LANGUAGE TupleSections          #-}
8{-# LANGUAGE TypeApplications       #-}
9{-# LANGUAGE TypeFamilies           #-}
10{-# LANGUAGE TypeInType             #-}
11{-# LANGUAGE TypeOperators          #-}
12{-# LANGUAGE UndecidableInstances   #-}
13
14-----------------------------------------------------------------------------
15-- |
16-- Module      :  Data.Generics.Product.Internal.HList
17-- Copyright   :  (C) 2020 Csongor Kiss
18-- License     :  BSD3
19-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
20-- Stability   :  experimental
21-- Portability :  non-portable
22--
23-- Derive an isomorphism between a product type and a flat HList.
24--
25-----------------------------------------------------------------------------
26
27module Data.Generics.Product.Internal.HList
28  ( GIsList(..)
29  , IndexList (..)
30  , HList (..)
31  , type (++)
32  , Elem
33  , ListTuple (..)
34  , TupleToList
35  ) where
36
37import GHC.TypeLits
38
39import Data.Kind    (Type)
40import GHC.Generics
41import Data.Profunctor.Indexed
42import Data.Generics.Internal.Profunctor.Lens
43import Data.Generics.Internal.Profunctor.Iso
44
45data HList (as :: [Type]) where
46  Nil :: HList '[]
47  (:>) :: a -> HList as -> HList (a ': as)
48
49infixr 5 :>
50
51type family ((as :: [k]) ++ (bs :: [k])) :: [k] where
52  '[]       ++ bs = bs
53  (a ': as) ++ bs = a ': as ++ bs
54
55instance Semigroup (HList '[]) where
56  _ <> _ = Nil
57
58instance Monoid (HList '[]) where
59  mempty  = Nil
60  mappend _ _ = Nil
61
62instance (Semigroup a, Semigroup (HList as)) => Semigroup (HList (a ': as)) where
63  (x :> xs) <> (y :> ys) = (x <> y) :> (xs <> ys)
64
65instance (Monoid a, Monoid (HList as)) => Monoid (HList (a ': as)) where
66  mempty = mempty :> mempty
67  mappend (x :> xs) (y :> ys) = mappend x y :> mappend xs ys
68
69class Elem (as :: [(k, Type)]) (key :: k) (i :: Nat) a | as key -> i a
70instance {-# OVERLAPPING #-} pos ~ 0 => Elem (a ': xs) key pos a
71instance (Elem xs key i a, pos ~ (i + 1)) => Elem (x ': xs) key pos a
72
73class GIsList
74  (f :: Type -> Type)
75  (g :: Type -> Type)
76  (as :: [Type])
77  (bs :: [Type]) | f -> as, g -> bs, bs f -> g, as g -> f where
78
79  glist :: Iso (f x) (g x) (HList as) (HList bs)
80
81instance
82  ( GIsList l l' as as'
83  , GIsList r r' bs bs'
84  , Appending as bs cs as' bs' cs'
85  , cs ~ (as ++ bs)
86  , cs' ~ (as' ++ bs')
87  ) => GIsList (l :*: r) (l' :*: r') cs cs' where
88
89  glist = prodIso . pairing glist glist . appending
90  {-# INLINE glist #-}
91
92instance GIsList f g as bs => GIsList (M1 t meta f) (M1 t meta g) as bs where
93  glist = mIso . glist
94  {-# INLINE glist #-}
95
96instance GIsList (Rec0 a) (Rec0 b) '[a] '[b] where
97  glist = kIso . singleton
98  {-# INLINE glist #-}
99
100instance GIsList U1 U1 '[] '[] where
101  glist = iso (const Nil) (const U1)
102  {-# INLINE glist #-}
103
104--------------------------------------------------------------------------------
105-- | as ++ bs === cs
106class Appending as bs cs as' bs' cs'
107  | as bs cs cs'   -> as' bs'
108  , as' bs' cs cs' -> as bs
109  , as bs          -> cs
110  , as' bs'        -> cs'
111  where
112  appending :: Iso (HList as, HList bs) (HList as', HList bs') (HList cs) (HList cs')
113
114-- | [] ++ bs === bs
115instance Appending '[] bs bs '[] bs' bs' where
116  appending = iso snd (Nil,)
117
118-- | (a : as) ++ bs === (a : cs)
119instance
120  Appending as bs cs as' bs' cs' -- as ++ bs == cs
121  => Appending (a ': as) bs (a ': cs) (a' ': as') bs' (a' ': cs') where
122  appending
123    = pairing (fromIso consing) id -- ((a, as), bs)
124    . assoc3                       -- (a, (as, bs))
125    . pairing id appending         -- (a, cs)
126    . consing                      -- (a : cs)
127
128singleton :: Iso a b (HList '[a]) (HList '[ b])
129singleton = iso (:> Nil) (\(x :> _) -> x)
130
131consing :: Iso (a, HList as) (b, HList bs) (HList (a ': as)) (HList (b ': bs))
132consing = iso (\(x, xs) -> x :> xs) (\(x :> xs) -> (x, xs))
133
134--------------------------------------------------------------------------------
135class IndexList (i :: Nat) as bs a b | i as -> a, i bs -> b, i as b -> bs, i bs a -> as where
136  point :: Lens (HList as) (HList bs) a b
137
138instance {-# OVERLAPPING #-}
139  ( as ~ (a ': as')
140  , bs ~ (b ': as')
141  ) => IndexList 0 as bs a b where
142  point = lens (\(x :> xs) -> (xs, x)) (\(xs, x') -> x' :> xs)
143  {-# INLINE point #-}
144
145instance
146  ( IndexList (n - 1) as' bs' a b
147  , as ~ (x ': as')
148  , bs ~ (x ': bs')
149  ) => IndexList n as bs a b where
150  point = fromIso consing . second' . point @(n-1)
151  {-# INLINE point #-}
152
153--------------------------------------------------------------------------------
154-- * Convert tuples to/from HLists
155
156class ListTuple (tuple :: Type) (tuple' :: Type) (as :: [Type]) (bs :: [Type]) | as -> tuple, bs -> tuple' where
157  tupled :: Iso (HList as) (HList bs) tuple tuple'
158  tupled = iso (listToTuple @tuple @tuple' @as @bs) (tupleToList @tuple @tuple' @as @bs)
159  {-# INLINE tupled #-}
160
161  tupleToList :: tuple' -> HList bs
162  listToTuple :: HList as -> tuple
163
164instance ListTuple () () '[] '[]
165  where
166  tupleToList _ = Nil
167  listToTuple _ = ()
168
169instance ListTuple a a' '[a] '[a'] where
170  tupleToList a
171    = a :> Nil
172  listToTuple (a :> Nil)
173    = a
174
175instance ListTuple
176  (a1, b1) (a2, b2)
177  [a1, b1] [a2, b2]
178  where
179  tupleToList (a, b)
180    = a :> b :> Nil
181  listToTuple (a :> b :> Nil)
182    = (a, b)
183
184instance ListTuple
185  (a1, b1, c1) (a2, b2, c2)
186  [a1, b1, c1] [a2, b2, c2]
187  where
188  tupleToList (a, b, c)
189    = a :> b :> c :> Nil
190  listToTuple (a :> b :> c :> Nil)
191    = (a, b, c)
192
193instance ListTuple
194  (a1, b1, c1, d1) (a2, b2, c2, d2)
195  [a1, b1, c1, d1] [a2, b2, c2, d2]
196  where
197  tupleToList (a, b, c, d)
198    = a :> b :> c :> d:> Nil
199  listToTuple (a :> b :> c :> d :> Nil)
200    = (a, b, c, d)
201
202instance ListTuple
203  (a1, b1, c1, d1, e1) (a2, b2, c2, d2, e2)
204  [a1, b1, c1, d1, e1] [a2, b2, c2, d2, e2]
205  where
206  tupleToList (a, b, c, d, e)
207    = a :> b :> c :> d:> e :> Nil
208  listToTuple (a :> b :> c :> d :> e :> Nil)
209    = (a, b, c, d, e)
210
211instance ListTuple
212  (a1, b1, c1, d1, e1, f1) (a2, b2, c2, d2, e2, f2)
213  [a1, b1, c1, d1, e1, f1] [a2, b2, c2, d2, e2, f2]
214  where
215  tupleToList (a, b, c, d, e, f)
216    = a :> b :> c :> d:> e :> f :> Nil
217  listToTuple (a :> b :> c :> d :> e :> f :> Nil)
218    = (a, b, c, d, e, f)
219
220instance ListTuple
221  (a1, b1, c1, d1, e1, f1, g1) (a2, b2, c2, d2, e2, f2, g2)
222  [a1, b1, c1, d1, e1, f1, g1] [a2, b2, c2, d2, e2, f2, g2]
223  where
224  tupleToList (a, b, c, d, e, f, g)
225    = a :> b :> c :> d:> e :> f :> g :> Nil
226  listToTuple (a :> b :> c :> d :> e :> f :> g :> Nil)
227    = (a, b, c, d, e, f, g)
228
229instance ListTuple
230  (a1, b1, c1, d1, e1, f1, g1, h1) (a2, b2, c2, d2, e2, f2, g2, h2)
231  [a1, b1, c1, d1, e1, f1, g1, h1] [a2, b2, c2, d2, e2, f2, g2, h2]
232  where
233  tupleToList (a, b, c, d, e, f, g, h)
234    = a :> b :> c :> d:> e :> f :> g :> h :> Nil
235  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> Nil)
236    = (a, b, c, d, e, f, g, h)
237
238instance ListTuple
239  (a1, b1, c1, d1, e1, f1, g1, h1, j1) (a2, b2, c2, d2, e2, f2, g2, h2, j2)
240  [a1, b1, c1, d1, e1, f1, g1, h1, j1] [a2, b2, c2, d2, e2, f2, g2, h2, j2]
241  where
242  tupleToList (a, b, c, d, e, f, g, h, j)
243    = a :> b :> c :> d:> e :> f :> g :> h :> j :> Nil
244  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> Nil)
245    = (a, b, c, d, e, f, g, h, j)
246
247instance ListTuple
248  (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2)
249  [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2]
250  where
251  tupleToList (a, b, c, d, e, f, g, h, j, k)
252    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> Nil
253  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> Nil)
254    = (a, b, c, d, e, f, g, h, j, k)
255
256instance ListTuple
257  (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2)
258  [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2]
259  where
260  tupleToList (a, b, c, d, e, f, g, h, j, k, l)
261    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> Nil
262  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> Nil)
263    = (a, b, c, d, e, f, g, h, j, k, l)
264
265instance ListTuple
266  (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2)
267  [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2]
268  where
269  tupleToList (a, b, c, d, e, f, g, h, j, k, l, m)
270    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> Nil
271  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> Nil)
272    = (a, b, c, d, e, f, g, h, j, k, l, m)
273
274instance ListTuple
275  (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2)
276  [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2]
277  where
278  tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n)
279    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> Nil
280  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> Nil)
281    = (a, b, c, d, e, f, g, h, j, k, l, m, n)
282
283instance ListTuple
284  (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2)
285  [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2]
286  where
287  tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o)
288    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> Nil
289  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> Nil)
290    = (a, b, c, d, e, f, g, h, j, k, l, m, n, o)
291
292instance ListTuple
293  (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2)
294  [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2]
295  where
296  tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p)
297    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> Nil
298  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> Nil)
299    = (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p)
300
301instance ListTuple
302  (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2)
303  [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2]
304  where
305  tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q)
306    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> Nil
307  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> Nil)
308    = (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q)
309
310instance ListTuple
311  (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1, r1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2)
312  [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1, r1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2]
313  where
314  tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r)
315    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> r :> Nil
316  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> r :> Nil)
317    = (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r)
318
319instance ListTuple
320  (a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1) (a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2)
321  [a1, b1, c1, d1, e1, f1, g1, h1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1] [a2, b2, c2, d2, e2, f2, g2, h2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2]
322  where
323  tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r, s)
324    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> r :> s :> Nil
325  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> r :> s :> Nil)
326    = (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r, s)
327
328type family TupleToList a where
329  TupleToList () = '[]
330  TupleToList (a, b) = '[a, b]
331  TupleToList (a, b, c) = '[a, b, c]
332  TupleToList (a, b, c, d) = '[a, b, c, d]
333  TupleToList (a, b, c, d, e) = '[a, b, c, d, e]
334  TupleToList (a, b, c, d, e, f) = '[a, b, c, d, e, f]
335  TupleToList (a, b, c, d, e, f, g) = '[a, b, c, d, e, f, g]
336  TupleToList (a, b, c, d, e, f, g, h) = '[a, b, c, d, e, f, g, h]
337  TupleToList (a, b, c, d, e, f, g, h, j) = '[a, b, c, d, e, f, g, h, j]
338  TupleToList (a, b, c, d, e, f, g, h, j, k) = '[a, b, c, d, e, f, g, h, j, k]
339  TupleToList (a, b, c, d, e, f, g, h, j, k, l) = '[a, b, c, d, e, f, g, h, j, k, l]
340  TupleToList (a, b, c, d, e, f, g, h, j, k, l, m) = '[a, b, c, d, e, f, g, h, j, k, l, m]
341  TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n) = '[a, b, c, d, e, f, g, h, j, k, l, m, n]
342  TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o) = '[a, b, c, d, e, f, g, h, j, k, l, m, n, o]
343  TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p) = '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p]
344  TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q) = '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q]
345  TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r) = '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r]
346  TupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r, s) = '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r, s]
347  TupleToList a = '[a]
348