6.4.11. Type-level data declarations¶
-
TypeData
¶ Since: 9.6.1 Allow
type data
declarations, which define constructors at the type level.
This extension facilitates type-level (compile-time) programming by
allowing a type-level counterpart of data
declarations, such as this
definition of type-level natural numbers:
type data Nat = Zero | Succ Nat
This is similar to the corresponding data
declaration, except that
the constructors Zero
and Succ
it introduces belong to the type
constructor namespace, so they can be used in types, such as the type
of length-indexed vectors:
data Vec :: Type -> Nat -> Type where
Nil :: Vec a Zero
Cons :: a -> Vec a n -> Vec a (Succ n)
TypeData
is a more fine-grained alternative to the
DataKinds
extension, which defines all the constructors
in all data
declarations as both data constructors and type
constructors.
A type data
declaration has the same syntax as a data
declaration,
either an ordinary algebraic data type or a GADT, prefixed with the keyword
type
, except that it may not contain
a datatype context (even with DatatypeContexts
),
labelled fields,
strictness flags, or
a deriving
clause.
The only constraints permitted in the types of constructors are equality constraints, e.g.:
type data P :: Type -> Type -> Type where
MkP :: (a ~ Natural, b ~~ Char) => P a b
Because type data
declarations introduce type constructors, they do
not permit constructors with the same names as types, so the following
declaration is invalid:
type data T = T // Invalid
The compiler will reject this declaration, because the type constructor
T
is defined twice (as the datatype being defined and as a type
constructor).
The main type constructor of a type data
declaration can be defined
recursively, as in the Nat
example above, but its constructors may not
be used in types within the same mutually recursive group of declarations,
so the following is forbidden:
type data T f = K (f (K Int)) // Invalid