6.4.10. Datatype promotion

DataKinds
Since:

7.4.1

Status:

Included in GHC2024

Allow promotion of data types to kind level.

This section describes data type promotion, an extension to the kind system that complements kind polymorphism. It is enabled by DataKinds, and described in more detail in the paper Giving Haskell a Promotion, which appeared at TLDI 2012. See also TypeData for a more fine-grained alternative.

6.4.10.1. Motivation

Standard Haskell has a rich type language. Types classify terms and serve to avoid many common programming mistakes. The kind language, however, is relatively simple, distinguishing only regular types (kind Type) and type constructors (e.g. kind Type->Type->Type). In particular when using advanced type system features, such as type families (Type families) or GADTs (Generalised Algebraic Data Types (GADTs)), this simple kind system is insufficient, and fails to prevent simple errors. Consider the example of type-level natural numbers, and length-indexed vectors:

dataZedataSundataVec::Type->Type->TypewhereNil::VecaZeCons::a->Vecan->Veca(Sun)

The kind of Vec is Type->Type->Type. This means that, e.g., VecIntChar is a well-kinded type, even though this is not what we intend when defining length-indexed vectors.

With DataKinds, the example above can then be rewritten to:

dataNat=Ze|SuNatdataVec::Type->Nat->TypewhereNil::VecaZeCons::a->Vecan->Veca(Sun)

With the improved kind of Vec, things like VecIntChar are now ill-kinded, and GHC will report an error.

6.4.10.2. Overview

With DataKinds, GHC automatically promotes every datatype to be a kind and its (value) constructors to be type constructors. The following types

dataNat=Zero|SuccNatdataLista=Nil|Consa(Lista)dataPairab=MkPairabdataSumab=La|Rb

give rise to the following kinds and type constructors:

Nat::TypeZero::NatSucc::Nat->NatList::Type->TypeNil::forallk.ListkCons::forallk.k->Listk->ListkPair::Type->Type->TypeMkPair::forallk1k2.k1->k2->Pairk1k2Sum::Type->Type->TypeL::k1->Sumk1k2R::k2->Sumk1k2

Virtually all data constructors, even those with rich kinds, can be promoted. There are only a couple of exceptions to this rule:

  • Data family instance constructors cannot be promoted at the moment. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types.

  • Data constructors with contexts cannot be promoted. For example:

    dataFoo::Type->TypewhereMkFoo::Showa=>Fooa-- not promotable

The following kinds and promoted data constructors can be used even when DataKinds is not enabled:

It is also possible to use kinds declared with typedata (see TypeData) without enabling DataKinds.

6.4.10.3. Distinguishing between types and constructors

Consider

dataP=MkP-- 1dataProm=P-- 2

The name P on the type level will refer to the type P (which has a constructor MkP) rather than the promoted data constructor P of kind Prom. To refer to the latter, prefix it with a single quote mark: 'P.

This syntax can be used even if there is no ambiguity (i.e. there’s no type P in scope).

GHC supports -Wunticked-promoted-constructors that warns whenever a promoted data constructor is written without a quote mark. As of GHC 9.4, this warning is no longer enabled by -Wall; we no longer recommend quote marks as a preferred default (see #20531).

Just as in the case of Template Haskell (Syntax), GHC gets confused if you put a quote mark before a data constructor whose second character is a quote mark. In this case, just put a space between the promotion quote and the data constructor:

data T = A' type S = 'A' -- ERROR: looks like a character type R = ' A' -- OK: promoted `A'`

6.4.10.4. Type-level literals

DataKinds enables the use of numeric and string literals at the type level. For more information, see Type-Level Literals.

6.4.10.6. Promoting existential data constructors

Note that we do promote existential data constructors that are otherwise suitable. For example, consider the following:

dataEx::TypewhereMkEx::foralla.a->Ex

Both the type Ex and the data constructor MkEx get promoted, with the polymorphic kind 'MkEx::forallk.k->Ex. Somewhat surprisingly, you can write a type family to extract the member of a type-level existential:

typefamilyUnEx(ex::Ex)::ktypeinstanceUnEx(MkExx)=x

At first blush, UnEx seems poorly-kinded. The return kind k is not mentioned in the arguments, and thus it would seem that an instance would have to return a member of kfor anyk. However, this is not the case. The type family UnEx is a kind-indexed type family. The return kind k is an implicit parameter to UnEx. The elaborated definitions are as follows (where implicit parameters are denoted by braces):

typefamilyUnEx{k::Type}(ex::Ex)::ktypeinstanceUnEx{k}(MkEx@kx)=x

Thus, the instance triggers only when the implicit parameter to UnEx matches the implicit parameter to MkEx. Because k is actually a parameter to UnEx, the kind is not escaping the existential, and the above code is valid.

See also #7347.

6.4.10.7. DataKinds and type synonyms

The DataKinds extension interacts with type synonyms in the following ways:

  1. In a type context: DataKinds is not required to use a type synonym that expands to a type that would otherwise require the extension. For example:

    {-# LANGUAGE DataKinds #-}moduleAwheretypeMyTrue='True{-# LANGUAGE NoDataKinds #-}moduleBwhereimportAimportData.Proxyf::ProxyMyTruef=Proxy

    GHC will accept the type signature for f even though DataKinds is not enabled, as the promoted data constructor True is tucked underneath the MyTrue type synonym. If the user had written Proxy'True directly, however, then DataKinds would be required.

  2. In a kind context: DataKinds applies to all types mentioned in the kind, including the expansions of type synonyms. For instance, given this module:

    moduleCwheretypeMyType=TypetypeMySymbol=Symbol

    We would accept or reject the following definitions in this module, which makes use of Standalone kind signatures and polymorphic recursion:

    {-# LANGUAGE NoDataKinds #-}moduleDwhereimportC-- ACCEPTED: The kind only mentions Type, which doesn't require DataKindstypeD1::Type->TypedataD1a-- REJECTED: The kind mentions Symbol, which requires DataKinds to use in-- a kind positiondataD2::Symbol->TypedataD2a-- ACCEPTED: The kind mentions a type synonym MyType that expands to-- Type, which doesn't require DataKindsdataD3::MyType->TypedataD3a-- REJECTED: The kind mentions a type synonym MySymbol that expands to-- Symbol, which requires DataKinds to use in a kind positiondataD4::MySymbol->TypedataD4a

6.4.11. Unique syntax for type-level lists and tuples

ListTuplePuns
Since:

9.10.1

Accept bracket syntax to denote type constructors, using single quotes to disambiguate data constructors.

The previously defined mechanism for specifying data constructors with bracket syntax and single quotes is governed by this extension, which is enabled by default.

With NoListTuplePuns, brackets are unambiguously parsed as data constructors, while the single quote is not accepted as a prefix for them anymore. Type constructors cannot be expressed with brackets anymore; instead, new data type declarations in regular syntax have been added to ghc-prim:

dataLista=[]|a:ListadataUnit=()dataTuple2ab=(a,b)dataTuple2#ab=(#a,b#)dataSum2#ab=(#a|#)|(#|b#)class(a,b)=>CTuple2abinstance(c1,c2)=>CTuple2c1c2

CTuple2 is a constraint tuple, which historically only concerns declarations like:

typeC=(EqInt,OrdString)

These are distinct from the usual specification of multiple constraints on functions or instances with parentheses, since those are treated specially by GHC.

When the extension is disabled, any occurrence of special syntax in types will be treated as the data constructor, so a type of (Int,String) has kind Tuple2TypeType, corresponding to the type '(Int,String) with kind (Type,Type) when ListTuplePuns is enabled.

The explicit disambiguation syntax using single quotes is invalid syntax when the extension is disabled.

The earlier example would need to be rewritten like this:

dataHList::ListType->TypewhereHNil::HList[]HCons::a->HListt->HList(a:t)dataTuple::Tuple2TypeType->TypewhereTuple::a->b->Tuple2abfoo0::HList[]foo0=HNilfoo1::HList[Int]foo1=HCons(3::Int)HNilfoo2::HList[Int,Bool]foo2=...

Constraint tuples may be mixed with conventional syntax:

f::Monadm=>CTuple2(Monadm)(Monadm)=>(Monadm,CTuple2(Monadm)(Monadm))=>mIntf=pure5

The new type constructors are exported only from the library ghc-experimental, by the modules Data.Tuple.Experimental, Data.Sum.Experimental and Prelude.Experimental.

Please refer to GHC Proposal #475 for the full specification of effects and interactions.