3 module T3330c where
5 import Data.Kind
7 data (f :+: g) x = Inl (f x) | Inr (g x)
9 data R :: (Type -> Type) -> Type where
10 RSum :: R f -> R g -> R (f :+: g)
12 class Rep f where
13 rep :: R f
15 instance (Rep f, Rep g) => Rep (f :+: g) where
16 rep = RSum rep rep
18 type family Der (f :: Type -> Type) :: Type -> Type
19 type instance Der (f :+: g) = Der f :+: Der g
21 plug :: Rep f => Der f x -> x -> f x
22 plug = plug' rep where
24 plug' :: R f -> Der f x -> x -> f x
25 plug' (RSum rf rg) (Inl df) x = Inl (plug rf df x)
27 {-
28 rf :: R f1, rg :: R g1
29 Given by GADT match: f ~ f1 :+: g1
31 Second arg has type (Der f x)
32 = (Der (f1:+:g1) x)
33 = (:+:) (Der f1) (Der g1) x
34 Hence df :: Der f1 x
36 Inl {f3,g3,x} (plug {f2,x1} rf df x) gives rise to
37 result of Inl: ((:+:) f3 g3 x ~ f x)
38 first arg (rf): (R f1 ~ Der f2 x1)
39 second arg (df): (Der f1 x ~ x1)
40 result of plug: (f2 x1 ~ x -> f3 x)
42 result of Inl: ((:+:) f3 g3 x ~ f x)
43 by given ((:+:) f3 g3 x ~ (:+:) f1 g1 x)
44 hence need f3~f1, g3~g1
46 So we are left with
47 first arg: (R f1 ~ Der f2 x1)
48 second arg: (Der f1 x ~ x1)
49 result: (f2 x1 ~ (->) x (f3 x))
51 Decompose result:
52 f2 ~ (->) x
53 x1 ~ f1 x
54 Hence
55 first: R f1 ~ Der ((->) x) (f1 x)
56 decompose : R ~ Der ((->) x)
57 f1 ~ f1 x
60 -}