open-typerep-0.3.1: Open type representations and dynamic types

Safe HaskellNone
LanguageHaskell2010

Data.TypeRep

Contents

Description

Open type representations and dynamic types

Synopsis

Helper types

module Data.Constraint

module Data.Proxy

module Data.Syntactic

Type representations

class Typeable t a Source

This class provides reification of type a in a universe t. Typeable t a means that a is in the type universe represented by t.

Minimal complete definition

typeRep'

Instances

data TypeRep t a Source

Representation of type a in a type universe t

This type can also be seen as a witness that a is a member of t (i.e. Typeable t a); see witTypeable.

Instances

Render t => Show (TypeRep t a) 
Syntactic (TypeRep t a) 
type Internal (TypeRep t a) = a 
type Domain (TypeRep t a) = t 

typeRep :: Typeable t a => TypeRep t a Source

Reification of type a in a type universe t

class Render t => TypeEq t u Source

Equality on type representations

Minimal complete definition

typeEqSym

Instances

typeEq :: (TypeEq t t, MonadError String m) => TypeRep t a -> TypeRep t b -> m (Dict (a ~ b)) Source

Equality on type representations

matchCon :: TypeRep t c -> [E (TypeRep t)] Source

Type constructor matching. This function makes it possible to match on type representations without dealing with the underlying AST representation.

For example, to check that a TypeRep represents the type a -> Int for some a:

is_atoi :: (TypeEq t t, IntType :<: t) => TypeRep t a -> Bool
is_atoi t
    | [E ta, E tb] <- matchCon t
    , Just _       <- typeEq ta intType = True
    | otherwise                         = False

matchConM :: Monad m => TypeRep t c -> m [E (TypeRep t)] Source

Monadic version of matchCon

matchConM = return . matchCon

matchConM is convenient when matching types in a monad, e.g.:

do ...
   [E ta, E tb] <- matchConM t
   Dict         <- typeEq ta tb
   ...

class Witness p t u Source

Witness a type constraint for a reified type

Minimal complete definition

witSym

Instances

class (ShowClass p, Render t) => PWitness p t u Source

Partially witness a type constraint for a reified type

Instances

wit :: forall p t a. Witness p t t => Proxy p -> TypeRep t a -> Dict (p a) Source

Witness a type constraint for a reified type

pwit :: forall p t m a. (PWitness p t t, MonadError String m) => Proxy p -> TypeRep t a -> m (Dict (p a)) Source

Partially witness a type constraint for a reified type

Dynamic types

cast :: forall t a b. (Typeable t a, Typeable t b, TypeEq t t) => Proxy t -> a -> Either String b Source

Safe cast (does not use unsafeCoerce)

gcast :: forall t a b c. (Typeable t a, Typeable t b, TypeEq t t) => Proxy t -> c a -> Either String (c b) Source

Safe generalized cast (does not use unsafeCoerce)

data Dynamic t where Source

Dynamic type parameterized on a type universe

Constructors

Dyn :: TypeRep t a -> a -> Dynamic t 

Instances

(TypeEq t t, Witness Eq t t) => Eq (Dynamic t) 
Witness Show t t => Show (Dynamic t) 

toDyn :: Typeable t a => a -> Dynamic t Source

fromDyn :: forall t a. (Typeable t a, TypeEq t t) => Dynamic t -> Either String a Source

dynToInteger :: PWitness Integral t t => Dynamic t -> Either String Integer Source

Type class witnessing

class Any a Source

The universal class

Instances

witTypeable :: Witness (Typeable t) t t => TypeRep t a -> Dict (Typeable t a) Source

Witness a Typeable constraint for a reified type

pwitTypeable :: PWitness (Typeable t) t t => TypeRep t a -> Either String (Dict (Typeable t a)) Source

Partially witness a Typeable constraint for a reified type

pAny :: Proxy Any Source

pEq :: Proxy Eq Source

pOrd :: Proxy Ord Source

pShow :: Proxy Show Source

pNum :: Proxy Num Source

pIntegral :: Proxy Integral Source

data BoolType a Source

Instances

data CharType a Source

Instances

data IntType a Source

Instances

data FloatType a Source

Instances

data ListType a Source

Instances

data FunType a Source

Instances

boolType :: (Syntactic a, BoolType :<: Domain a, Internal a ~ Bool) => a Source

charType :: (Syntactic a, CharType :<: Domain a, Internal a ~ Char) => a Source

intType :: (Syntactic a, IntType :<: Domain a, Internal a ~ Int) => a Source

floatType :: (Syntactic a, FloatType :<: Domain a, Internal a ~ Float) => a Source

listType :: (Syntactic list, Syntactic elem, Domain list ~ Domain elem, ListType :<: Domain list, Internal list ~ [Internal elem], elem ~ c e, list ~ c l) => elem -> list Source

funType :: (Syntactic fun, Syntactic a, Syntactic b, Domain fun ~ Domain a, Domain fun ~ Domain b, FunType :<: Domain fun, Internal fun ~ (Internal a -> Internal b), a ~ c x, b ~ c y, fun ~ c z) => a -> b -> fun Source

Sub-universes

class SubUniverse sub sup where Source

Sub-universe relation

In general, a universe t is a sub-universe of u if u has the form

t1 :+: t2 :+: ... :+: t

Methods

weakenUniverse :: TypeRep sub a -> TypeRep sup a Source

Cast a type representation to a larger universe

Instances

(SubUniverse sub sup', (~) (* -> *) sup ((:+:) t sup')) => SubUniverse sub sup 
SubUniverse t t