@@ -12,7 +12,6 @@
12{-# LANGUAGE TypeOperators #-}
12{-# LANGUAGE TypeOperators #-}
13{-# LANGUAGE UndecidableInstances #-}
13{-# LANGUAGE UndecidableInstances #-}
15−{-# LANGUAGE DeriveGeneric #-}
16-----------------------------------------------------------------------------
15-----------------------------------------------------------------------------
18-- Module : Data.Generics.Sum.HasConstructor
17-- Module : Data.Generics.Sum.HasConstructor
@@ -24,7 +23,31 @@
25-- Derive prisms generically
24-- Derive prisms generically
27−-- TODO: add examples
26+-- @
31+-- | Baz (Int, String)
33+-- deriving (Show, Generic)
35+-- >>> Bar 5 "coconut" ^? as @"Bar"
36+-- Just (5, "coconut")
38+-- >>> Qux ^? as @"Qux"
41+-- >>> as @"Bar" # (5, "asd") :: FooBar
44+-- >>> as @"Barz" # (5, "asd") :: FooBar
46+-- <interactive>:264:1: error:
47+-- • FooBar has no constructor with name "Barz"
28-----------------------------------------------------------------------------
51-----------------------------------------------------------------------------
30module Data.Generics.Sum.HasConstructor where
53module Data.Generics.Sum.HasConstructor where
@@ -36,14 +59,16 @@ import Data.Kind (Type, Constraint)
36import GHC.Generics
59import GHC.Generics
38class HasConstructor (con :: Symbol) a s | s con -> a where
61class HasConstructor (con :: Symbol) a s | s con -> a where
39− is :: Prism' s a
62+ as :: Prism' s a
42 ( Generic s
65 ( Generic s
43 , ErrorUnless (ContainsC con (Rep s)) con s
66 , ErrorUnless (ContainsC con (Rep s)) con s
44 , GHasConstructor con (Rep s) a
67 , GHasConstructor con (Rep s) a
45 ) => HasConstructor con a s where
68 ) => HasConstructor con a s where
46− is = repIso . gconstruct @con
69+ as = repIso . gconstruct @con
71+--------------------------------------------------------------------------------
48type family ErrorUnless (contains :: Bool) (con :: Symbol) (s :: *) :: Constraint where
73type family ErrorUnless (contains :: Bool) (con :: Symbol) (s :: *) :: Constraint where
49 ErrorUnless 'False con s
74 ErrorUnless 'False con s
@@ -53,6 +78,8 @@ type family ErrorUnless (contains :: Bool) (con :: Symbol) (s :: *) :: Constrain
53 ErrorUnless _ _ _
78 ErrorUnless _ _ _
81+--------------------------------------------------------------------------------
56data HList (xs :: [Type]) where
83data HList (xs :: [Type]) where
57 Nil :: HList '[]
84 Nil :: HList '[]
58 (:>) :: x -> HList xs -> HList (x ': xs)
85 (:>) :: x -> HList xs -> HList (x ': xs)
@@ -67,6 +94,13 @@ class AsList (tup :: *) (xs :: [*]) | xs -> tup where
67 asList :: tup -> HList xs
94 asList :: tup -> HList xs
68 asTuple :: HList xs -> tup
95 asTuple :: HList xs -> tup
97+instance AsList () '[] where
70instance AsList a '[a] where
104instance AsList a '[a] where
72 = a :> Nil
106 = a :> Nil
@@ -127,6 +161,8 @@ type family ((xs :: [k]) ++ (ys :: [k])) :: [k] where
127 '[] ++ ys = ys
161 '[] ++ ys = ys
128 (x ': xs) ++ ys = x ': xs ++ ys
162 (x ': xs) ++ ys = x ': xs ++ ys
164+--------------------------------------------------------------------------------
130class GHasConstructor (con :: Symbol) (s :: Type -> Type) a | con s -> a where
166class GHasConstructor (con :: Symbol) (s :: Type -> Type) a | con s -> a where
131 gconstruct :: Prism' (s x) a
167 gconstruct :: Prism' (s x) a
@@ -151,29 +187,45 @@ instance GHasConstructor con r a => GHasConstructorSum con l r a 'False where
151instance GHasConstructorSum con l r a (ContainsC con l) => GHasConstructor con (l :+: r) a where
187instance GHasConstructorSum con l r a (ContainsC con l) => GHasConstructor con (l :+: r) a where
152 gconstruct = gconstructSum @con @l @r @a @(ContainsC con l)
188 gconstruct = gconstructSum @con @l @r @a @(ContainsC con l)
190+--------------------------------------------------------------------------------
191+-- * Split is the inverse of append
154−class Partition xs ys zs | xs ys -> zs, xs zs -> ys where
193+class Split xs ys zs | xs ys -> zs, xs zs -> ys where
155− partition :: HList zs -> (HList xs, HList ys)
194+ split :: HList zs -> (HList xs, HList ys)
196+instance Split '[] xs xs where
197+ split xs = (Nil, xs)
157−instance Partition '[] xs xs where
199+instance Split xs ys zs => Split (x ': xs) ys (x ': zs) where
158− partition xs = (Nil, xs)
200+ split (x :> xs) = (x :> xs', ys')
201+ where (xs', ys') = split xs
160−instance Partition xs ys zs => Partition (x ': xs) ys (x ': zs) where
203+--------------------------------------------------------------------------------
161− partition (x :> xs) = (x :> xs', ys')
162− where (xs', ys') = partition xs
205+-- | Collect parameters of a constructor into an HList
164class GCollect (s :: Type -> Type) (xs :: [Type]) | s -> xs where
206class GCollect (s :: Type -> Type) (xs :: [Type]) | s -> xs where
165 gfrom :: s x -> HList xs
207 gfrom :: s x -> HList xs
166 gto :: HList xs -> s x
208 gto :: HList xs -> s x
168−instance (GCollect a as, GCollect b bs, xs ~ (as ++ bs), Partition as bs xs) => GCollect (a :*: b) xs where
215+ ) => GCollect (a :*: b) xs where
169 gfrom (a :*: b) = gfrom a `append` gfrom b
217 gfrom (a :*: b) = gfrom a `append` gfrom b
170 gto xs = gto l :*: gto r
218 gto xs = gto l :*: gto r
171− where (l, r) = partition @as @bs xs
219+ where (l, r) = split @as @bs xs
173instance GCollect (K1 R a) '[a] where
221instance GCollect (K1 R a) '[a] where
174 gfrom (K1 x) = x :> Nil
222 gfrom (K1 x) = x :> Nil
175 gto (x :> Nil) = K1 x
223 gto (x :> Nil) = K1 x
225+instance GCollect U1 '[] where
177instance GCollect s a => GCollect (M1 S c s) a where
229instance GCollect s a => GCollect (M1 S c s) a where
178 gfrom (M1 x) = gfrom x
230 gfrom (M1 x) = gfrom x
179 gto x = M1 $ gto x
231 gto x = M1 $ gto x