Safe Haskell  None 

Language  Haskell2010 
This module is internal to QuickSpec.
Polymorphic types and dynamic values.
Synopsis
 class Typeable (a :: k)
 type Type = Term TyCon
 data TyCon
 tyCon :: Typeable a => proxy a > TyCon
 fromTyCon :: TyCon > TyCon
 data A
 data B
 data C
 data D
 data E
 class ClassA
 class ClassB
 class ClassC
 class ClassD
 class ClassE
 class ClassF
 type SymA = "__polymorphic_symbol__"
 typeVar :: Type
 isTypeVar :: Type > Bool
 typeOf :: Typeable a => a > Type
 typeRep :: Typeable (a :: k) => proxy a > Type
 typeFromTyCon :: TyCon > Type
 applyType :: Type > Type > Type
 fromTypeRep :: TypeRep > Type
 arrowType :: [Type] > Type > Type
 isArrowType :: Type > Bool
 unpackArrow :: Type > Maybe (Type, Type)
 typeArgs :: Type > [Type]
 typeRes :: Type > Type
 typeDrop :: Int > Type > Type
 typeArity :: Type > Int
 isDictionary :: Type > Bool
 getDictionary :: Type > Maybe Type
 splitConstrainedType :: Type > ([Type], Type)
 dictArity :: Type > Int
 pPrintType :: Type > Doc
 class Typed a where
 typ :: a > Type
 otherTypesDL :: a > DList Type
 typeSubst_ :: (Var > Builder TyCon) > a > a
 typeSubst :: (Typed a, Substitution s, SubstFun s ~ TyCon) => s > a > a
 typesDL :: Typed a => a > DList Type
 tyVars :: Typed a => a > [Var]
 cast :: Typed a => Type > a > Maybe a
 matchType :: Type > Type > Maybe (Subst TyCon)
 newtype TypeView a = TypeView {
 unTypeView :: a
 class Typed a => Apply a where
 apply :: Apply a => a > a > a
 canApply :: Apply a => a > a > Bool
 oneTypeVar :: Typed a => a > a
 defaultTo :: Typed a => Type > a > a
 skolemiseTypeVars :: Typed a => a > a
 canonicaliseType :: Typed a => a > a
 data Poly a
 toPolyValue :: (Applicative f, Typeable a) => a > Poly (Value f)
 poly :: Typed a => a > Poly a
 unPoly :: Poly a > a
 polyTyp :: Typed a => Poly a > Poly Type
 polyRename :: (Typed a, Typed b) => a > Poly b > b
 polyApply :: (Typed a, Typed b, Typed c) => (a > b > c) > Poly a > Poly b > Poly c
 polyPair :: (Typed a, Typed b) => Poly a > Poly b > Poly (a, b)
 polyList :: Typed a => [Poly a] > Poly [a]
 polyMgu :: Poly Type > Poly Type > Maybe (Poly Type)
 data Value f
 toValue :: forall f (a :: *). Typeable a => f a > Value f
 fromValue :: forall f (a :: *). Typeable a => Value f > Maybe (f a)
 valueType :: Value f > Type
 unwrap :: Value f > Unwrapped f
 data Unwrapped f where
 data Wrapper a = Wrapper {}
 mapValue :: (forall a. f a > g a) > Value f > Value g
 forValue :: Value f > (forall a. f a > g a) > Value g
 ofValue :: (forall a. f a > b) > Value f > b
 withValue :: Value f > (forall a. f a > b) > b
 pairValues :: forall f g. Typeable g => (forall a b. f a > f b > f (g a b)) > Value f > Value f > Value f
 wrapFunctor :: forall f g h. Typeable h => (forall a. f a > g (h a)) > Value f > Value g
 unwrapFunctor :: forall f g h. Typeable g => (forall a. f (g a) > h a) > Value f > Value h
 bringFunctor :: Functor f => Value f > f (Value Identity)
Types
The class Typeable
allows a concrete representation of a type to
be calculated.
typeRep#
A type constructor.
Arrow  The function type constructor 
TyCon TyCon  An ordinary Haskell type constructor. 
String String  A string. Can be used to represent miscellaneous types that do not really exist in Haskell. 
Instances
Eq TyCon Source #  
Ord TyCon Source #  
Show TyCon Source #  
CoArbitrary Type Source #  
Defined in QuickSpec.Internal.Type coarbitrary :: Type > Gen b > Gen b #  
Pretty TyCon Source #  
Defined in QuickSpec.Internal.Type pPrintPrec :: PrettyLevel > Rational > TyCon > Doc # pPrintList :: PrettyLevel > [TyCon] > Doc #  
PrettyTerm TyCon Source #  
Defined in QuickSpec.Internal.Type  
Apply Type Source #  
Typed Type Source #  
CoArbitrary (TermList TyCon) Source #  
Defined in QuickSpec.Internal.Type  
Typed a => Has (TypeView a) Type Source #  
Defined in QuickSpec.Internal.Type 
applyType :: Type > Type > Type Source #
Function application for type constructors.
For example, applyType (typeRep (Proxy :: Proxy [])) (typeRep (Proxy :: Proxy Int)) == typeRep (Proxy :: Proxy [Int])
.
isArrowType :: Type > Bool Source #
Is a given type a function type?
unpackArrow :: Type > Maybe (Type, Type) Source #
Decompose a function type into (argument, result).
For multipleargument functions, unpacks one argument.
typeDrop :: Int > Type > Type Source #
Given the type of a function, returns the type of applying that function to
n
arguments. Crashes if the type does not have enough arguments.
getDictionary :: Type > Maybe Type Source #
Check if a type is of the form
, and if so, return Dict
cc
.
splitConstrainedType :: Type > ([Type], Type) Source #
Split a type into constraints and normal type.
pPrintType :: Type > Doc Source #
Prettyprint a type. Differs from the Pretty
instance by printing type
variables in lowercase.
Things that have types
A class for things that have a type.
The type.
otherTypesDL :: a > DList Type Source #
Types that appear elsewhere in the Typed
, for example, types of subterms.
Should return everything which is affected by typeSubst
.
typeSubst_ :: (Var > Builder TyCon) > a > a Source #
Substitute for all type variables.
Instances
Typed Type Source #  
Typed Var Source #  
Typed a => Typed [a] Source #  
Typed a => Typed (Poly a) Source #  
Typed f => Typed (Term f) Source #  
(Typed a, Typed b) => Typed (Either a b) Source #  
(Typed a, Typed b) => Typed (a, b) Source #  
Typed (Value f) Source #  
(Typed fun1, Typed fun2) => Typed (fun1 :+: fun2) Source #  
typeSubst :: (Typed a, Substitution s, SubstFun s ~ TyCon) => s > a > a Source #
Substitute for all type variables in a Typed
.
cast :: Typed a => Type > a > Maybe a Source #
Cast a Typed
to a target type.
Succeeds if the target type is an instance of the current type.
matchType :: Type > Type > Maybe (Subst TyCon) Source #
Check if the second argument is an instance of the first argument.
A wrapper for using the Symbolic
machinery on types.
TypeView  

class Typed a => Apply a where Source #
Typed things that support function application.
oneTypeVar :: Typed a => a > a Source #
Unify all type variables in a type.
skolemiseTypeVars :: Typed a => a > a Source #
Make a type ground by replacing all type variables with Skolem constants.
Polymorphic types
canonicaliseType :: Typed a => a > a Source #
Alpharename type variables in a canonical way.
Represents a forallquantifier over all the type variables in a type.
Wrapping a term in Poly
normalises the type by alpharenaming
type variables canonically.
The Apply
instance for Poly
does unification to handle applying a
polymorphic function.
Instances
Eq a => Eq (Poly a) Source #  
Ord a => Ord (Poly a) Source #  
Show a => Show (Poly a) Source #  
Pretty a => Pretty (Poly a) Source #  
Defined in QuickSpec.Internal.Type pPrintPrec :: PrettyLevel > Rational > Poly a > Doc # pPrintList :: PrettyLevel > [Poly a] > Doc #  
Apply a => Apply (Poly a) Source #  
Typed a => Typed (Poly a) Source #  
toPolyValue :: (Applicative f, Typeable a) => a > Poly (Value f) Source #
Convert an ordinary value to a dynamic value.
polyRename :: (Typed a, Typed b) => a > Poly b > b Source #
Rename the type variables of the second argument so that they don't overlap with those of the first argument.
polyApply :: (Typed a, Typed b, Typed c) => (a > b > c) > Poly a > Poly b > Poly c Source #
Rename the type variables of both arguments so that they don't overlap.
polyPair :: (Typed a, Typed b) => Poly a > Poly b > Poly (a, b) Source #
Rename the type variables of both arguments so that they don't overlap.
polyList :: Typed a => [Poly a] > Poly [a] Source #
Rename the type variables of all arguments so that they don't overlap.
polyMgu :: Poly Type > Poly Type > Maybe (Poly Type) Source #
Find the most general unifier of two types.
Dynamic values
Dynamic values inside an applicative functor.
For example, a value of type Value Maybe
represents a Maybe something
.
unwrap :: Value f > Unwrapped f Source #
Unwrap a value to get at the thing inside, with an existential type.
data Unwrapped f where Source #
The unwrapped value. Consists of the value itself (with an existential type) and functions to wrap it up again.
Functions for rewrapping an Unwrapped
value.
mapValue :: (forall a. f a > g a) > Value f > Value g Source #
Apply a polymorphic function to a Value
.
forValue :: Value f > (forall a. f a > g a) > Value g Source #
Apply a polymorphic function to a Value
.
pairValues :: forall f g. Typeable g => (forall a b. f a > f b > f (g a b)) > Value f > Value f > Value f Source #
Apply a polymorphic function to a pair of Value
s.
wrapFunctor :: forall f g h. Typeable h => (forall a. f a > g (h a)) > Value f > Value g Source #