Safe Haskell | None |
---|---|
Language | Haskell2010 |
Open type representations and dynamic types
- module Data.Constraint
- module Data.Proxy
- module Language.Syntactic
- class Typeable t a
- data TypeRep t a
- typeRep :: Typeable t a => TypeRep t a
- class Render t => TypeEq t u
- typeEq :: (TypeEq t t, MonadError String m) => TypeRep t a -> TypeRep t b -> m (Dict (a ~ b))
- matchCon :: TypeRep t c -> [E (TypeRep t)]
- matchConM :: Monad m => TypeRep t c -> m [E (TypeRep t)]
- class Witness p t u
- class (ShowClass p, Render t) => PWitness p t u
- wit :: forall p t a. Witness p t t => Proxy p -> TypeRep t a -> Dict (p a)
- pwit :: forall p t m a. (PWitness p t t, MonadError String m) => Proxy p -> TypeRep t a -> m (Dict (p a))
- cast :: forall t a b. (Typeable t a, Typeable t b, TypeEq t t) => Proxy t -> a -> Either String b
- gcast :: forall t a b c. (Typeable t a, Typeable t b, TypeEq t t) => Proxy t -> c a -> Either String (c b)
- data Dynamic t where
- toDyn :: Typeable t a => a -> Dynamic t
- fromDyn :: forall t a. (Typeable t a, TypeEq t t) => Dynamic t -> Either String a
- dynToInteger :: PWitness Integral t t => Dynamic t -> Either String Integer
- class Any a
- witTypeable :: Witness (Typeable t) t t => TypeRep t a -> Dict (Typeable t a)
- pwitTypeable :: PWitness (Typeable t) t t => TypeRep t a -> Either String (Dict (Typeable t a))
- pAny :: Proxy Any
- pEq :: Proxy Eq
- pOrd :: Proxy Ord
- pShow :: Proxy Show
- pNum :: Proxy Num
- pIntegral :: Proxy Integral
- data BoolType a
- data CharType a
- data IntType a
- data FloatType a
- data ListType a
- data FunType a
- boolType :: (Syntactic a, BoolType :<: Domain a, Internal a ~ Bool) => a
- charType :: (Syntactic a, CharType :<: Domain a, Internal a ~ Char) => a
- intType :: (Syntactic a, IntType :<: Domain a, Internal a ~ Int) => a
- floatType :: (Syntactic a, FloatType :<: Domain a, Internal a ~ Float) => a
- listType :: (Syntactic list, Syntactic elem, Domain list ~ Domain elem, ListType :<: Domain list, Internal list ~ [Internal elem], elem ~ c e, list ~ c l) => elem -> list
- 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
- class SubUniverse sub sup where
- weakenUniverse :: TypeRep sub a -> TypeRep sup a
Helper types
module Data.Constraint
module Data.Proxy
module Language.Syntactic
Type representations
This class provides reification of type a
in a universe t
.
means that Typeable
t aa
is in the type universe represented by t
.
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.
); see
Typeable
t awitTypeable
.
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
Witness a type constraint for a reified type
class (ShowClass p, Render t) => PWitness p t u Source
Partially witness a type constraint for a reified type
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
)
Dynamic type parameterized on a type universe
Type class witnessing
The universal class
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
Render BoolType Source | |
VarArg BoolType Source | |
TypeEq BoolType t Source | |
PWitness Eq BoolType t Source | |
PWitness Integral BoolType t Source | |
PWitness Num BoolType t Source | |
PWitness Ord BoolType t Source | |
PWitness Show BoolType t Source | |
PWitness Any BoolType t Source | |
Witness Eq BoolType t Source | |
Witness Ord BoolType t Source | |
Witness Show BoolType t Source | |
Witness Any BoolType t Source | |
(:<:) BoolType t => PWitness (Typeable t) BoolType t Source | |
(:<:) BoolType t => Witness (Typeable t) BoolType t Source |
Render CharType Source | |
VarArg CharType Source | |
TypeEq CharType t Source | |
PWitness Eq CharType t Source | |
PWitness Integral CharType t Source | |
PWitness Num CharType t Source | |
PWitness Ord CharType t Source | |
PWitness Show CharType t Source | |
PWitness Any CharType t Source | |
Witness Eq CharType t Source | |
Witness Ord CharType t Source | |
Witness Show CharType t Source | |
Witness Any CharType t Source | |
(:<:) CharType t => PWitness (Typeable t) CharType t Source | |
(:<:) CharType t => Witness (Typeable t) CharType t Source |
Render IntType Source | |
VarArg IntType Source | |
TypeEq IntType t Source | |
PWitness Eq IntType t Source | |
PWitness Integral IntType t Source | |
PWitness Num IntType t Source | |
PWitness Ord IntType t Source | |
PWitness Show IntType t Source | |
PWitness Any IntType t Source | |
Witness Eq IntType t Source | |
Witness Integral IntType t Source | |
Witness Num IntType t Source | |
Witness Ord IntType t Source | |
Witness Show IntType t Source | |
Witness Any IntType t Source | |
(:<:) IntType t => PWitness (Typeable t) IntType t Source | |
(:<:) IntType t => Witness (Typeable t) IntType t Source |
Render FloatType Source | |
VarArg FloatType Source | |
TypeEq FloatType t Source | |
PWitness Eq FloatType t Source | |
PWitness Integral FloatType t Source | |
PWitness Num FloatType t Source | |
PWitness Ord FloatType t Source | |
PWitness Show FloatType t Source | |
PWitness Any FloatType t Source | |
Witness Eq FloatType t Source | |
Witness Num FloatType t Source | |
Witness Ord FloatType t Source | |
Witness Show FloatType t Source | |
Witness Any FloatType t Source | |
(:<:) FloatType t => PWitness (Typeable t) FloatType t Source | |
(:<:) FloatType t => Witness (Typeable t) FloatType t Source |
Render ListType Source | |
VarArg ListType Source | |
TypeEq t t => TypeEq ListType t Source | |
PWitness Eq t t => PWitness Eq ListType t Source | |
PWitness Integral ListType t Source | |
PWitness Num ListType t Source | |
PWitness Ord t t => PWitness Ord ListType t Source | |
PWitness Show t t => PWitness Show ListType t Source | |
PWitness Any ListType t Source | |
Witness Eq t t => Witness Eq ListType t Source | |
Witness Ord t t => Witness Ord ListType t Source | |
Witness Show t t => Witness Show ListType t Source | |
Witness Any ListType t Source | |
((:<:) ListType t, PWitness (Typeable t) t t) => PWitness (Typeable t) ListType t Source | |
((:<:) ListType t, Witness (Typeable t) t t) => Witness (Typeable t) ListType t Source |
Render FunType Source | |
VarArg FunType Source | |
TypeEq t t => TypeEq FunType t Source | |
PWitness Eq FunType t Source | |
PWitness Integral FunType t Source | |
PWitness Num FunType t Source | |
PWitness Ord FunType t Source | |
PWitness Show FunType t Source | |
PWitness Any FunType t Source | |
Witness Any FunType t Source | |
((:<:) FunType t, PWitness (Typeable t) t t) => PWitness (Typeable t) FunType t Source | |
((:<:) FunType t, Witness (Typeable t) t t) => Witness (Typeable t) FunType t 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
weakenUniverse :: TypeRep sub a -> TypeRep sup a Source
Cast a type representation to a larger universe
(SubUniverse sub sup', (~) (* -> *) sup ((:+:) t sup')) => SubUniverse sub sup Source | |
SubUniverse t t Source |