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