Remove the type-checking knot.
[ghc.git] / testsuite / tests / polykinds / Freeman.hs
1 -- From the blog post Fun With XPolyKinds : Polykinded Folds
2 -- http://www.typesandotherdistractions.com/2012/02/fun-with-xpolykinds-polykinded-folds.html
3
4 {-
5 In the following, I will write a polykinded version of the combinators
6 fold and unfold, along with three examples: folds for regular
7 datatypes (specialized to kind *), folds for nested datatypes
8 (specialized to kind * -> *), and folds for mutually recursive data
9 types (specialized to the product kind (*,*)). The approach should
10 generalise easily enough to things such as types indexed by another
11 kind (e.g. by specializing to kind Nat -> *, using the XDataKinds
12 extension), or higher order nested datatypes (e.g. by specializing to
13 kind (* -> *) -> (* -> *)).
14
15 The following will compile in the new GHC 7.4.1 release. We require
16 the following GHC extensions:
17 -}
18
19 {-# LANGUAGE GADTs #-}
20 {-# LANGUAGE PolyKinds #-}
21 {-# LANGUAGE KindSignatures #-}
22 {-# LANGUAGE DataKinds #-}
23 {-# LANGUAGE RankNTypes #-}
24 {-# LANGUAGE FlexibleInstances #-}
25 {-# LANGUAGE MultiParamTypeClasses #-}
26 {-# LANGUAGE ScopedTypeVariables #-}
27 {-# LANGUAGE StandaloneDeriving #-}
28 module Main where
29
30 {- The basic fold and unfold combinators can be written as follows:
31
32 fold phi = phi . fmap (fold phi) . out
33 unfold psi = in . fmap (unfold psi) . psi
34
35 The idea now is to generalize these combinators by working over
36 different categories. We can capture the basic operations in a
37 category with a typeclass: -}
38
39 class Category hom where
40 ident :: hom a a
41 compose :: hom a b -> hom b c -> hom a c
42
43 {- A category has two operations: an identity morphism for every
44 object, and for every two compatible morphisms, the composition of
45 those morphisms.
46
47 In earlier versions of GHC, the type hom would have been specialized
48 to kind * -> * -> *, but with the new PolyKinds extension, hom is
49 polykinded, and the Category typeclass can be instantiated to k -> k
50 -> * for any kind k. This means that in addition to all of the
51 Category instances that we could have written before, we can now write
52 instances of Category for type constructors, type constructor
53 constructors, etc.
54
55 Here is the instance for the category Hask of Haskell types. Objects
56 are Haskell types and morphisms are functions between types. The
57 identity is the regular polymorphic identity function id, and
58 composition is given by the (flipped) composition operator (.) -}
59
60 instance Category (->) where
61 ident = id
62 compose = flip (.)
63
64 {- Another example is the category of type constructors and natural
65 transformations. A natural transformation is defined as follows: -}
66
67 newtype Nat f g = Nat { nu :: (forall a. f a -> g a) }
68
69 {- Here is the Category instance for natural transformations. This
70 time the type hom is inferred to have kind (* -> *) -> (* -> *) ->
71 *. Identity and composition are both defined pointwise. -}
72
73 instance Category (Nat :: (* -> *) -> (* -> *) -> *) where
74 ident = Nat id
75 compose f g = Nat (nu g . nu f)
76
77 {- Let's define a type class which will capture the idea of a fixed point
78 in a category. This generalizes the idea of recursive types in Hask: -}
79
80 class Rec hom f t where
81 _in :: hom (f t) t
82 out :: hom t (f t)
83
84 {- The class Rec defines two morphisms: _in, which is the constructor of
85 the fixed point type t, and out, its destructor.
86
87 The final piece is the definition of a higher order functor, which
88 generalizes the typeclass Functor: -}
89
90 class HFunctor hom f where
91 hmap :: hom a b -> hom (f a) (f b)
92
93 {- Note the similarity with the type signature of the function fmap ::
94 (Functor f) => (a -> b) -> f a -> f b. Indeed, specializing hom to
95 (->) in the definition of HFunctor gives back the type signature of
96 fmap.
97
98 Finally, we can define folds and unfolds in a category. The
99 definitions are as before, but with explicit composition, constructors
100 and destructors replaced with the equivalent type class methods, and
101 hmap in place of fmap: -}
102
103 fold :: (Category hom, HFunctor hom f, Rec hom f rec) => hom (f t) t -> hom rec t
104 fold phi = compose out (compose (hmap (fold phi)) phi)
105
106 unfold :: (Category hom, HFunctor hom f, Rec hom f rec) => hom t (f t) -> hom t rec
107 unfold phi = compose phi (compose (hmap (unfold phi)) _in)
108
109 -- Now for some examples.
110
111 -- The first example is a regular recursive datatype of binary leaf
112 -- trees. The functor FTree is the base functor of this recursive type:
113
114 data FTree a b = FLeaf a | FBranch b b
115 data Tree a = Leaf a | Branch (Tree a) (Tree a)
116
117 -- An instance of Rec shows the relationship between the defining functor
118 -- and the recursive type itself:
119
120 instance Rec (->) (FTree a) (Tree a) where
121 _in (FLeaf a) = Leaf a
122 _in (FBranch a b) = Branch a b
123 out (Leaf a) = FLeaf a
124 out (Branch a b) = FBranch a b
125
126 -- FTree is indeed a functor, so it is also a HFunctor:
127
128 instance HFunctor (->) (FTree a) where
129 hmap f (FLeaf a) = FLeaf a
130 hmap f (FBranch a b) = FBranch (f a) (f b)
131
132 -- These instances are enough to define folds and unfolds for this
133 -- type. The following fold calculates the depth of a tree:
134
135 depth :: Tree a -> Int
136 depth = (fold :: (FTree a Int -> Int) -> Tree a -> Int) phi where
137 phi :: FTree a Int -> Int
138 phi (FLeaf a) = 1
139 phi (FBranch a b) = 1 + max a b
140
141 -- The second example is a fold for the nested (or non-regular)
142 -- datatype of complete binary leaf trees. The higher order functor
143 -- FCTree defines the type constructor CTree as its fixed point:
144
145 data FCTree f a = FCLeaf a | FCBranch (f (a, a))
146 -- FCTree :: (* -> *) -> * -> *
147
148 data CTree a = CLeaf a | CBranch (CTree (a, a))
149
150 -- Again, we define type class instances for HFunctor and Rec:
151
152 instance HFunctor Nat FCTree where
153 hmap (f :: Nat (f :: * -> *) (g :: * -> *)) = Nat ff where
154 ff :: forall a. FCTree f a -> FCTree g a
155 ff (FCLeaf a) = FCLeaf a
156 ff (FCBranch a) = FCBranch (nu f a)
157
158 instance Rec Nat FCTree CTree where
159 _in = Nat inComplete where
160 inComplete (FCLeaf a) = CLeaf a
161 inComplete (FCBranch a) = CBranch a
162 out = Nat outComplete where
163 outComplete(CLeaf a) = FCLeaf a
164 outComplete(CBranch a) = FCBranch a
165
166 -- Morphisms between type constructors are natural transformations, so we
167 -- need a type constructor to act as the target of the fold. For our
168 -- purposes, a constant functor will do:
169
170 data K a b = K a -- K :: forall k. * -> k -> *
171
172
173 -- And finally, the following fold calculates the depth of a complete binary leaf tree:
174
175 cdepth :: CTree a -> Int
176 cdepth c = let (K d) = nu (fold (Nat phi)) c in d where
177 phi :: FCTree (K Int) a -> K Int a
178 phi (FCLeaf a) = K 1
179 phi (FCBranch (K n)) = K (n + 1)
180
181 {- The final example is a fold for the pair of mutually recursive
182 datatype of lists of even and odd lengths. The fold will take a list
183 of even length and produce a list of pairs.
184
185 We cannot express type constructors in Haskell whose return kind is
186 anything other than *, so we cheat a little and emulate the product
187 kind using an arrow kind Choice -> *, where Choice is a two point
188 kind, lifted using the XDataKinds extension: -}
189
190 data Choice = Fst | Snd
191
192 -- A morphism of pairs of types is just a pair of morphisms. For
193 -- technical reasons, we represent this using a Church-style encoding,
194 -- along with helper methods, as follows:
195
196 newtype PHom h1 h2 p1 p2 = PHom { runPHom :: forall r. (h1 (p1 Fst) (p2 Fst) -> h2 (p1 Snd) (p2 Snd) -> r) -> r }
197
198 mkPHom f g = PHom (\h -> h f g)
199 fstPHom p = runPHom p (\f -> \g -> f)
200 sndPHom p = runPHom p (\f -> \g -> g)
201
202 -- Now, PHom allows us to take two categories and form the product category:
203
204 instance (Category h1, Category h2) => Category (PHom h1 h2) where
205 ident = mkPHom ident ident
206 compose p1 p2 = mkPHom (compose (fstPHom p1) (fstPHom p2)) (compose (sndPHom p1) (sndPHom p2))
207
208 -- We can define the types of lists of even and odd length as
209 -- follows. Note that the kind annotation indicates the appearance of the
210 -- kind Choice -> *:
211
212 data FAlt :: * -> (Choice -> *) -> Choice -> * where
213 FZero :: FAlt a p Fst
214 FSucc1 :: a -> (p Snd) -> FAlt a p Fst
215 FSucc2 :: a -> (p Fst) -> FAlt a p Snd
216
217 data Alt :: * -> Choice -> * where
218 Zero :: Alt a Fst
219 Succ1 :: a -> Alt a Snd -> Alt a Fst
220 Succ2 :: a -> Alt a Fst -> Alt a Snd
221
222 deriving instance Show a => Show (Alt a b)
223
224 -- Again, we need to define instances of Rec and HFunctor:
225
226 instance Rec (PHom (->) (->)) (FAlt a) (Alt a) where
227 _in = mkPHom f g where
228 f,g :: FAlt a (Alt a) s -> Alt a s
229 f FZero = Zero
230 f (FSucc1 a b) = Succ1 a b
231 g (FSucc2 a b) = Succ2 a b
232
233 out = mkPHom f g where
234 f,g :: Alt a s -> FAlt a (Alt a) s
235 f Zero = FZero
236 f (Succ1 a b) = FSucc1 a b
237 g (Succ2 a b) = FSucc2 a b
238
239 instance HFunctor (PHom (->) (->)) (FAlt a) where
240 hmap p = mkPHom hf hg where
241 hf FZero = FZero
242 hf (FSucc1 a x) = FSucc1 a (sndPHom p x)
243 hg (FSucc2 a x) = FSucc2 a (fstPHom p x)
244
245 -- As before, we create a target type for our fold, and this time a type synonym as well:
246
247 data K2 :: * -> * -> Choice -> * where
248 K21 :: a -> K2 a b Fst
249 K22 :: b -> K2 a b Snd
250
251 type PairUpResult a = K2 [(a, a)] (a, [(a, a)])
252
253 -- At last, here is the fold pairUp, taking even length lists to lists of pairs:
254
255 pairUp :: Alt a Fst -> [(a, a)]
256 pairUp xs = let (K21 xss) = (fstPHom (fold (mkPHom phi psi))) xs in xss
257 where
258 phi :: FAlt y (K2 v (r,[(y,r)])) s -> K2 [(y,r)] (y,z) s
259 phi FZero = K21 []
260 phi (FSucc1 x1 (K22 (x2, xss))) = K21 ((x1, x2):xss)
261
262 psi :: FAlt y (K2 z w) s -> K2 [x] (y,z) s
263 psi (FSucc2 x (K21 xss)) = K22 (x, xss)
264
265 main = print (Succ1 (0::Int) $ Succ2 1 $ Succ1 2 $ Succ2 3 $ Succ1 4 $ Succ2 5 Zero)