Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : ghc-7.6
http://hackage.haskell.org/trac/ghc/changeset/f630eb5122b5d6c16b449451e33adda5341b6775 >--------------------------------------------------------------- commit f630eb5122b5d6c16b449451e33adda5341b6775 Author: Simon Peyton Jones <simo...@microsoft.com> Date: Wed Dec 5 16:41:53 2012 +0000 Document promotion of existential data types Thanks to Richard Eisenberg for writing this. >--------------------------------------------------------------- docs/users_guide/glasgow_exts.xml | 47 ++++++++++++++++++++++++++++++++++-- 1 files changed, 44 insertions(+), 3 deletions(-) diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml index 4870490..2a1002a 100644 --- a/docs/users_guide/glasgow_exts.xml +++ b/docs/users_guide/glasgow_exts.xml @@ -5500,8 +5500,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. </para></listitem> <listitem><para>We do not promote data family instances (<xref linkend="data-families"/>). </para></listitem> @@ -5556,7 +5557,7 @@ Note that this requires <option>-XTypeOperators</option>. <sect2 id="promoted-literals"> <title>Promoted Literals</title> <para> -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 @@ -5597,6 +5598,46 @@ example = from (Point 1 2) (Get :: Label "x") </para> </sect2> +<sect2 id="promotion-existentials"> +<title>Promoting existential data constructors</title> +<para> +Note that we do promote existential data constructors that are otherwise suitable. +For example, consider the following: +<programlisting> +data Ex :: * where + MkEx :: forall a. a -> Ex +</programlisting> +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: +<programlisting> +type family UnEx (ex :: Ex) :: k +type instance UnEx (MkEx x) = x +</programlisting> +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: +<programlisting> +type family UnEx (k :: BOX) (ex :: Ex) :: k +type instance UnEx k (MkEx k x) = x +</programlisting> +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. +</para> + +<para> +See also <ulink url="http://hackage.haskell.org/trac/ghc/ticket/7347";>Trac #7347</ulink>. +</para> +</sect2> + + </sect1> _______________________________________________ Cvs-ghc mailing list Cvs-ghc@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc
