2 -----------------------------------------------------------------------------
4 -- Module : Generics.Pointless.Functors
5 -- Copyright : (c) 2008 University of Minho
8 -- Maintainer : hpacheco@di.uminho.pt
9 -- Stability : experimental
10 -- Portability : non-portable
13 -- point-free programming with recursion patterns as hylomorphisms
15 -- This module defines data types as fixed points of functor.
16 -- Pointless Haskell works on a view of data types as fixed points of functors, in the same style as the PolyP (<http://www.cse.chalmers.se/~patrikj/poly/polyp/>) library.
17 -- Instead of using an explicit fixpoint operator, a type function is used to relate the data types with their equivalent functor representations.
19 -----------------------------------------------------------------------------
21 module Generics.Pointless.Functors where
23 import Generics.Pointless.Combinators
24 import Prelude hiding (Functor(..))
28 -- ** Definition and operations over functors
30 -- | Identity functor.
31 newtype Id x = Id {unId :: x}
33 -- | Constant functor.
34 newtype Const t x = Const {unConst :: t}
38 data (g :+: h) x = Inl (g x) | Inr (h x)
40 -- | Product of functors.
42 data (g :*: h) x = g x :*: h x
44 -- | Composition of functors.
46 newtype (g :@: h) x = Comp {unComp :: g (h x)}
48 -- | Explicit fixpoint operator.
49 newtype Fix f = Fix { -- | The unfolding of the fixpoint of a functor is a the functor applied to its fixpoint.
51 -- 'unFix' is specialized with the application of 'Rep' in order to subsume functor application
52 unFix :: Rep f (Fix f)
55 instance Show (Rep f (Fix f)) => Show (Fix f) where
56 show (Fix f) = "(Fix " ++ show f ++ ")"
58 -- | Family of patterns functors of data types.
60 -- The type function is not necessarily injective, this is, different data types can have the same base functor.
61 type family PF a :: * -> *
62 -- ^ Semantically, we can say that @a = 'Fix' f@.
64 type instance PF (Fix f) = f
65 -- ^ The pattern functor of the fixpoint of a functor is the functor itself.
67 -- | Family of functor representations.
69 -- The 'Rep' family implements the implicit coercion between the application of a functor and the structurally equivalent sum of products.
70 type family Rep (f :: * -> *) x :: *
71 -- ^ Functors applied to types can be represented as sums of products.
73 type instance Rep Id x = x
74 -- ^ The identity functor applied to some type is the type itself.
76 type instance Rep (Const t) x = t
77 -- ^ The constant functor applied to some type is the type parameterized by the functor.
79 type instance Rep (g :+: h) x = Rep g x `Either` Rep h x
80 -- ^ The application of a sum of functors to some type is the sum of applying the functors to the argument type.
82 type instance Rep (g :*: h) x = (Rep g x,Rep h x)
83 -- ^ The application of a product of functors to some type is the product of applying the functors to the argument type.
85 type instance Rep (g :@: h) x = Rep g (Rep h x)
86 -- ^ The application of a composition of functors to some type is the nested application of the functors to the argument type.
88 -- This particular instance requires that nexted type function application is enabled as a type system extension.
90 type instance Rep [] x = [x]
91 -- ^ The application of the list functor to some type returns a list of the argument type.
93 -- | Polytypic 'Prelude.Functor' class for functor representations
94 class Functor (f :: * -> *) where
95 fmap :: Fix f -- ^ For desambiguation purposes, the type of the functor must be passed as an explicit paramaeter to 'fmap'
96 -> (x -> y) -> Rep f x -> Rep f y -- ^ The mapping over representations
98 instance Functor Id where
100 -- ^ The identity functor applies the mapping function the argument type
102 instance Functor (Const t) where
104 -- ^ The constant functor preserves the argument type
106 instance (Functor g,Functor h) => Functor (g :+: h) where
107 fmap _ f (Left x) = Left (fmap (_L :: Fix g) f x)
108 fmap _ f (Right x) = Right (fmap (_L :: Fix h) f x)
109 -- ^ The sum functor recursively applies the mapping function to each alternative
111 instance (Functor g,Functor h) => Functor (g :*: h) where
112 fmap _ f (x,y) = (fmap (_L :: Fix g) f x,fmap (_L :: Fix h) f y)
113 -- ^ The product functor recursively applies the mapping function to both sides
115 instance (Functor g,Functor h) => Functor (g :@: h) where
116 fmap _ f x = fmap (_L :: Fix g) (fmap (_L :: Fix h) f) x
117 -- ^ The composition functor applies in the nesting of the mapping function to the nested functor applications
119 instance Functor [] where
121 -- ^ The list functor maps the specific 'map' function over lists of types
123 -- | Short alias to express the structurally equivalent sum of products for some data type
124 type F a x = Rep (PF a) x
126 -- | Polytypic map function
127 pmap :: Functor (PF a) => a -- ^ A value of a data type that is the fixed point of the desired functor
128 -> (x -> y) -> F a x -> F a y -- ^ The mapping over the equivalent sum of products
129 pmap (_::a) f = fmap (_L :: Fix (PF a)) f
131 -- | The 'Mu' class provides the value-level translation between data types and their sum of products representations
133 -- | Packs a sum of products into one equivalent data type
135 -- | unpacks a data type into the equivalent sum of products
138 instance Mu (Fix f) where
141 -- ^ Expanding/contracting the fixed point of a functor is the same as consuming/applying it's single type constructor
143 -- ** Fixpoint combinators
145 -- | In order to simplify type-level composition of functors, we can create fixpoint combinators that implicitely assume fixpoint application.
148 -- ^ Semantically, we can say that @'I' = 'Fix' 'Id'@.
149 type instance PF I = Id
155 data K a = FixConst {unFixConst :: a}
156 -- ^ Semantically, we can say that @'K' t = 'Fix' ('Const' t)@.
157 type instance PF (K a) = Const a
159 instance Mu (K a) where
164 data (a :+!: b) = FixSum {unFixSum :: F (a :+!: b) (a :+!: b)}
165 -- ^ Semantically, we can say that @'Fix' f :+!: 'Fix' g = 'Fix' (f :+: g)@.
166 type instance PF (a :+!: b) = PF a :+: PF b
168 instance Mu (a :+!: b) where
173 data (a :*!: b) = FixProd {unFixProd :: F (a :*!: b) (a :*!: b)}
174 -- ^ Semantically, we can say that @'Fix' f :*!: 'Fix' g = 'Fix' (f :*: g)@.
175 type instance PF (a :*!: b) = PF a :*: PF b
177 instance Mu (a :*!: b) where
182 data (a :@!: b) = FixComp {unFixComp :: F (a :@!: b) (a :@!: b)}
183 -- ^ Semantically, we can say that @'Fix' f :\@!: 'Fix' g = 'Fix' (f ':\@: g)@.
184 type instance PF (a :@!: b) = PF a :@: PF b
186 instance Mu (a :@!: b) where
190 -- * Default definitions for commonly used data types
194 type instance PF [a] = Const One :+: Const a :*: Id
196 instance Mu [a] where
198 inn (Right (x,xs)) = x:xs
200 out (x:xs) = Right (x,xs)
205 cons :: (a,[a]) -> [a]
210 type instance PF Int = Const One :+: Id
212 instance (Mu Int) where
214 inn (Right n) = succ n
216 out n = Right (pred n)
226 type instance PF Bool = Const One :+: Const One
228 instance Mu Bool where
230 inn (Right _) = False
242 type instance PF (Maybe a) = Const One :+: Const a
244 instance Mu (Maybe a) where
245 inn (Left _) = Nothing
246 inn (Right x) = Just x
247 out Nothing = Left _L
248 out (Just x) = Right x
250 maybe2bool :: Maybe a -> Bool
251 maybe2bool = inn . (id -|- bang) . out