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
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module T15703 where
import Data.Kind
import Data.Type.Equality
import GHC.Generics
import T15703_aux
-----
-- The important bits
-----
-- DefaultSignatures-based instances
instance PMonoid a => PApplicative ((,) a)
instance SMonoid a => SApplicative ((,) a)
instance VMonoid a => VApplicative ((,) a)
instance SApplicative f => SApplicative (M1 i c f) where
sPure x = singFun3 @(.@#@$) (%.) @@ singFun1 @M1Sym0 SM1 @@ (singFun1 @PureSym0 sPure) @@ x
-- If I change the implementation of sPure above to be this:
--
-- sPure x = SM1 (sPure x)
--
-- Then T15703.hs compiles quickly again (< 1 second) with -O1.
SM1 f %<*> SM1 x = SM1 (f %<*> x)
-------------------------------------------------------------------------------
type GenericPure :: a -> f a
type family GenericPure (x :: a) :: f a where
GenericPure x = To1 (Pure x)
type GenericPureC (f :: Type -> Type) (x :: a) =
(Pure x :: f a) ~ (GenericPure x :: f a)
type GenericAp :: f (a ~> b) -> f a -> f b
type family (g :: f (a ~> b)) `GenericAp` (x :: f a) :: f b where
g `GenericAp` x = To1 (From1 g <*> From1 x)
type GenericApC (g :: f (a ~> b)) (x :: f a) =
(g <*> x) ~ (g `GenericAp` x)
class PApplicative f where
type Pure (x :: a) :: f a
type Pure x = GenericPure x
type (g :: f (a ~> b)) <*> (x :: f a) :: f b
type g <*> x = g `GenericAp` x
data PureSym0 :: forall f a. a ~> f a
type instance Apply PureSym0 x = Pure x
data (<*>@#@$) :: forall f a b. f (a ~> b) ~> f a ~> f b
type instance Apply (<*>@#@$) g = (<*>@#@$$) g
data (<*>@#@$$) :: forall f a b. f (a ~> b) -> f a ~> f b
type instance Apply ((<*>@#@$$) g) x = g <*> x
class SApplicative f where
sPure :: forall a (x :: a).
Sing x -> Sing (Pure x :: f a)
default sPure :: forall a (x :: a).
( SGeneric1 f, SApplicative (Rep1 f)
, GenericPureC f x )
=> Sing x -> Sing (Pure x :: f a)
sPure = sTo1 . sPure
(%<*>) :: forall a b (g :: f (a ~> b)) (x :: f a).
Sing g -> Sing x -> Sing (g <*> x)
default (%<*>) :: forall a b (g :: f (a ~> b)) (x :: f a).
( SGeneric1 f, SApplicative (Rep1 f)
, GenericApC g x )
=> Sing g -> Sing x -> Sing (g <*> x)
sg %<*> sx = sTo1 (sFrom1 sg %<*> sFrom1 sx)
class (PApplicative f, SApplicative f) => VApplicative f where
applicativeHomomorphism :: forall a b (g :: a ~> b) (x :: a).
Sing g -> Sing x
-> (Pure g <*> Pure x) :~: (Pure (g `Apply` x) :: f b)
default applicativeHomomorphism :: forall a b (g :: a ~> b) (x :: a).
( VGeneric1 f, VApplicative (Rep1 f)
, GenericPureC f g, GenericPureC f x, GenericPureC f (g `Apply` x)
, GenericApC (Pure g :: f (a ~> b)) (Pure x :: f a)
)
=> Sing g -> Sing x
-> (Pure g <*> Pure x) :~: (Pure (g `Apply` x) :: f b)
applicativeHomomorphism sg sx
| Refl <- sFot1 @Type @f (sPure sg)
, Refl <- sFot1 @Type @f (sPure sx)
, Refl <- applicativeHomomorphism @(Rep1 f) sg sx
, Refl <- sFot1 @Type @f pureGX
, Refl <- sTof1 @Type @f (sTo1 pureGX)
= Refl
where
pureGX :: Sing (Pure (Apply g x) :: Rep1 f b)
pureGX = sPure (sg @@ sx)
instance PApplicative (K1 i c) where
type Pure _ = 'K1 Mempty
type 'K1 x <*> 'K1 y = 'K1 (x <> y)
instance SMonoid c => SApplicative (K1 i c) where
sPure _ = SK1 sMempty
SK1 x %<*> SK1 y = SK1 (x %<> y)
instance VMonoid c => VApplicative (K1 i c) where
applicativeHomomorphism _ _ | Refl <- monoidLeftIdentity (sMempty @c) = Refl
instance PApplicative (M1 i c f) where
type Pure x = 'M1 (Pure x)
type 'M1 ff <*> 'M1 x = 'M1 (ff <*> x)
instance VApplicative f => VApplicative (M1 i c f) where
applicativeHomomorphism sg sx
| Refl <- applicativeHomomorphism @f sg sx
= Refl
instance PApplicative (f :*: g) where
type Pure a = Pure a ':*: Pure a
type (ff ':*: gg) <*> (x ':*: y) = (ff <*> x) ':*: (gg <*> y)
instance (SApplicative f, SApplicative g) => SApplicative (f :*: g) where
sPure a = sPure a :%*: sPure a
(f :%*: g) %<*> (x :%*: y) = (f %<*> x) :%*: (g %<*> y)
instance (VApplicative f, VApplicative g) => VApplicative (f :*: g) where
applicativeHomomorphism sg sx
| Refl <- applicativeHomomorphism @f sg sx
, Refl <- applicativeHomomorphism @g sg sx
= Refl
instance PApplicative Par1 where
type Pure x = 'Par1 x
type 'Par1 f <*> 'Par1 x = 'Par1 (f @@ x)
instance SApplicative Par1 where
sPure = SPar1
SPar1 f %<*> SPar1 x = SPar1 (f @@ x)
instance VApplicative Par1 where
applicativeHomomorphism _ _ = Refl
|
