-----------------------------------------------------------------------------
-- |
-- 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 at the value level, including
-- representation of recursive types as fixpoints of functors.
--
-----------------------------------------------------------------------------
module Data.Type where
import Prelude hiding (Functor(..))
import Data.Monoid hiding (Any)
import Data.Char
import Data.List
import {-# SOURCE #-} Data.Pf
import Generics.Pointless.Combinators
import Generics.Pointless.Functors hiding (rep)
import Generics.Pointless.Lenses
import Generics.Pointless.Lenses.Examples.Examples
-- * Representation of types
data Type a where
-- Internal representations
Var :: String -> Type a
Any :: Type 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)
-- Built-in
List :: Type a -> Type [a]
-- Recursive
Data :: (Mu a,Functor (PF a)) => String -> Fctr (PF a) -> Type a
NewData :: Functor f => String -> Fctr f -> Type (Fix f)
Pf :: Type a -> Type (Pf a)
Dynamic :: Type Dynamic
-- Types for SYB generic programming
TP :: Type T
TU :: Type a -> Type (Q a)
TypeRep :: Type (Type a)
FctrRep :: Type (Fctr f)
isData :: Type a -> Bool
isData (Data _ _) = True
isData (NewData _ _) = True
isData _ = False
isAtt :: Type a -> Bool
isAtt (dataName -> Just s) = isPrefixOf "@" s
isAtt _ = False
isOne :: Type a -> Bool
isOne One = True
isOne _ = False
isBasic :: Type a -> Bool
isBasic (List Char) = True
isBasic (Data "Nat" _) = True
isBasic Int = True
isBasic Bool = True
isBasic _ = False
-- | Selects the name and functor of a non-based type
dataNameFctr :: Type a -> Maybe (String,Fctr (PF a))
dataNameFctr a = do
s <- dataName a
f <- dataFctr a
return (s,f)
refname :: String -> String
refname s = aux $ span (/= '\'') s
where aux (x,[]) = x
aux (x,'\'':y) = x ++ y
nodename :: String -> String
nodename = takeWhile (/= '\'')
-- | Checks if two name strings are equal modulo an arbitrary sufix
sameName :: String -> String -> Bool
sameName n n' = map toLower (takeWhile (/= '\'') n) == map toLower (takeWhile (/= '\'') n')
-- | Selects the name of a non-based type
dataName :: Type a -> Maybe String
dataName (Data s _) = Just s
dataName (NewData s _) = Just s
dataName (List a) = Just "List"
dataName _ = Nothing
-- | Selects the functor of a non-base type
dataFctr :: Type a -> Maybe (Fctr (PF a))
dataFctr (Data _ f) = Just f
dataFctr (NewData _ f) = Just f
dataFctr (List a) = Just $ listfctr a
dataFctr a = Nothing
instance Monoid Bool where
mempty = False
mappend = (||)
instance Monoid One where
mempty = _L
mappend _ _ = _L
instance Monoid Int where
mempty = 0
mappend = (+)
instance Monoid Nat where
mempty = nzero
mappend = curry (get plus_lns)
-- | A generic type encapsulator.
data Dynamic where
Dyn :: Type a -> a -> Dynamic
-- Convert a regular type to a dynamic type.
mkDyn :: Type a -> a -> Dynamic
mkDyn a v = Dyn a v
-- Apply a generic function to a dynamically typed value.
applyDyn :: (forall a . Type a -> a -> b) -> Dynamic -> b
applyDyn f (Dyn ta a) = f ta a
data DynType where
DynT :: Type a -> DynType
applyDynT :: (forall a . Type a -> b) -> DynType -> b
applyDynT f (DynT t) = f t
applyDynT2 :: (forall a b . Type a -> Type b -> c) -> DynType -> DynType -> c
applyDynT2 f (DynT a) (DynT b) = f a b
data DynFctr where
DynF :: Functor f => Fctr f -> DynFctr
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 Dynamic where
typeof = Dynamic
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
listfctr :: Type a -> Fctr (Const One :+: Const a :*: Id)
listfctr a = K One :+!: (K a :*!: I)
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)
AnyF :: Fctr a
rep :: Fctr f -> Type a -> Type (Rep f a)
rep I a = a
rep L a = List 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)
-- | 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 = NewData "Fix" f
annT :: Type a -> Ann a
annT (_::Type a) = ann
fixF :: Fctr f -> Ann (Fix f)
fixF (_::Fctr f) = ann
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) ++ ")"
showLst :: [String] -> String
showLst [] = "[]"
showLst [x] = x
showLst xs = "[" ++ init (Prelude.foldr (\a b -> a ++ "," ++ b) "" xs) ++ "]"