Commit b0626b63 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Document promotion of existential data types

Thanks to Richard Eisenberg for writing this.
parent 57d67983
......@@ -5530,8 +5530,9 @@ The following restrictions apply to promotion:
higher-kinded datatypes such as <literal>data Fix f = In (f (Fix f))</literal>,
or datatypes whose kinds involve promoted types such as
<literal>Vec :: * -> Nat -> *</literal>.</para></listitem>
<listitem><para>We do not promote datatypes whose constructors are kind
polymorphic, involve constraints, or use existential quantification.
<listitem><para>We do not promote data constructors that are kind
polymorphic, involve constraints, mention type or data families, or involve types that
are not promotable.
<listitem><para>We do not promote data family instances (<xref linkend="data-families"/>).
......@@ -5586,7 +5587,7 @@ Note that this requires <option>-XTypeOperators</option>.
<sect2 id="promoted-literals">
<title>Promoted Literals</title>
Numeric and string literals are prmoted to the type level, giving convenient
Numeric and string literals are promoted to the type level, giving convenient
access to a large number of predefined type-level constants. Numeric literals
are of kind <literal>Nat</literal>, while string literals are of kind
<literal>Symbol</literal>. These kinds are defined in the module
......@@ -5627,6 +5628,46 @@ example = from (Point 1 2) (Get :: Label "x")
<sect2 id="promotion-existentials">
<title>Promoting existential data constructors</title>
Note that we do promote existential data constructors that are otherwise suitable.
For example, consider the following:
data Ex :: * where
MkEx :: forall a. a -> Ex
Both the type <literal>Ex</literal> and the data constructor <literal>MkEx</literal>
get promoted, with the polymorphic kind <literal>'MkEx :: forall k. k -> Ex</literal>.
Somewhat surprisingly, you can write a type family to extract the member
of a type-level existential:
type family UnEx (ex :: Ex) :: k
type instance UnEx (MkEx x) = x
At first blush, <literal>UnEx</literal> seems poorly-kinded. The return kind
<literal>k</literal> is not mentioned in the arguments, and thus it would seem
that an instance would have to return a member of <literal>k</literal>
<emphasis>for any</emphasis> <literal>k</literal>. However, this is not the
case. The type family <literal>UnEx</literal> is a kind-indexed type family.
The return kind <literal>k</literal> is an implicit parameter to <literal>UnEx</literal>.
The elaborated definitions are as follows:
type family UnEx (k :: BOX) (ex :: Ex) :: k
type instance UnEx k (MkEx k x) = x
Thus, the instance triggers only when the implicit parameter to <literal>UnEx</literal>
matches the implicit parameter to <literal>MkEx</literal>. Because <literal>k</literal>
is actually a parameter to <literal>UnEx</literal>, the kind is not escaping the
existential, and the above code is valid.
See also <ulink url="">Trac #7347</ulink>.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment