-----------------------------------------------------------------------------
-- |
-- Module : Data.Type
-- Copyright : (c) 2010 University of Minho
-- License : BSD3
--
-- Maintainer : hpacheco@di.uminho.pt
-- Stability : experimental
-- Portability : non-portable
--
-- Pointless Rewrite:
-- automatic transformation system for point-free programs
--
-- Type-safe representation of types and point-free expressions at the value level, including
-- representation of recursive types as fixpoints of functors.
--
-----------------------------------------------------------------------------
module Data.Type where
import Prelude hiding (Functor(..))
import Data.Monoid
import Generics.Pointless.Combinators
import Generics.Pointless.Functors
import Generics.Pointless.Lenses
-- * Representation of types
data Type a where
-- Internal representations
Any :: Type a
-- INTERNAL: denotes explicit recursivity, needed in some computations where F a c and c \= a
Id :: Type a -> Type a
-- Non-recursive
Int :: Type Int
Bool :: Type Bool
Char :: Type Char
One :: Type One
Either :: Type a -> Type b -> Type (Either a b)
Prod :: Type a -> Type b -> Type (a,b)
Fun :: Type a -> Type b -> Type (a -> b)
Lns :: Type a -> Type b -> Type (Lens a b)
-- Recursive
Data :: (Mu a,Functor (PF a)) => String -> Fctr (PF a) -> Type a
Pf :: Type a -> Type (Pf a)
Dynamic :: Type Dynamic
-- Types for SYB generic programming
TP :: Type T
TU :: Type a -> Type (Q a)
instance Monoid Int where
mempty = 0
mappend = (+)
mconcat = foldr (+) 0
data Dynamic where
Dyn :: Type a -> a -> Dynamic
newtype T = T {unT :: GenericT}
type GenericT = forall a . Type a -> a -> a
newtype Q r = Q {unQ :: GenericQ r}
type GenericQ r = forall a . Type a -> a -> r
class Typeable a where
typeof :: Type a
instance Typeable Int where
typeof = Int
instance Typeable Bool where
typeof = Bool
instance Typeable Char where
typeof = Char
instance Typeable One where
typeof = One
instance (Typeable a,Typeable b) => Typeable (Either a b) where
typeof = Either typeof typeof
instance (Typeable a,Typeable b) => Typeable (a,b) where
typeof = Prod typeof typeof
instance (Typeable a, Typeable b) => Typeable (a -> b) where
typeof = Fun typeof typeof
instance (Typeable a,Typeable b) => Typeable (Lens a b) where
typeof = Lns typeof typeof
instance Typeable a => Typeable (Pf a) where
typeof = Pf typeof
instance Typeable T where
typeof = TP
instance Typeable r => Typeable (Q r) where
typeof = TU typeof
instance Typeable Nat where
typeof = nat
instance Typeable a => Typeable [a] where
typeof = list typeof
nat :: Type Nat
nat = Data "Nat" fctrof
list :: Type a -> Type [a]
list a = Data "List" $ K One :+!: (K a :*!: I)
unlist :: Type [a] -> Type a
unlist (Data "List" (K One :+!: (K a :*!: I))) = a
instance Typeable a => Typeable (Maybe a) where
typeof = Data "Maybe" fctrof
instance (Fctrable f) => Typeable (Fix f) where
typeof = fixof fctrof
-- | Functor GADT for polytypic recursive functions.
-- At the moment it does not rely on a @Typeable@ instance for constants.
data Fctr (f :: * -> *) where
I :: Fctr Id
K :: Type c -> Fctr (Const c)
L :: Fctr []
(:*!:) :: (Functor f,Functor g) => Fctr f -> Fctr g -> Fctr (f :*: g)
(:+!:) :: (Functor f,Functor g) => Fctr f -> Fctr g -> Fctr (f :+: g)
(:@!:) :: (Functor f,Functor g) => Fctr f -> Fctr g -> Fctr (f :@: g)
rep :: Fctr f -> Type a -> Type (Rep f a)
rep I a = a
rep (K c) a = c
rep (f:*!:g) a = Prod (rep f a) (rep g a)
rep (f:+!:g) a = Either (rep f a) (rep g a)
rep (f:@!:g) a = rep f (rep g a)
rep L a = list a
-- | Class of representable functors.
class (Functor f) => Fctrable (f :: * -> *) where
fctrof :: Fctr f
instance Fctrable Id where
fctrof = I
instance Typeable c => Fctrable (Const c) where
fctrof = K typeof
instance Fctrable [] where
fctrof = L
instance (Functor f,Fctrable f,Functor g,Fctrable g) => Fctrable (f :*: g) where
fctrof = (:*!:) fctrof fctrof
instance (Functor f,Fctrable f,Functor g,Fctrable g) => Fctrable (f :+: g) where
fctrof = (:+!:) fctrof fctrof
instance (Functor f,Fctrable f,Functor g,Fctrable g) => Fctrable (f :@: g) where
fctrof = (:@!:) fctrof fctrof
fixof :: (Functor f) => Fctr f -> Type (Fix f)
fixof f = Data "" f
fixF :: Fctr f -> Fix f
fixF (_::Fctr f) = (_L :: Fix f)
fctrofF :: Fctrable f => Fix f -> Fctr f
fctrofF (_::Fix f) = fctrof :: Fctr f
showL :: [String] -> String
showL [x] = x
showL xs = "(" ++ init (Prelude.foldr (\a b -> a ++ " " ++ b) "" xs) ++ ")"
-- * Representation of point-free expressions
data Pf a where
-- Variables and pointwise expressions
VAR :: String -> Pf a
FUN :: String -> (a -> b) -> Pf (a -> b)
-- Internal combinators
HOLE :: Pf a
TOP :: Pf a
CONV :: Either One One -> Pf (a -> b) -> Pf (b -> a)
CONV_LNS :: Either One One -> Pf (Lens c a) -> Pf (Lens a c)
LNS :: String -> Lens c a -> Pf (Lens c a)
COMPF :: Functor f => Fctr f -> Type a -> Pf (Rep f a -> b) -> Pf (c -> Rep f a) -> Pf (c -> b)
COMPF_LNS :: Functor f => Fctr f -> Type a -> Pf (Lens (Rep f a) b) -> Pf (Lens c (Rep f a)) -> Pf (Lens c b)
-- Internal encapsulators
PROTECT :: Pf (a -> b) -> Pf (a -> b)
PROTECT_LNS :: Pf (Lens a b) -> Pf (Lens a b)
-- Non-recursive point-free combinators
PNT :: a -> Pf (One -> a)
BANG :: Pf (a -> One)
COMP :: Type b -> Pf (b -> c) -> Pf (a -> b) -> Pf (a -> c)
FST :: Pf ((a,b) -> a)
SND :: Pf ((a,b) -> b)
SPLIT :: Pf (a -> b) -> Pf (a -> c) -> Pf (a -> (b,c))
PROD :: Pf (a -> c) -> Pf (b -> d) -> Pf ((a,b) -> (c,d))
INL :: Pf (a -> Either a b)
INR :: Pf (b -> Either a b)
EITHER :: Pf (a -> c) -> Pf (b -> c) -> Pf (Either a b -> c)
SUM :: Pf (a -> c) -> Pf (b -> d) -> Pf (Either a b -> Either c d)
-- Monoids
ZERO :: Monoid b => Pf (a -> b)
PLUS :: Monoid a => Pf ((a,a) -> a)
-- Isomorphic point-free combinators
ID :: Pf (c -> c)
SWAP :: Pf ((a,b) -> (b,a))
COSWAP :: Pf ((Either a b) -> (Either b a))
DISTL :: Pf ((Either a b,c) -> (Either (a,c) (b,c)))
UNDISTL :: Pf ((Either (a,c) (b,c)) -> (Either a b, c))
DISTR :: Pf ((c, Either a b) -> (Either (c,a) (c,b)))
UNDISTR :: Pf ((Either (c,a) (c,b)) -> (c,Either a b))
ASSOCL :: Pf ((a,(b,c)) -> ((a,b),c))
ASSOCR :: Pf (((a,b),c) -> (a,(b,c)))
COASSOCL :: Pf ((Either a (Either b c)) -> (Either (Either a b) c))
COASSOCR :: Pf ((Either (Either a b) c) -> (Either a (Either b c)))
-- Recursive point-free combinators
INN :: (Mu a,Functor (PF a)) => Pf (F a a -> a)
OUT :: (Mu a,Functor (PF a)) => Pf (a -> F a a)
FMAP :: Functor f => Fctr f -> Type (c -> a) -> Pf (c -> a) -> Pf (Rep f c -> Rep f a)
FZIP :: Functor f => Fctr f -> Type (a -> c) -> Pf (a -> c) -> Pf ((Rep f a,Rep f c) -> Rep f (a,c))
ANA :: (Mu b,Functor (PF b)) => Pf (a -> (F b a)) -> Pf (a -> b)
CATA :: (Mu a,Functor (PF a)) => Pf (F a b -> b) -> Pf (a -> b)
PARA :: (Mu a,Functor (PF a)) => Pf (F a (c,a) -> c) -> Pf (a -> c)
-- Lens Point-free functions
GET :: Pf (Lens c a) -> Pf (c -> a)
PUT :: Pf (Lens c a) -> Pf ((a,c) -> c)
CREATE :: Pf (Lens c a) -> Pf (a -> c)
-- Non-recursive lenses
COMP_LNS :: Type b -> Pf (Lens b a) -> Pf (Lens c b) -> Pf (Lens c a)
FST_LNS :: Pf (a -> b) -> Pf (Lens (a,b) a)
SND_LNS :: Pf (b -> a) -> Pf (Lens (a,b) b)
PROD_LNS :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (c,d) (a,b))
EITHER_LNS :: Pf (c -> Either One One) -> Pf (Lens a c) -> Pf (Lens b c) -> Pf (Lens (Either a b) c)
SUM_LNS :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (Either c d) (Either a b))
SUMW_LNS :: Pf ((a,d) -> c) -> Pf ((b,c) -> d) -> Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (Either c d) (Either a b))
BANG_LNS :: Pf (One -> c) -> Pf (Lens c One)
BANGL_LNS :: Pf (Lens c (One,c))
BANGR_LNS :: Pf (Lens c (c,One))
-- Non-recursive isomorphisms
ID_LNS :: Pf (Lens c c)
SWAP_LNS :: Pf (Lens (a,b) (b,a))
COSWAP_LNS :: Pf (Lens (Either a b) (Either b a))
DISTL_LNS :: Pf (Lens (Either a b,c) (Either (a,c) (b,c)))
UNDISTL_LNS :: Pf (Lens (Either (a,c) (b,c)) (Either a b,c))
DISTR_LNS :: Pf (Lens (c, Either a b) (Either (c,a) (c,b)))
UNDISTR_LNS :: Pf (Lens (Either (c,a) (c,b)) (c,Either a b))
ASSOCL_LNS :: Pf (Lens (a,(b,c)) ((a,b),c))
ASSOCR_LNS :: Pf (Lens ((a,b),c) (a,(b,c)))
COASSOCL_LNS :: Pf (Lens (Either a (Either b c)) (Either (Either a b) c))
COASSOCR_LNS :: Pf (Lens (Either (Either a b) c) (Either a (Either b c)))
-- Recursive lenses
INN_LNS :: (Mu a,Functor (PF a)) => Pf (Lens (F a a) a)
OUT_LNS :: (Mu a,Functor (PF a)) => Pf (Lens a (F a a))
FMAP_LNS :: Functor f => Fctr f -> Type (c -> a) -> Pf (Lens c a) -> Pf (Lens (Rep f c) (Rep f a))
ANA_LNS :: (Mu b,Functor (PF b)) => Pf (Lens a (F b a)) -> Pf (Lens a b)
CATA_LNS :: (Mu a,Functor (PF a)) => Pf ((Lens (F a b) b)) -> Pf (Lens a b)
-- User-defined lenses
MAP_LNS :: Pf (Lens a b) -> Pf (Lens [a] [b])
LENGTH_LNS :: a -> Pf (Lens [a] Nat)
FILTER_LEFT_LNS :: Pf (Lens [Either a b] [a])
FILTER_RIGHT_LNS :: Pf (Lens [Either a b] [b])
CAT_LNS :: Pf (Lens ([a],[a]) [a])
CONCAT_LNS :: Pf (Lens [[a]] [a])
SUML_LNS :: Pf (Lens [Nat] Nat)
PLUS_LNS :: Pf (Lens (Nat,Nat) Nat)
-- Type-preserving strategy combinators
APPLY :: Type a -> Pf T -> Pf (a -> a)
MKT :: Type a -> Pf (a -> a) -> Pf T
NOP :: Pf T
SEQ :: Pf T -> Pf T -> Pf T
EXTT :: Pf T -> Type b -> Pf (b -> b) -> Pf T
ALL :: Pf T -> Pf T
EVERYWHERE :: Pf T -> Pf T -- bottom-up (catamorphism)
EVERYWHERE' :: Pf T -> Pf T -- top-down (anamorphism)
-- Type-unifying strategy combinators
APPLYQ :: Type a -> Pf (Q r) -> Pf (a -> r)
MKQ :: Monoid r => Type a -> Pf (a -> r) -> Pf (Q r)
EMPTYQ :: Monoid r => Pf (Q r)
UNION :: Monoid r => Pf (Q r) -> Pf (Q r) -> Pf (Q r)
EXTQ :: Pf (Q r) -> Type a -> Pf (a -> r) -> Pf (Q r)
GMAPQ :: Monoid r => Pf (Q r) -> Pf (Q r)
EVERYTHING :: Monoid r => Pf (Q r) -> Pf (Q r) -- bottom-up, right-to-left (paramorphism)
infix 5 ?=
(?=) :: Type a -> Pf (a -> Either One One) -> Pf (a -> Either a a)
(?=) a p = COMP (Either (Prod One a) (Prod One a)) (SND -|-= SND) $ COMP (Prod (Either One One) a) DISTL $ p /\= ID
infixr 9 .=
(.=) :: Typeable b => Pf (b -> a) -> Pf (c -> b) -> Pf (c -> a)
(.=) f g = COMP typeof f g
infix 6 /\=
(/\=) :: Pf (a -> b) -> Pf (a -> c) -> Pf (a -> (b,c))
(/\=) f g = SPLIT f g
infix 7 ><=
(><=) :: Pf (c -> a) -> Pf (d -> b) -> Pf ((c,d) -> (a,b))
(><=) f g = PROD f g
infix 4 \/=
(\/=) :: Pf (b -> a) -> Pf (c -> a) -> Pf (Either b c -> a)
(\/=) f g = EITHER f g
infix 5 -|-=
(-|-=) :: Pf (c -> a) -> Pf (d -> b) -> Pf ((Either c d) -> (Either a b))
(-|-=) f g = SUM f g
distp_pf :: Pf (((c,d),(a,b)) -> ((c,a),(d,b)))
distp_pf = FST ><= FST /\= SND ><= SND
dists_pf :: Type (Either a b,Either c d) -> Pf ((Either a b,Either c d) -> (Either (Either (a,c) (a,d)) (Either (b,c) (b,d))))
dists_pf (Prod (Either a b) (Either c d)) = COMP t (DISTR -|-= DISTR) DISTL
where t = Either (Prod a (Either c d)) (Prod b (Either c d))
infixr 9 .<<
(.<<) :: Typeable b => Pf (Lens b a) -> Pf (Lens c b) -> Pf (Lens c a)
(.<<) f g = COMP_LNS typeof f g
infix 7 ><<<
(><<<) :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (c,d) (a,b))
(><<<) f g = PROD_LNS f g
infix 5 -|-<<
(-|-<<) :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (Either c d) (Either a b))
(-|-<<) f g = SUM_LNS f g
infix 4 \/<<
(\/<<) :: Pf (c -> Either One One) -> Pf (Lens a c) -> Pf (Lens b c) -> Pf (Lens (Either a b) c)
(\/<<) x f g = EITHER_LNS x f g
dists_lns :: Type (Either a b,Either c d) -> Pf (Lens (Either a b,Either c d) (Either (Either (a,c) (a,d)) (Either (b,c) (b,d))))
dists_lns (Prod (Either a b) (Either c d)) = COMP_LNS t (DISTR_LNS -|-<< DISTR_LNS) DISTL_LNS
where t = Either (Prod a (Either c d)) (Prod b (Either c d))
fmap_Lns :: (Functor f,Typeable (c -> a)) => Fctr f -> Pf (Lens c a) -> Pf (Lens (Rep f c) (Rep f a))
fmap_Lns fctr f = FMAP_LNS fctr typeof f