Ticket #11523: Categories.hs

File Categories.hs, 7.0 KB (added by ekmett, 4 years ago)

a test case that is still failing after february 8th patches

Line 
1{-# language KindSignatures #-}
2{-# language PolyKinds #-}
3{-# language DataKinds #-}
4{-# language TypeFamilies #-}
5{-# language RankNTypes #-}
6{-# language NoImplicitPrelude #-}
7{-# language FlexibleContexts #-}
8{-# language MultiParamTypeClasses #-}
9{-# language GADTs #-}
10{-# language ConstraintKinds #-}
11{-# language FlexibleInstances #-}
12{-# language TypeOperators #-}
13{-# language ScopedTypeVariables #-}
14{-# language DefaultSignatures #-}
15{-# language FunctionalDependencies #-}
16{-# language UndecidableSuperClasses #-}
17{-# language UndecidableInstances #-}
18{-# language TypeInType #-}
19
20import qualified Data.Type.Coercion as Coercion
21import Data.Type.Coercion (Coercion(..))
22import qualified Data.Type.Equality as Equality
23import Data.Type.Equality ((:~:)(..))
24import GHC.Types (Constraint, Type)
25import qualified Prelude
26import Prelude (Either(..), Maybe, IO)
27
28type Cat i = i -> i -> Type
29
30newtype Y (p :: i -> j -> Type) (a :: j) (b :: i) = Y { getY :: p b a }
31
32class Vacuous (p :: Cat i) (a :: i)
33instance Vacuous p a
34
35data Dict (p :: Constraint) where
36  Dict :: p => Dict p
37
38class (Functor p, Dom p ~ Op p, Cod p ~ Nat p (->), Ob (Op p) ~ Ob p) => Category (p :: Cat i) where
39  type Op p :: Cat i
40  type Op p = Y p
41
42  type Ob p :: i -> Constraint
43  type Ob p = Vacuous p
44
45  id :: Ob p a => p a a
46  (.) :: p b c -> p a b -> p a c
47
48  source :: p a b -> Dict (Ob p a)
49  default source :: (Ob p ~ Vacuous p) => p a b -> Dict (Ob p a)
50  source _ = Dict
51
52  target :: p a b -> Dict (Ob p b)
53  default target :: (Ob p ~ Vacuous p) => p a b -> Dict (Ob p b)
54  target _ = Dict
55
56  op :: p b a -> Op p a b
57  default op :: Op p ~ Y p => p b a -> Op p a b
58  op = Y
59 
60  unop :: Op p b a -> p a b
61  default unop :: Op p ~ Y p => Op p b a -> p a b
62  unop = getY
63
64class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where
65  type Dom f :: Cat i
66  type Cod f :: Cat j
67  fmap :: p a b -> q (f a) (f b)
68
69class (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f | f -> p q
70instance (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f
71
72data Nat (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j) =
73  (FunctorOf p q f, FunctorOf p q g) => Nat { runNat :: forall a. Ob p a => q (f a) (g a) }
74
75instance (Category p, Category q) => Category (Nat p q) where
76  type Ob (Nat p q) = FunctorOf p q
77  id = Nat id1 where
78    id1 :: forall f x. (FunctorOf p q f, Ob p x) => q (f x) (f x)
79    id1 = id \\ (ob :: Ob p x :- Ob q (f x))
80  Nat f . Nat g = Nat (f . g)
81  source Nat{} = Dict
82  target Nat{} = Dict
83
84ob :: forall p q f a. FunctorOf p q f => Ob p a :- Ob q (f a)
85ob = Sub (case source (fmap id :: q (f a) (f a)) of Dict -> Dict)
86
87instance (Category p, Category q) => Functor (Nat p q) where
88  type Dom (Nat p q) = Y (Nat p q)
89  type Cod (Nat p q) = Nat (Nat p q) (->)
90  fmap (Y f) = Nat (. f)
91
92instance (Category p, Category q) => Functor (Nat p q f) where
93  type Dom (Nat p q f) = Nat p q
94  type Cod (Nat p q f) = (->)
95  fmap = (.)
96
97contramap :: Functor f => Op (Dom f) b a -> Cod f (f a) (f b)
98contramap = fmap . unop
99
100instance Category (->) where
101  id = Prelude.id
102  (.) = (Prelude..)
103
104instance Functor ((->) e) where
105  type Dom ((->) e) = (->)
106  type Cod ((->) e) = (->)
107  fmap = (.)
108
109instance Functor (->) where
110  type Dom (->) = Y (->)
111  type Cod (->) = Nat (->) (->)
112  fmap (Y f) = Nat (. f)
113
114instance (Category p, Op p ~ Y p) => Category (Y p) where
115  type Op (Y p) = p
116  type Ob (Y p) = Ob p
117  id = Y id
118  Y f . Y g = Y (g . f)
119  source (Y f) = target f
120  target (Y f) = source f
121  unop = Y
122  op = getY
123
124instance (Category p, Op p ~ Y p) => Functor (Y p a) where
125  type Dom (Y p a) = Y p
126  type Cod (Y p a) = (->)
127  fmap = (.)
128
129instance (Category p, Op p ~ Y p) => Functor (Y p) where
130  type Dom (Y p) = p
131  type Cod (Y p) = Nat (Y p) (->)
132  fmap f = Nat (. Y f)
133
134--------------------------------------------------------------------------------
135-- Type Constraints
136--------------------------------------------------------------------------------
137
138infixl 1 \\ -- comment required for cpp
139(\\) :: a => (b => r) -> (a :- b) -> r
140r \\ Sub Dict = r
141
142newtype p :- q = Sub (p => Dict q)
143
144instance Functor Dict where
145  type Dom Dict = (:-)
146  type Cod Dict = (->)
147  fmap p Dict = case p of
148    Sub q -> q
149
150instance Category (:-) where
151  id = Sub Dict
152  f . g = Sub (Dict \\ f \\ g)
153
154instance Functor ((:-) e) where
155  type Dom ((:-) e) = (:-)
156  type Cod ((:-) e) = (->)
157  fmap = (.)
158
159instance Functor (:-) where
160  type Dom (:-) = Y (:-)
161  type Cod (:-) = Nat (:-) (->)
162  fmap (Y f) = Nat (. f)
163
164--------------------------------------------------------------------------------
165-- * Common Functors
166--------------------------------------------------------------------------------
167
168instance Functor ((,) e) where
169  type Dom ((,) e) = (->)
170  type Cod ((,) e) = (->)
171  fmap f ~(a,b) = (a, f b)
172
173instance Functor (Either e) where
174  type Dom (Either e) = (->)
175  type Cod (Either e) = (->)
176  fmap _ (Left a) = Left a
177  fmap f (Right b) = Right (f b)
178
179instance Functor [] where
180  type Dom [] = (->)
181  type Cod [] = (->)
182  fmap = Prelude.fmap
183
184instance Functor Prelude.Maybe where
185  type Dom Maybe = (->)
186  type Cod Maybe = (->)
187  fmap = Prelude.fmap
188
189instance Functor IO where
190  type Dom IO = (->)
191  type Cod IO = (->)
192  fmap = Prelude.fmap
193
194instance Functor (,) where
195  type Dom (,) = (->)
196  type Cod (,) = Nat (->) (->)
197  fmap f = Nat (\(a,b) -> (f a, b))
198
199instance Functor Either where
200  type Dom Either = (->)
201  type Cod Either = Nat (->) (->)
202  fmap f0 = Nat (go f0) where
203    go :: (a -> b) -> Either a c -> Either b c
204    go f (Left a)  = Left (f a)
205    go _ (Right b) = Right b
206
207--------------------------------------------------------------------------------
208-- * Groupoids
209--------------------------------------------------------------------------------
210
211class Category p => Groupoid p where
212  sym :: p a b -> p b a
213
214instance (Category p, Groupoid q) => Groupoid (Nat p q) where
215  sym f@Nat{} = Nat (sym (runNat f))
216
217--------------------------------------------------------------------------------
218-- * Type Equality
219--------------------------------------------------------------------------------
220
221instance Category (:~:) where
222  type Op (:~:) = (:~:)
223  id = Refl
224  (.) = Prelude.flip Equality.trans
225  op = sym
226  unop = sym
227
228instance Functor (:~:) where
229  type Dom (:~:) = (:~:)
230  type Cod (:~:) = Nat (:~:) (->)
231  fmap f = Nat (. Equality.sym f)
232
233instance Functor ((:~:) e) where
234  type Dom ((:~:) e) = (:~:)
235  type Cod ((:~:) e) = (->)
236  fmap = (.)
237
238instance Groupoid (:~:) where
239  sym = Equality.sym
240
241--------------------------------------------------------------------------------
242-- * Type Coercions
243--------------------------------------------------------------------------------
244
245instance Category Coercion where
246  type Op Coercion = Coercion
247  id = Coercion
248  (.) = Prelude.flip Coercion.trans
249  op   = sym
250  unop = sym
251
252instance Functor Coercion where
253  type Dom Coercion = Coercion
254  type Cod Coercion = Nat Coercion (->)
255  fmap f = Nat (. Coercion.sym f)
256
257instance Functor (Coercion e) where
258  type Dom (Coercion e) = Coercion
259  type Cod (Coercion e) = (->)
260  fmap = (.)
261
262instance Groupoid Coercion where
263  sym = Coercion.sym