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
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
|
{-# language KindSignatures #-}
{-# language PolyKinds #-}
{-# language DataKinds #-}
{-# language TypeFamilies #-}
{-# language RankNTypes #-}
{-# language NoImplicitPrelude #-}
{-# language FlexibleContexts #-}
{-# language MultiParamTypeClasses #-}
{-# language GADTs #-}
{-# language ConstraintKinds #-}
{-# language FlexibleInstances #-}
{-# language TypeOperators #-}
{-# language ScopedTypeVariables #-}
{-# language DefaultSignatures #-}
{-# language FunctionalDependencies #-}
{-# language UndecidableSuperClasses #-}
-- This code, supplied by Edward Kmett, uses UndecidableSuperClasses along
-- with a bunch of other stuff, so it's a useful stress test.
-- See #11480 comment:12.
module T11480b where
import Data.Kind (Constraint, Type)
import Data.Type.Equality as Equality
import Data.Type.Coercion as Coercion
import qualified Prelude
import Prelude (Either(..))
newtype Y (p :: i -> j -> Type) (a :: j) (b :: i) = Y { getY :: p b a }
type family Op (p :: i -> j -> Type) :: j -> i -> Type where
Op (Y p) = p
Op p = Y p
class Vacuous (p :: i -> i -> Type) (a :: i)
instance Vacuous p a
data Dict (p :: Constraint) where
Dict :: p => Dict p
class Functor (Op p) (Nat p (->)) p => Category (p :: i -> i -> Type) where
type Ob p :: i -> Constraint
type Ob p = Vacuous p
id :: Ob p a => p a a
(.) :: p b c -> p a b -> p a c
source :: p a b -> Dict (Ob p a)
default source :: (Ob p ~ Vacuous p) => p a b -> Dict (Ob p a)
source _ = Dict
target :: p a b -> Dict (Ob p b)
default target :: (Ob p ~ Vacuous p) => p a b -> Dict (Ob p b)
target _ = Dict
op :: p b a -> Op p a b
default op :: Op p ~ Y p => p b a -> Op p a b
op = Y
unop :: Op p b a -> p a b
default unop :: Op p ~ Y p => Op p b a -> p a b
unop = getY
class (Category p, Category q) =>
Functor (p :: i -> i -> Type)
(q :: j -> j -> Type)
(f :: i -> j) | f -> p q where
fmap :: p a b -> q (f a) (f b)
data Nat (p :: i -> i -> Type)
(q :: j -> j -> Type) (f :: i -> j) (g :: i -> j) where
Nat :: (Functor p q f, Functor p q g) =>
{ runNat :: forall a. Ob p a => q (f a) (g a) } -> Nat p q f g
instance (Category p, Category q) => Category (Nat p q) where
type Ob (Nat p q) = Functor p q
id = Nat id1 where
id1 :: forall f x. (Functor p q f, Ob p x) => q (f x) (f x)
id1 = id \\ (ob :: Ob p x :- Ob q (f x))
Nat f . Nat g = Nat (f . g)
source Nat{} = Dict
target Nat{} = Dict
ob :: forall p q f a. Functor p q f => Ob p a :- Ob q (f a)
ob = Sub (case source (fmap (id :: p a a) :: q (f a) (f a)) of Dict -> Dict)
instance (Category p, Category q) =>
Functor (Y (Nat p q)) (Nat (Nat p q) (->)) (Nat p q) where
fmap (Y f) = Nat (. f)
instance (Category p, Category q) => Functor (Nat p q) (->) (Nat p q f) where
fmap = (.)
contramap :: Functor p q f => Op p b a -> q (f a) (f b)
contramap = fmap . unop
instance Category (->) where
id = Prelude.id
(.) = (Prelude..)
instance Functor (->) (->) ((->) e) where
fmap = (.)
instance Functor (Y (->)) (Nat (->) (->)) (->) where
fmap (Y f) = Nat (. f)
instance (Category p, Op p ~ Y p) => Category (Y p) where
type Ob (Y p) = Ob p
id = Y id
Y f . Y g = Y (g . f)
source (Y f) = target f
target (Y f) = source f
unop = Y
op = getY
instance (Category p, Op p ~ Y p) => Functor (Y p) (->) (Y p a) where
fmap = (.)
instance (Category p, Op p ~ Y p) => Functor p (Nat (Y p) (->)) (Y p) where
fmap f = Nat (. Y f)
--------------------------------------------------------------------------------
-- * Constraints
--------------------------------------------------------------------------------
infixl 1 \\ -- comment required for cpp
(\\) :: a => (b => r) -> (a :- b) -> r
r \\ Sub Dict = r
newtype p :- q = Sub (p => Dict q)
instance Functor (:-) (->) Dict where
fmap p Dict = case p of
Sub q -> q
instance Category (:-) where
id = Sub Dict
f . g = Sub (Dict \\ f \\ g)
instance Functor (:-) (->) ((:-) e) where
fmap = (.)
instance Functor (Y (:-)) (Nat (:-) (->)) (:-) where
fmap (Y f) = Nat (. f)
--------------------------------------------------------------------------------
-- * Common Functors
--------------------------------------------------------------------------------
instance Functor (->) (->) ((,) e) where
fmap f ~(a,b) = (a, f b)
instance Functor (->) (->) (Either e) where
fmap _ (Left a) = Left a
fmap f (Right b) = Right (f b)
instance Functor (->) (->) [] where
fmap = Prelude.fmap
instance Functor (->) (->) Prelude.Maybe where
fmap = Prelude.fmap
instance Functor (->) (->) Prelude.IO where
fmap = Prelude.fmap
instance Functor (->) (Nat (->) (->)) (,) where
fmap f = Nat (\(a,b) -> (f a, b))
instance Functor (->) (Nat (->) (->)) Either where
fmap f0 = Nat (go f0) where
go :: (a -> b) -> Either a c -> Either b c
go f (Left a) = Left (f a)
go _ (Right b) = Right b
--------------------------------------------------------------------------------
-- * Type Equality
--------------------------------------------------------------------------------
instance Category (:~:) where
id = Refl
(.) = Prelude.flip Equality.trans
instance Functor (Y (:~:)) (Nat (:~:) (->)) (:~:) where
fmap (Y f) = Nat (. f)
instance Functor (:~:) (->) ((:~:) e) where
fmap = (.)
--------------------------------------------------------------------------------
-- * Type Coercions
--------------------------------------------------------------------------------
instance Category Coercion where
id = Coercion
(.) = Prelude.flip Coercion.trans
instance Functor (Y Coercion) (Nat Coercion (->)) Coercion where
fmap (Y f) = Nat (. f)
instance Functor Coercion (->) (Coercion e) where
fmap = (.)
|
