----------------------------------------------------------------------------- -- | -- Module : Generics.Pointless.Functors -- Copyright : (c) 2008 University of Minho -- License : BSD3 -- -- Maintainer : hpacheco@di.uminho.pt -- Stability : experimental -- Portability : non-portable -- -- Pointless Haskell: -- point-free programming with recursion patterns as hylomorphisms -- -- This module defines data types as fixed points of functor. -- 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. -- Instead of using an explicit fixpoint operator, a type function is used to relate the data types with their equivalent functor representations. -- ----------------------------------------------------------------------------- module Generics.Pointless.Functors where import Prelude hiding (Functor(..)) import Generics.Pointless.Combinators -- * Functors -- ** Definition and operations over functors -- | Identity functor. newtype Id x = Id {unId :: x} -- | Constant functor. newtype Const t x = Cons {unCons :: t} -- | Sum of functors. infixr 5 :+: data (g :+: h) x = Inl (g x) | Inr (h x) -- | Product of functors. infixr 6 :*: data (g :*: h) x = Prod (g x) (h x) -- | Composition of functors. infixr 9 :@: newtype (g :@: h) x = Comp {unComp :: g (h x)} -- | Explicit fixpoint operator. newtype Fix f = Fix { -- | The unfolding of the fixpoint of a functor is the functor applied to its fixpoint. -- -- 'unFix' is specialized with the application of 'Rep' in order to subsume functor application unFix :: Rep f (Fix f) } instance Show (Rep f (Fix f)) => Show (Fix f) where show (Fix f) = "(Fix " ++ show f ++ ")" -- | Family of patterns functors of data types. -- -- The type function is not necessarily injective, this is, different data types can have the same base functor. type family PF a :: * -> * -- ^ Semantically, we can say that @a = 'Fix' f@. type instance PF (Fix f) = f -- ^ The pattern functor of the fixpoint of a functor is the functor itself. -- | Family of functor representations. -- -- The 'Rep' family implements the implicit coercion between the application of a functor and the structurally equivalent sum of products. type family Rep (f :: * -> *) x :: * -- ^ Functors applied to types can be represented as sums of products. type instance Rep Id x = x -- ^ The identity functor applied to some type is the type itself. type instance Rep (Const t) x = t -- ^ The constant functor applied to some type is the type parameterized by the functor. type instance Rep (g :+: h) x = Rep g x `Either` Rep h x -- ^ The application of a sum of functors to some type is the sum of applying the functors to the argument type. type instance Rep (g :*: h) x = (Rep g x,Rep h x) -- ^ The application of a product of functors to some type is the product of applying the functors to the argument type. type instance Rep (g :@: h) x = Rep g (Rep h x) -- ^ The application of a composition of functors to some type is the nested application of the functors to the argument type. -- -- This particular instance requires that nexted type function application is enabled as a type system extension. type instance Rep [] x = [x] -- ^ The application of the list functor to some type returns a list of the argument type. -- | Polytypic 'Prelude.Functor' class for functor representations class Functor (f :: * -> *) where fmap :: Fix f -- ^ For desambiguation purposes, the type of the functor must be passed as an explicit paramaeter to 'fmap' -> (x -> y) -> Rep f x -> Rep f y -- ^ The mapping over representations instance Functor Id where fmap _ f = f -- ^ The identity functor applies the mapping function the argument type instance Functor (Const t) where fmap _ f = id -- ^ The constant functor preserves the argument type instance (Functor g,Functor h) => Functor (g :+: h) where fmap _ f (Left x) = Left (fmap (_L :: Fix g) f x) fmap _ f (Right x) = Right (fmap (_L :: Fix h) f x) -- ^ The sum functor recursively applies the mapping function to each alternative instance (Functor g,Functor h) => Functor (g :*: h) where fmap _ f (x,y) = (fmap (_L :: Fix g) f x,fmap (_L :: Fix h) f y) -- ^ The product functor recursively applies the mapping function to both sides instance (Functor g,Functor h) => Functor (g :@: h) where fmap _ f x = fmap (_L :: Fix g) (fmap (_L :: Fix h) f) x -- ^ The composition functor applies in the nesting of the mapping function to the nested functor applications instance Functor [] where fmap _ = map -- ^ The list functor maps the specific 'map' function over lists of types -- | Short alias to express the structurally equivalent sum of products for some data type type F a x = Rep (PF a) x -- | Polytypic map function pmap :: Functor (PF a) => a -- ^ A value of a data type that is the fixed point of the desired functor -> (x -> y) -> F a x -> F a y -- ^ The mapping over the equivalent sum of products pmap (_::a) f = fmap (_L :: Fix (PF a)) f -- | The 'Mu' class provides the value-level translation between data types and their sum of products representations class Mu a where -- | Packs a sum of products into one equivalent data type inn :: F a a -> a -- | unpacks a data type into the equivalent sum of products out :: a -> F a a instance Mu (Fix f) where inn = Fix out = unFix -- ^ Expanding/contracting the fixed point of a functor is the same as consuming/applying it's single type constructor -- ** Fixpoint combinators -- | In order to simplify type-level composition of functors, we can create fixpoint combinators that implicitely assume fixpoint application. data I = FixId -- ^ Semantically, we can say that @'I' = 'Fix' 'Id'@. type instance PF I = Id instance Mu I where inn = id out = id data K a = FixConst {unFixConst :: a} -- ^ Semantically, we can say that @'K' t = 'Fix' ('Const' t)@. type instance PF (K a) = Const a instance Mu (K a) where inn = FixConst out = unFixConst infixr 5 :+!: data (a :+!: b) = FixSum {unFixSum :: F (a :+!: b) (a :+!: b)} -- ^ Semantically, we can say that @'Fix' f :+!: 'Fix' g = 'Fix' (f :+: g)@. type instance PF (a :+!: b) = PF a :+: PF b instance Mu (a :+!: b) where inn = FixSum out = unFixSum infixr 6 :*!: data (a :*!: b) = FixProd {unFixProd :: F (a :*!: b) (a :*!: b)} -- ^ Semantically, we can say that @'Fix' f :*!: 'Fix' g = 'Fix' (f :*: g)@. type instance PF (a :*!: b) = PF a :*: PF b instance Mu (a :*!: b) where inn = FixProd out = unFixProd infixr 9 :@!: data (a :@!: b) = FixComp {unFixComp :: F (a :@!: b) (a :@!: b)} -- ^ Semantically, we can say that @'Fix' f :\@!: 'Fix' g = 'Fix' (f ':\@: g)@. type instance PF (a :@!: b) = PF a :@: PF b instance Mu (a :@!: b) where inn = FixComp out = unFixComp -- * Default definitions for commonly used data types -- ** List type instance PF [a] = Const One :+: Const a :*: Id instance Mu [a] where inn (Left _) = [] inn (Right (x,xs)) = x:xs out [] = Left _L out (x:xs) = Right (x,xs) nil :: One -> [a] nil = inn . inl cons :: (a,[a]) -> [a] cons = inn . inr -- ** Natural Numbers data Nat = Zero | Succ Nat deriving (Eq,Show) type instance PF Nat = Const One :+: Id instance Mu Nat where inn (Left _) = Zero inn (Right n) = Succ n out Zero = Left _L out (Succ n) = Right n -- ** Int (positive only) type instance PF Int = Const One :+: Id instance (Mu Int) where inn (Left _) = 0 inn (Right n) = succ n out 0 = Left _L out n = Right (pred n) zero :: One -> Int zero = inn . inl suck :: Int -> Int suck = inn . inr -- ** Bool type instance PF Bool = Const One :+: Const One instance Mu Bool where inn (Left _) = True inn (Right _) = False out True = Left _L out False = Right _L true :: One -> Bool true = inn . inl false :: One -> Bool false = inn . inr -- ** Maybe type instance PF (Maybe a) = Const One :+: Const a instance Mu (Maybe a) where inn (Left _) = Nothing inn (Right x) = Just x out Nothing = Left _L out (Just x) = Right x maybe2bool :: Maybe a -> Bool maybe2bool = inn . (id -|- bang) . out