Safe Haskell | None |
---|---|
Language | Haskell2010 |
Type-level metadata
This module provides datatypes (to be used promoted) that can represent the metadata of Haskell datatypes on the type level.
We do not reuse the term-level metadata types, because these are GADTs that incorporate additional invariants. We could (at least in GHC 8) impose the same invariants on the type level as well, but some tests have revealed that the resulting type are rather inconvenient to work with.
So we use simple datatypes to represent the type-level metadata, even if this means that some invariants are not explicitly captured.
We establish a relation between the term- and type-level versions of the metadata by automatically computing the term-level version from the type-level version.
As we now have two versions of metadata (term-level and type-level) with very similar, yet slightly different datatype definitions, the names between the modules clash, and this module is recommended to be imported qualified when needed.
The interface exported by this module is still somewhat experimental.
Since: 0.3.0.0
- data DatatypeInfo
- data ConstructorInfo
- data FieldInfo = FieldInfo FieldName
- type DatatypeName = Symbol
- type ModuleName = Symbol
- type ConstructorName = Symbol
- type FieldName = Symbol
- type Fixity = Nat
- class DemoteDatatypeInfo (x :: DatatypeInfo) (xss :: [[*]]) where
- class DemoteConstructorInfos (cs :: [ConstructorInfo]) (xss :: [[*]]) where
- class DemoteConstructorInfo (x :: ConstructorInfo) (xs :: [*]) where
- class SListI xs => DemoteFieldInfos (fs :: [FieldInfo]) (xs :: [*]) where
- class DemoteFieldInfo (x :: FieldInfo) (a :: *) where
- class DemoteAssociativity (a :: Associativity) where
- data Associativity :: *
Documentation
data DatatypeInfo Source #
Metadata for a datatype (to be used promoted).
A type of kind
contains meta-information about a datatype
that is not contained in its code. This information consists
primarily of the names of the datatype, its constructors, and possibly its
record selectors.DatatypeInfo
The constructor indicates whether the datatype has been declared using newtype
or not.
Since: 0.3.0.0
ADT ModuleName DatatypeName [ConstructorInfo] | Standard algebraic datatype |
Newtype ModuleName DatatypeName ConstructorInfo | Newtype |
data ConstructorInfo Source #
Metadata for a single constructors (to be used promoted).
Since: 0.3.0.0
Constructor ConstructorName | Normal constructor |
Infix ConstructorName Associativity Fixity | Infix constructor |
Record ConstructorName [FieldInfo] | Record constructor |
DemoteConstructorInfos ([] ConstructorInfo) ([] [*]) Source # | |
(DemoteConstructorInfo c xs, DemoteConstructorInfos cs xss) => DemoteConstructorInfos ((:) ConstructorInfo c cs) ((:) [*] xs xss) Source # | |
Metadata for a single record field (to be used promoted).
Since: 0.3.0.0
DemoteFieldInfos ([] FieldInfo) ([] *) Source # | |
(DemoteFieldInfo f x, DemoteFieldInfos fs xs) => DemoteFieldInfos ((:) FieldInfo f fs) ((:) * x xs) Source # | |
type DatatypeName = Symbol Source #
The name of a datatype.
type ModuleName = Symbol Source #
The name of a module.
type ConstructorName = Symbol Source #
The name of a data constructor.
class DemoteDatatypeInfo (x :: DatatypeInfo) (xss :: [[*]]) where Source #
Class for computing term-level datatype information from type-level datatype information.
Since: 0.3.0.0
demoteDatatypeInfo :: proxy x -> DatatypeInfo xss Source #
Given a proxy of some type-level datatype information, return the corresponding term-level information.
Since: 0.3.0.0
(KnownSymbol m, KnownSymbol d, DemoteConstructorInfos cs xss) => DemoteDatatypeInfo (ADT m d cs) xss Source # | |
(KnownSymbol m, KnownSymbol d, DemoteConstructorInfo c ((:) * x ([] *))) => DemoteDatatypeInfo (Newtype m d c) ((:) [*] ((:) * x ([] *)) ([] [*])) Source # | |
class DemoteConstructorInfos (cs :: [ConstructorInfo]) (xss :: [[*]]) where Source #
Class for computing term-level constructor information from type-level constructor information.
Since: 0.3.0.0
demoteConstructorInfos :: proxy cs -> NP ConstructorInfo xss Source #
Given a proxy of some type-level constructor information, return the corresponding term-level information as a product.
Since: 0.3.0.0
DemoteConstructorInfos ([] ConstructorInfo) ([] [*]) Source # | |
(DemoteConstructorInfo c xs, DemoteConstructorInfos cs xss) => DemoteConstructorInfos ((:) ConstructorInfo c cs) ((:) [*] xs xss) Source # | |
class DemoteConstructorInfo (x :: ConstructorInfo) (xs :: [*]) where Source #
Class for computing term-level constructor information from type-level constructor information.
Since: 0.3.0.0
demoteConstructorInfo :: proxy x -> ConstructorInfo xs Source #
Given a proxy of some type-level constructor information, return the corresponding term-level information.
Since: 0.3.0.0
(KnownSymbol s, SListI * xs) => DemoteConstructorInfo (Constructor s) xs Source # | |
(KnownSymbol s, DemoteFieldInfos fs xs) => DemoteConstructorInfo (Record s fs) xs Source # | |
(KnownSymbol s, DemoteAssociativity a, KnownNat f) => DemoteConstructorInfo (Infix s a f) ((:) * y ((:) * z ([] *))) Source # | |
class SListI xs => DemoteFieldInfos (fs :: [FieldInfo]) (xs :: [*]) where Source #
Class for computing term-level field information from type-level field information.
Since: 0.3.0.0
demoteFieldInfos :: proxy fs -> NP FieldInfo xs Source #
Given a proxy of some type-level field information, return the corresponding term-level information as a product.
Since: 0.3.0.0
DemoteFieldInfos ([] FieldInfo) ([] *) Source # | |
(DemoteFieldInfo f x, DemoteFieldInfos fs xs) => DemoteFieldInfos ((:) FieldInfo f fs) ((:) * x xs) Source # | |
class DemoteFieldInfo (x :: FieldInfo) (a :: *) where Source #
Class for computing term-level field information from type-level field information.
Since: 0.3.0.0
demoteFieldInfo :: proxy x -> FieldInfo a Source #
Given a proxy of some type-level field information, return the corresponding term-level information.
Since: 0.3.0.0
KnownSymbol s => DemoteFieldInfo (FieldInfo s) a Source # | |
class DemoteAssociativity (a :: Associativity) where Source #
Class for computing term-level associativity information from type-level associativity information.
Since: 0.3.0.0
demoteAssociativity :: proxy a -> Associativity Source #
Given a proxy of some type-level associativity information, return the corresponding term-level information.
Since: 0.3.0.0
re-exports
data Associativity :: * #
Datatype to represent the associativity of a constructor
Bounded Associativity | |
Enum Associativity | |
Eq Associativity | |
Data Associativity | Since: 4.9.0.0 |
Ord Associativity | |
Read Associativity | |
Show Associativity | |
Ix Associativity | |
Generic Associativity | |
SingKind Associativity | Since: 4.0.0.0 |
SingI Associativity LeftAssociative | Since: 4.9.0.0 |
SingI Associativity RightAssociative | Since: 4.9.0.0 |
SingI Associativity NotAssociative | Since: 4.9.0.0 |
type Rep Associativity | |
data Sing Associativity | |
type DemoteRep Associativity | |