1 -- From the blog post Fun With XPolyKinds : Polykinded Folds

2 -- http://www.typesandotherdistractions.com/2012/02/fun-with-xpolykinds-polykinded-folds.html

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 (* -> *) -> (* -> *)).

15 The following will compile in the new GHC 7.4.1 release. We require

16 the following GHC extensions:

17 -}

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 #-}

30 {- The basic fold and unfold combinators can be written as follows:

32 fold phi = phi . fmap (fold phi) . out

33 unfold psi = in . fmap (unfold psi) . psi

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: -}

40 ident :: hom a a

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.

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.

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 (.) -}

64 {- Another example is the category of type constructors and natural

65 transformations. A natural transformation is defined as follows: -}

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. -}

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: -}

84 {- The class Rec defines two morphisms: _in, which is the constructor of

85 the fixed point type t, and out, its destructor.

87 The final piece is the definition of a higher order functor, which

88 generalizes the typeclass Functor: -}

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.

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: -}

109 -- Now for some examples.

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:

117 -- An instance of Rec shows the relationship between the defining functor

118 -- and the recursive type itself:

126 -- FTree is indeed a functor, so it is also a HFunctor:

132 -- These instances are enough to define folds and unfolds for this

133 -- type. The following fold calculates the depth of a tree:

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:

146 -- FCTree :: (* -> *) -> * -> *

150 -- Again, we define type class instances for HFunctor and Rec:

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:

173 -- And finally, the following fold calculates the depth of a complete binary leaf tree:

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.

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: -}

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:

196 newtype PHom h1 h2 p1 p2 = PHom { runPHom :: forall r. (h1 (p1 Fst) (p2 Fst) -> h2 (p1 Snd) (p2 Snd) -> r) -> r }

202 -- Now, PHom allows us to take two categories and form the product category:

205 ident = mkPHom ident ident

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 -> *:

213 FZero :: FAlt a p Fst

218 Zero :: Alt a Fst

224 -- Again, we need to define instances of Rec and HFunctor:

229 f FZero = Zero

235 f Zero = FZero

241 hf FZero = FZero

245 -- As before, we create a target type for our fold, and this time a type synonym as well:

253 -- At last, here is the fold pairUp, taking even length lists to lists of pairs:

257 where