<itemizedlist>
<listitem>
<para>The Foreign Function Interface language specification
- (included in this manual, in <xref linkend="ffi">).</para>
+ (included in this manual, in <xref linkend="ffi">).
+ You must use the <option>-fglasgow-exts</option> command-line option
+ to make GHC understand the <literal>foreign</literal> declarations
+ defined by the FFI.</para>
</listitem>
<listitem>
<para>
When generating C (using the <option>-fvia-C</option> directive), one can assist the
-C compiler in detecting type errors by using the <Command>-#include</Command> directive
-to provide <filename>.h</filename> files containing function headers.
+C compiler in detecting type errors by using the <option>-#include</option> directive
+(<xref linkend="options-C-compiler">) to provide <filename>.h</filename> files containing function headers.
</para>
<para>
</para>
<para>
+ Pattern type signatures are completely orthogonal to ordinary, separate
+type signatures. The two can be used independently or together.
At ordinary type signatures, such as that for <VarName>ys</VarName>, any type variables
mentioned in the type signature <emphasis>that are not in scope</emphasis> are
implicitly universally quantified. (If there are no type variables in
</para>
<sect2>
+<title>What a pattern type signature means</title>
+<para>
+A type variable brought into scope by a pattern type signature is simply
+the name for a type. The restriction they express is that all occurrences
+of the same name mean the same type. For example:
+<programlisting>
+ f :: [Int] -> Int -> Int
+ f (xs::[a]) (y::a) = (head xs + y) :: a
+</programlisting>
+The pattern type signatures on the left hand side of
+<literal>f</literal> express the fact that <literal>xs</literal>
+must be a list of things of some type <literal>a</literal>; and that <literal>y</literal>
+must have this same type. The type signature on the expression <literal>(head xs)</literal>
+specifies that this expression must have the same type <literal>a</literal>.
+<emphasis>There is no requirement that the type named by "<literal>a</literal>" is
+in fact a type variable</emphasis>. Indeed, in this case, the type named by "<literal>a</literal>" is
+<literal>Int</literal>. (This is a slight liberalisation from the original rather complex
+rules, which specified that a pattern-bound type variable should be universally quantified.)
+For example, all of these are legal:</para>
+
+<programlisting>
+ t (x::a) (y::a) = x+y*2
+
+ f (x::a) (y::b) = [x,y] -- a unifies with b
+
+ g (x::a) = x + 1::Int -- a unifies with Int
+
+ h x = let k (y::a) = [x,y] -- a is free in the
+ in k x -- environment
+
+ k (x::a) True = ... -- a unifies with Int
+ k (x::Int) False = ...
+
+ w :: [b] -> [b]
+ w (x::a) = x -- a unifies with [b]
+</programlisting>
+
+</sect2>
+
+<sect2>
<title>Scope and implicit quantification</title>
<para>
<listitem>
<para>
- All the type variables mentioned in the patterns for a single
-function definition equation, that are not already in scope,
-are brought into scope by the patterns. We describe this set as
-the <emphasis>type variables bound by the equation</emphasis>.
-
+All the type variables mentioned in a pattern,
+that are not already in scope,
+are brought into scope by the pattern. We describe this set as
+the <emphasis>type variables bound by the pattern</emphasis>.
+For example:
+<programlisting>
+ f (x::a) = let g (y::(a,b)) = fst y
+ in
+ g (x,True)
+</programlisting>
+The pattern <literal>(x::a)</literal> brings the type variable
+<literal>a</literal> into scope, as well as the term
+variable <literal>x</literal>. The pattern <literal>(y::(a,b))</literal>
+contains an occurrence of the already-in-scope type variable <literal>a</literal>,
+and brings into scope the type variable <literal>b</literal>.
</para>
</listitem>
-<listitem>
+<listitem>
<para>
The type variables thus brought into scope may be mentioned
in ordinary type signatures or pattern type signatures anywhere within
</para>
</listitem>
-<listitem>
+<listitem>
<para>
In ordinary type signatures, any type variable mentioned in the
signature that is in scope is <emphasis>not</emphasis> universally quantified.
</para>
</listitem>
+
<listitem>
<para>
Ordinary type signatures do not bring any new type variables
into scope (except in the type signature itself!). So this is illegal:
-
<programlisting>
f :: a -> a
f x = x::a
</programlisting>
-
It's illegal because <VarName>a</VarName> is not in scope in the body of <function>f</function>,
so the ordinary signature <literal>x::a</literal> is equivalent to <literal>x::forall a.a</literal>;
and that is an incorrect typing.
</para>
</listitem>
-<listitem>
+<listitem>
<para>
There is no implicit universal quantification on pattern type
signatures, nor may one write an explicit <literal>forall</literal> type in a pattern
</para>
</listitem>
-<listitem>
+<listitem>
<para>
The type variables in the head of a <literal>class</literal> or <literal>instance</literal> declaration
</sect2>
<sect2>
-<title>Polymorphism</title>
-
-<para>
-
-<itemizedlist>
-<listitem>
-
-<para>
- Pattern type signatures are completely orthogonal to ordinary, separate
-type signatures. The two can be used independently or together. There is
-no scoping associated with the names of the type variables in a separate type signature.
-
-
-<programlisting>
- f :: [a] -> [a]
- f (xs::[b]) = reverse xs
-</programlisting>
-
-
-</para>
-</listitem>
-<listitem>
-
-<para>
- The function must be polymorphic in the type variables
-bound by all its equations. Operationally, the type variables bound
-by one equation must not:
-
-
-<itemizedlist>
-<listitem>
-
-<para>
- Be unified with a type (such as <literal>Int</literal>, or <literal>[a]</literal>).
-</para>
-</listitem>
-<listitem>
-
-<para>
- Be unified with a type variable free in the environment.
-</para>
-</listitem>
-<listitem>
-
-<para>
- Be unified with each other. (They may unify with the type variables
-bound by another equation for the same function, of course.)
-</para>
-</listitem>
-
-</itemizedlist>
-
-
-For example, the following all fail to type check:
-
-
-<programlisting>
- f (x::a) (y::b) = [x,y] -- a unifies with b
-
- g (x::a) = x + 1::Int -- a unifies with Int
-
- h x = let k (y::a) = [x,y] -- a is free in the
- in k x -- environment
-
- k (x::a) True = ... -- a unifies with Int
- k (x::Int) False = ...
-
- w :: [b] -> [b]
- w (x::a) = x -- a unifies with [b]
-</programlisting>
-
-
-</para>
-</listitem>
-<listitem>
-
-<para>
- The pattern-bound type variable may, however, be constrained
-by the context of the principal type, thus:
-
-
-<programlisting>
- f (x::a) (y::a) = x+y*2
-</programlisting>
-
-
-gets the inferred type: <literal>forall a. Num a => a -> a -> a</literal>.
-</para>
-</listitem>
-
-</itemizedlist>
-
-</para>
-
-</sect2>
-
-<sect2>
<title>Result type signatures</title>
<para>
</sect2>
<sect2>
-<title>Pattern signatures on other constructs</title>
+<title>Where a pattern type signature can occur</title>
<para>
-
+A pattern type signature can occur in any pattern, but there
+are restrictions on pattern bindings:
<itemizedlist>
-<listitem>
+<listitem>
<para>
- A pattern type signature can be on an arbitrary sub-pattern, not
-just on a variable:
+A pattern type signature can be on an arbitrary sub-pattern, not
+ust on a variable:
<programlisting>
Pattern type signatures, including the result part, can be used
in lambda abstractions:
-
<programlisting>
(\ (x::a, y) :: a -> x)
</programlisting>
-
-
-Type variables bound by these patterns must be polymorphic in
-the sense defined above.
-For example:
-
-
-<programlisting>
- f1 (x::c) = f1 x -- ok
- f2 = \(x::c) -> f2 x -- not ok
-</programlisting>
-
-
-Here, <function>f1</function> is OK, but <function>f2</function> is not, because <VarName>c</VarName> gets unified
-with a type variable free in the environment, in this
-case, the type of <function>f2</function>, which is in the environment when
-the lambda abstraction is checked.
-
</para>
</listitem>
<listitem>
case e of { (x::a, y) :: a -> x }
</programlisting>
+</para>
+</listitem>
-The pattern-bound type variables must, as usual,
-be polymorphic in the following sense: each case alternative,
-considered as a lambda abstraction, must be polymorphic.
-Thus this is OK:
-
-
-<programlisting>
- case (True,False) of { (x::a, y) -> x }
-</programlisting>
-
-
-Even though the context is that of a pair of booleans,
-the alternative itself is polymorphic. Of course, it is
-also OK to say:
+<listitem>
+<para>
+To avoid ambiguity, the type after the “<literal>::</literal>” in a result
+pattern signature on a lambda or <literal>case</literal> must be atomic (i.e. a single
+token or a parenthesised type of some sort). To see why,
+consider how one would parse this:
<programlisting>
- case (True,False) of { (x::Bool, y) -> x }
+ \ x :: a -> b -> x
</programlisting>
</para>
</listitem>
+
<listitem>
<para>
-To avoid ambiguity, the type after the “<literal>::</literal>” in a result
-pattern signature on a lambda or <literal>case</literal> must be atomic (i.e. a single
-token or a parenthesised type of some sort). To see why,
-consider how one would parse this:
+ Pattern type signatures can bind existential type variables.
+For example:
<programlisting>
- \ x :: a -> b -> x
+ data T = forall a. MkT [a]
+
+ f :: T -> T
+ f (MkT [t::a]) = MkT t3
+ where
+ t3::[a] = [t,t,t]
</programlisting>
</para>
</listitem>
+
+
<listitem>
<para>
- Pattern type signatures that bind new type variables
+Pattern type signatures that bind new type variables
may not be used in pattern bindings at all.
So this is illegal:
</sect2>
-<sect2>
-<title>Existentials</title>
-
-<para>
-
-<itemizedlist>
-<listitem>
-
-<para>
- Pattern type signatures can bind existential type variables.
-For example:
-
-
-<programlisting>
- data T = forall a. MkT [a]
-
- f :: T -> T
- f (MkT [t::a]) = MkT t3
- where
- t3::[a] = [t,t,t]
-</programlisting>
-
-
-</para>
-</listitem>
-
-</itemizedlist>
-
-</para>
-
-</sect2>
</sect1>
<para>To use generics you need to</para>
<itemizedlist>
<listitem>
- <para>Use the <option>-fgenerics</option> flag.</para>
+ <para>Use the flags <option>-fglasgow-exts</option> (to enable the extra syntax),
+ <option>-fgenerics</option> (to generate extra per-data-type code),
+ and <option>-package lang</option> (to make the <literal>Generics</literal> library
+ available. </para>
</listitem>
<listitem>
<para>Import the module <literal>Generics</literal> from the
any operator starting in a colon as an infix type constructor). Also note that
the type constructors are not exactly as in the paper (Unit instead of 1, etc).
Finally, note that the syntax of the type patterns in the class declaration
-uses "<literal>{|</literal>" and "<literal>{|</literal>" brackets; curly braces
+uses "<literal>{|</literal>" and "<literal>|}</literal>" brackets; curly braces
alone would ambiguous when they appear on right hand sides (an extension we
anticipate wanting).
</para>
projects / ghc-hetmet.git / blobdiff