summaryrefslogtreecommitdiff
path: root/testsuite/tests/polykinds/Freeman.hs
diff options
context:
space:
mode:
authorSimon Peyton Jones <simonpj@microsoft.com>2012-03-02 16:35:42 +0000
committerSimon Peyton Jones <simonpj@microsoft.com>2012-03-02 16:35:42 +0000
commit64880bb7693ca9a97e26a292b5d3fe402f72c143 (patch)
tree87885e83aab4d79fdc15922eba28ea0e63f622c1 /testsuite/tests/polykinds/Freeman.hs
parent7a29e7e2e17b47360adfca59d049b77f8ec3f0f7 (diff)
downloadhaskell-64880bb7693ca9a97e26a292b5d3fe402f72c143.tar.gz
Modified error output and new tests for PolyKinds commit
Diffstat (limited to 'testsuite/tests/polykinds/Freeman.hs')
-rw-r--r--testsuite/tests/polykinds/Freeman.hs259
1 files changed, 259 insertions, 0 deletions
diff --git a/testsuite/tests/polykinds/Freeman.hs b/testsuite/tests/polykinds/Freeman.hs
new file mode 100644
index 0000000000..ea8aff0f8a
--- /dev/null
+++ b/testsuite/tests/polykinds/Freeman.hs
@@ -0,0 +1,259 @@
+-- From the blog post Fun With XPolyKinds : Polykinded Folds
+-- http://www.typesandotherdistractions.com/2012/02/fun-with-xpolykinds-polykinded-folds.html
+
+{-
+In the following, I will write a polykinded version of the combinators
+fold and unfold, along with three examples: folds for regular
+datatypes (specialized to kind *), folds for nested datatypes
+(specialized to kind * -> *), and folds for mutually recursive data
+types (specialized to the product kind (*,*)). The approach should
+generalise easily enough to things such as types indexed by another
+kind (e.g. by specializing to kind Nat -> *, using the XDataKinds
+extension), or higher order nested datatypes (e.g. by specializing to
+kind (* -> *) -> (* -> *)).
+
+The following will compile in the new GHC 7.4.1 release. We require
+the following GHC extensions:
+-}
+
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+module Main where
+
+{- The basic fold and unfold combinators can be written as follows:
+
+fold phi = phi . fmap (fold phi) . out
+unfold psi = in . fmap (unfold psi) . psi
+
+The idea now is to generalize these combinators by working over
+different categories. We can capture the basic operations in a
+category with a typeclass: -}
+
+class Category hom where
+ ident :: hom a a
+ compose :: hom a b -> hom b c -> hom a c
+
+{- A category has two operations: an identity morphism for every
+object, and for every two compatible morphisms, the composition of
+those morphisms.
+
+In earlier versions of GHC, the type hom would have been specialized
+to kind * -> * -> *, but with the new PolyKinds extension, hom is
+polykinded, and the Category typeclass can be instantiated to k -> k
+-> * for any kind k. This means that in addition to all of the
+Category instances that we could have written before, we can now write
+instances of Category for type constructors, type constructor
+constructors, etc.
+
+Here is the instance for the category Hask of Haskell types. Objects
+are Haskell types and morphisms are functions between types. The
+identity is the regular polymorphic identity function id, and
+composition is given by the (flipped) composition operator (.) -}
+
+instance Category (->) where
+ ident = id
+ compose = flip (.)
+
+{- Another example is the category of type constructors and natural
+transformations. A natural transformation is defined as follows: -}
+
+newtype Nat f g = Nat { nu :: (forall a. f a -> g a) }
+
+{- Here is the Category instance for natural transformations. This
+time the type hom is inferred to have kind (* -> *) -> (* -> *) ->
+*. Identity and composition are both defined pointwise. -}
+
+instance Category (Nat :: (* -> *) -> (* -> *) -> *) where
+ ident = Nat id
+ compose f g = Nat (nu g . nu f)
+
+{- Let's define a type class which will capture the idea of a fixed point
+in a category. This generalizes the idea of recursive types in Hask: -}
+
+class Rec hom f t where
+ _in :: hom (f t) t
+ out :: hom t (f t)
+
+{- The class Rec defines two morphisms: _in, which is the constructor of
+the fixed point type t, and out, its destructor.
+
+The final piece is the definition of a higher order functor, which
+generalizes the typeclass Functor: -}
+
+class HFunctor hom f where
+ hmap :: hom a b -> hom (f a) (f b)
+
+{- Note the similarity with the type signature of the function fmap ::
+(Functor f) => (a -> b) -> f a -> f b. Indeed, specializing hom to
+(->) in the definition of HFunctor gives back the type signature of
+fmap.
+
+Finally, we can define folds and unfolds in a category. The
+definitions are as before, but with explicit composition, constructors
+and destructors replaced with the equivalent type class methods, and
+hmap in place of fmap: -}
+
+fold :: (Category hom, HFunctor hom f, Rec hom f rec) => hom (f t) t -> hom rec t
+fold phi = compose out (compose (hmap (fold phi)) phi)
+
+unfold :: (Category hom, HFunctor hom f, Rec hom f rec) => hom t (f t) -> hom t rec
+unfold phi = compose phi (compose (hmap (unfold phi)) _in)
+
+-- Now for some examples.
+
+-- The first example is a regular recursive datatype of binary leaf
+-- trees. The functor FTree is the base functor of this recursive type:
+
+data FTree a b = FLeaf a | FBranch b b
+data Tree a = Leaf a | Branch (Tree a) (Tree a)
+
+-- An instance of Rec shows the relationship between the defining functor
+-- and the recursive type itself:
+
+instance Rec (->) (FTree a) (Tree a) where
+ _in (FLeaf a) = Leaf a
+ _in (FBranch a b) = Branch a b
+ out (Leaf a) = FLeaf a
+ out (Branch a b) = FBranch a b
+
+-- FTree is indeed a functor, so it is also a HFunctor:
+
+instance HFunctor (->) (FTree a) where
+ hmap f (FLeaf a) = FLeaf a
+ hmap f (FBranch a b) = FBranch (f a) (f b)
+
+-- These instances are enough to define folds and unfolds for this
+-- type. The following fold calculates the depth of a tree:
+
+depth :: Tree a -> Int
+depth = (fold :: (FTree a Int -> Int) -> Tree a -> Int) phi where
+ phi :: FTree a Int -> Int
+ phi (FLeaf a) = 1
+ phi (FBranch a b) = 1 + max a b
+
+-- The second example is a fold for the nested (or non-regular)
+-- datatype of complete binary leaf trees. The higher order functor
+-- FCTree defines the type constructor CTree as its fixed point:
+
+data FCTree f a = FCLeaf a | FCBranch (f (a, a))
+ -- FCTree :: (* -> *) -> * -> *
+
+data CTree a = CLeaf a | CBranch (CTree (a, a))
+
+-- Again, we define type class instances for HFunctor and Rec:
+
+instance HFunctor Nat FCTree where
+ hmap (f :: Nat (f :: * -> *) (g :: * -> *)) = Nat ff where
+ ff :: forall a. FCTree f a -> FCTree g a
+ ff (FCLeaf a) = FCLeaf a
+ ff (FCBranch a) = FCBranch (nu f a)
+
+instance Rec Nat FCTree CTree where
+ _in = Nat inComplete where
+ inComplete (FCLeaf a) = CLeaf a
+ inComplete (FCBranch a) = CBranch a
+ out = Nat outComplete where
+ outComplete(CLeaf a) = FCLeaf a
+ outComplete(CBranch a) = FCBranch a
+
+-- Morphisms between type constructors are natural transformations, so we
+-- need a type constructor to act as the target of the fold. For our
+-- purposes, a constant functor will do:
+
+data K a b = K a -- K :: forall k. * -> k -> *
+
+
+-- And finally, the following fold calculates the depth of a complete binary leaf tree:
+
+cdepth :: CTree a -> Int
+cdepth c = let (K d) = nu (fold (Nat phi)) c in d where
+ phi :: FCTree (K Int) a -> K Int a
+ phi (FCLeaf a) = K 1
+ phi (FCBranch (K n)) = K (n + 1)
+
+{- The final example is a fold for the pair of mutually recursive
+datatype of lists of even and odd lengths. The fold will take a list
+of even length and produce a list of pairs.
+
+We cannot express type constructors in Haskell whose return kind is
+anything other than *, so we cheat a little and emulate the product
+kind using an arrow kind Choice -> *, where Choice is a two point
+kind, lifted using the XDataKinds extension: -}
+
+data Choice = Fst | Snd
+
+-- A morphism of pairs of types is just a pair of morphisms. For
+-- technical reasons, we represent this using a Church-style encoding,
+-- along with helper methods, as follows:
+
+newtype PHom h1 h2 p1 p2 = PHom { runPHom :: forall r. (h1 (p1 Fst) (p2 Fst) -> h2 (p1 Snd) (p2 Snd) -> r) -> r }
+
+mkPHom f g = PHom (\h -> h f g)
+fstPHom p = runPHom p (\f -> \g -> f)
+sndPHom p = runPHom p (\f -> \g -> g)
+
+-- Now, PHom allows us to take two categories and form the product category:
+
+instance (Category h1, Category h2) => Category (PHom h1 h2) where
+ ident = mkPHom ident ident
+ compose p1 p2 = mkPHom (compose (fstPHom p1) (fstPHom p2)) (compose (sndPHom p1) (sndPHom p2))
+
+-- We can define the types of lists of even and odd length as
+-- follows. Note that the kind annotation indicates the appearance of the
+-- kind Choice -> *:
+
+data FAlt :: * -> (Choice -> *) -> Choice -> * where
+ FZero :: FAlt a p Fst
+ FSucc1 :: a -> (p Snd) -> FAlt a p Fst
+ FSucc2 :: a -> (p Fst) -> FAlt a p Snd
+
+data Alt :: * -> Choice -> * where
+ Zero :: Alt a Fst
+ Succ1 :: a -> Alt a Snd -> Alt a Fst
+ Succ2 :: a -> Alt a Fst -> Alt a Snd
+
+deriving instance Show a => Show (Alt a b)
+
+-- Again, we need to define instances of Rec and HFunctor:
+
+instance Rec (PHom (->) (->)) (FAlt a) (Alt a) where
+ _in = mkPHom f g where
+ f FZero = Zero
+ f (FSucc1 a b) = Succ1 a b
+ g (FSucc2 a b) = Succ2 a b
+ out = mkPHom f g where
+ f Zero = FZero
+ f (Succ1 a b) = FSucc1 a b
+ g (Succ2 a b) = FSucc2 a b
+
+instance HFunctor (PHom (->) (->)) (FAlt a) where
+ hmap p = mkPHom hf hg where
+ hf FZero = FZero
+ hf (FSucc1 a x) = FSucc1 a (sndPHom p x)
+ hg (FSucc2 a x) = FSucc2 a (fstPHom p x)
+
+-- As before, we create a target type for our fold, and this time a type synonym as well:
+
+data K2 :: * -> * -> Choice -> * where
+ K21 :: a -> K2 a b Fst
+ K22 :: b -> K2 a b Snd
+
+type PairUpResult a = K2 [(a, a)] (a, [(a, a)])
+
+-- At last, here is the fold pairUp, taking even length lists to lists of pairs:
+
+pairUp :: Alt a Fst -> [(a, a)]
+pairUp xs = let (K21 xss) = (fstPHom (fold (mkPHom phi psi))) xs in xss
+ where
+ phi FZero = K21 []
+ phi (FSucc1 x1 (K22 (x2, xss))) = K21 ((x1, x2):xss)
+ psi (FSucc2 x (K21 xss)) = K22 (x, xss)
+
+main = print (Succ1 (0::Int) $ Succ2 1 $ Succ1 2 $ Succ2 3 $ Succ1 4 $ Succ2 5 Zero)