@@ -12,7 +12,6 @@
1212{-# LANGUAGE TypeOperators #-}
1313{-# LANGUAGE UndecidableInstances #-}
1414
15−{-# LANGUAGE DeriveGeneric #-}
1615-----------------------------------------------------------------------------
1716-- |
1817-- Module : Data.Generics.Sum.HasConstructor
@@ -24,7 +23,31 @@
2423--
2524-- Derive prisms generically
2625--
27−-- TODO: add examples
26+-- @
27+--
28+-- data FooBar
29+-- = Foo Int
30+-- | Bar Int String
31+-- | Baz (Int, String)
32+-- | Qux
33+-- deriving (Show, Generic)
34+--
35+-- >>> Bar 5 "coconut" ^? as @"Bar"
36+-- Just (5, "coconut")
37+--
38+-- >>> Qux ^? as @"Qux"
39+-- Just ()
40+--
41+-- >>> as @"Bar" # (5, "asd") :: FooBar
42+-- Bar 5 "asd"
43+--
44+-- >>> as @"Barz" # (5, "asd") :: FooBar
45+--
46+-- <interactive>:264:1: error:
47+-- • FooBar has no constructor with name "Barz"
48+-- @
49+--
50+
2851-----------------------------------------------------------------------------
2952
3053module Data.Generics.Sum.HasConstructor where
@@ -36,14 +59,16 @@ import Data.Kind (Type, Constraint)
3659import GHC.Generics
3760
3861class HasConstructor (con :: Symbol) a s | s con -> a where
39− is :: Prism' s a
62+ as :: Prism' s a
4063
4164instance
4265 ( Generic s
4366 , ErrorUnless (ContainsC con (Rep s)) con s
4467 , GHasConstructor con (Rep s) a
4568 ) => HasConstructor con a s where
46− is = repIso . gconstruct @con
69+ as = repIso . gconstruct @con
70+
71+--------------------------------------------------------------------------------
4772
4873type family ErrorUnless (contains :: Bool) (con :: Symbol) (s :: *) :: Constraint where
4974 ErrorUnless 'False con s
@@ -53,6 +78,8 @@ type family ErrorUnless (contains :: Bool) (con :: Symbol) (s :: *) :: Constrain
5378 ErrorUnless _ _ _
5479 = ()
5580
81+--------------------------------------------------------------------------------
82+
5683data HList (xs :: [Type]) where
5784 Nil :: HList '[]
5885 (:>) :: x -> HList xs -> HList (x ': xs)
@@ -67,6 +94,13 @@ class AsList (tup :: *) (xs :: [*]) | xs -> tup where
6794 asList :: tup -> HList xs
6895 asTuple :: HList xs -> tup
6996
97+instance AsList () '[] where
98+ asList _
99+ = Nil
100+
101+ asTuple _
102+ = ()
103+
70104instance AsList a '[a] where
71105 asList a
72106 = a :> Nil
@@ -127,6 +161,8 @@ type family ((xs :: [k]) ++ (ys :: [k])) :: [k] where
127161 '[] ++ ys = ys
128162 (x ': xs) ++ ys = x ': xs ++ ys
129163
164+--------------------------------------------------------------------------------
165+
130166class GHasConstructor (con :: Symbol) (s :: Type -> Type) a | con s -> a where
131167 gconstruct :: Prism' (s x) a
132168
@@ -151,29 +187,45 @@ instance GHasConstructor con r a => GHasConstructorSum con l r a 'False where
151187instance GHasConstructorSum con l r a (ContainsC con l) => GHasConstructor con (l :+: r) a where
152188 gconstruct = gconstructSum @con @l @r @a @(ContainsC con l)
153189
154−class Partition xs ys zs | xs ys -> zs, xs zs -> ys where
155− partition :: HList zs -> (HList xs, HList ys)
190+--------------------------------------------------------------------------------
191+-- * Split is the inverse of append
192+
193+class Split xs ys zs | xs ys -> zs, xs zs -> ys where
194+ split :: HList zs -> (HList xs, HList ys)
195+
196+instance Split '[] xs xs where
197+ split xs = (Nil, xs)
156198
157−instance Partition '[] xs xs where
158− partition xs = (Nil, xs)
199+instance Split xs ys zs => Split (x ': xs) ys (x ': zs) where
200+ split (x :> xs) = (x :> xs', ys')
201+ where (xs', ys') = split xs
159202
160−instance Partition xs ys zs => Partition (x ': xs) ys (x ': zs) where
161− partition (x :> xs) = (x :> xs', ys')
162− where (xs', ys') = partition xs
203+--------------------------------------------------------------------------------
163204
205+-- | Collect parameters of a constructor into an HList
164206class GCollect (s :: Type -> Type) (xs :: [Type]) | s -> xs where
165207 gfrom :: s x -> HList xs
166208 gto :: HList xs -> s x
167209
168−instance (GCollect a as, GCollect b bs, xs ~ (as ++ bs), Partition as bs xs) => GCollect (a :*: b) xs where
210+instance
211+ ( GCollect a as
212+ , GCollect b bs
213+ , xs ~ (as ++ bs)
214+ , Split as bs xs
215+ ) => GCollect (a :*: b) xs where
216+
169217 gfrom (a :*: b) = gfrom a `append` gfrom b
170218 gto xs = gto l :*: gto r
171− where (l, r) = partition @as @bs xs
219+ where (l, r) = split @as @bs xs
172220
173221instance GCollect (K1 R a) '[a] where
174222 gfrom (K1 x) = x :> Nil
175223 gto (x :> Nil) = K1 x
176224
225+instance GCollect U1 '[] where
226+ gfrom U1 = Nil
227+ gto Nil = U1
228+
177229instance GCollect s a => GCollect (M1 S c s) a where
178230 gfrom (M1 x) = gfrom x
179231 gto x = M1 $ gto x