blob: e6c4dfbb30f4c34ac41adae3c5b6431b81b21969 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
|
{-# LANGUAGE EmptyDataDecls, TypeFamilies, TypeOperators, GADTs, KindSignatures #-}
module T3330c where
data (f :+: g) x = Inl (f x) | Inr (g x)
data R :: (* -> *) -> * where
RSum :: R f -> R g -> R (f :+: g)
class Rep f where
rep :: R f
instance (Rep f, Rep g) => Rep (f :+: g) where
rep = RSum rep rep
type family Der (f :: * -> *) :: * -> *
type instance Der (f :+: g) = Der f :+: Der g
plug :: Rep f => Der f x -> x -> f x
plug = plug' rep where
plug' :: R f -> Der f x -> x -> f x
plug' (RSum rf rg) (Inl df) x = Inl (plug rf df x)
{-
rf :: R f1, rg :: R g1
Given by GADT match: f ~ f1 :+: g1
Second arg has type (Der f x)
= (Der (f1:+:g1) x)
= (:+:) (Der f1) (Der g1) x
Hence df :: Der f1 x
Inl {f3,g3,x} (plug {f2,x1} rf df x) gives rise to
result of Inl: ((:+:) f3 g3 x ~ f x)
first arg (rf): (R f1 ~ Der f2 x1)
second arg (df): (Der f1 x ~ x1)
result of plug: (f2 x1 ~ x -> f3 x)
result of Inl: ((:+:) f3 g3 x ~ f x)
by given ((:+:) f3 g3 x ~ (:+:) f1 g1 x)
hence need f3~f1, g3~g1
So we are left with
first arg: (R f1 ~ Der f2 x1)
second arg: (Der f1 x ~ x1)
result: (f2 x1 ~ (->) x (f3 x))
Decompose result:
f2 ~ (->) x
x1 ~ f1 x
Hence
first: R f1 ~ Der ((->) x) (f1 x)
decompose : R ~ Der ((->) x)
f1 ~ f1 x
-}
|
