Commit 03aaa24e authored by simonpj's avatar simonpj
Browse files

[project @ 2005-10-26 13:03:39 by simonpj]

Improve documentation of typeclass extensions; merge to stable if it goes easily
parent 07806d2b
......@@ -1429,19 +1429,20 @@ declarations. Define your own instances!
<title>Class declarations</title>
<para>
This section documents GHC's implementation of multi-parameter type
classes. There's lots of background in the paper <ulink
This section, and the next one, documents GHC's type-class extensions.
There's lots of background in the paper <ulink
url="http://research.microsoft.com/~simonpj/Papers/type-class-design-space" >Type
classes: exploring the design space</ulink > (Simon Peyton Jones, Mark
Jones, Erik Meijer).
</para>
<para>
There are the following constraints on class declarations:
<orderedlist>
<listitem>
All the extensions are enabled by the <option>-fglasgow-exts</option> flag.
</para>
<sect3>
<title>Multi-parameter type classes</title>
<para>
<emphasis>Multi-parameter type classes are permitted</emphasis>. For example:
Multi-parameter type classes are permitted. For example:
<programlisting>
......@@ -1450,39 +1451,16 @@ There are the following constraints on class declarations:
...etc.
</programlisting>
</para>
</listitem>
<listitem>
<para>
<emphasis>The class hierarchy must be acyclic</emphasis>. However, the definition
of "acyclic" involves only the superclass relationships. For example,
this is OK:
<programlisting>
class C a where {
op :: D b => a -> b -> b
}
class C a => D a where { ... }
</programlisting>
Here, <literal>C</literal> is a superclass of <literal>D</literal>, but it's OK for a
class operation <literal>op</literal> of <literal>C</literal> to mention <literal>D</literal>. (It
would not be OK for <literal>D</literal> to be a superclass of <literal>C</literal>.)
</sect3>
</para>
</listitem>
<listitem>
<sect3>
<title>The superclasses of a class declaration</title>
<para>
<emphasis>There are no restrictions on the context in a class declaration
There are no restrictions on the context in a class declaration
(which introduces superclasses), except that the class hierarchy must
be acyclic</emphasis>. So these class declarations are OK:
be acyclic. So these class declarations are OK:
<programlisting>
......@@ -1495,62 +1473,33 @@ be acyclic</emphasis>. So these class declarations are OK:
</para>
</listitem>
<listitem>
<para>
<emphasis>All of the class type variables must be reachable (in the sense
mentioned in <xref linkend="type-restrictions"/>)
from the free variables of each method type
</emphasis>. For example:
As in Haskell 98, The class hierarchy must be acyclic. However, the definition
of "acyclic" involves only the superclass relationships. For example,
this is OK:
<programlisting>
class Coll s a where
empty :: s
insert :: s -> a -> s
</programlisting>
is not OK, because the type of <literal>empty</literal> doesn't mention
<literal>a</literal>. This rule is a consequence of Rule 1(a), above, for
types, and has the same motivation.
Sometimes, offending class declarations exhibit misunderstandings. For
example, <literal>Coll</literal> might be rewritten
class C a where {
op :: D b => a -> b -> b
}
<programlisting>
class Coll s a where
empty :: s a
insert :: s a -> a -> s a
class C a => D a where { ... }
</programlisting>
which makes the connection between the type of a collection of
<literal>a</literal>'s (namely <literal>(s a)</literal>) and the element type <literal>a</literal>.
Occasionally this really doesn't work, in which case you can split the
class like this:
<programlisting>
class CollE s where
empty :: s
class CollE s => Coll s a where
insert :: s -> a -> s
</programlisting>
Here, <literal>C</literal> is a superclass of <literal>D</literal>, but it's OK for a
class operation <literal>op</literal> of <literal>C</literal> to mention <literal>D</literal>. (It
would not be OK for <literal>D</literal> to be a superclass of <literal>C</literal>.)
</para>
</sect3>
</para>
</listitem>
</orderedlist>
</para>
<sect3 id="class-method-types">
<title>Class method types</title>
<para>
Haskell 98 prohibits class method types to mention constraints on the
class type variable, thus:
......@@ -1562,186 +1511,120 @@ class type variable, thus:
The type of <literal>elem</literal> is illegal in Haskell 98, because it
contains the constraint <literal>Eq a</literal>, constrains only the
class type variable (in this case <literal>a</literal>).
GHC lifts this restriction.
</para>
<para>
With the <option>-fglasgow-exts</option> GHC lifts this restriction.
</para>
</sect3>
</sect2>
<sect2 id="type-restrictions">
<title>Type signatures</title>
<sect3 id="functional-dependencies">
<title>Functional dependencies
</title>
<sect3><title>The context of a type signature</title>
<para> Functional dependencies are implemented as described by Mark Jones
in &ldquo;<ulink url="http://www.cse.ogi.edu/~mpj/pubs/fundeps.html">Type Classes with Functional Dependencies</ulink>&rdquo;, Mark P. Jones,
In Proceedings of the 9th European Symposium on Programming,
ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782,
.
</para>
<para>
Unlike Haskell 98, constraints in types do <emphasis>not</emphasis> have to be of
the form <emphasis>(class type-variable)</emphasis> or
<emphasis>(class (type-variable type-variable ...))</emphasis>. Thus,
these type signatures are perfectly OK
Functional dependencies are introduced by a vertical bar in the syntax of a
class declaration; e.g.
<programlisting>
g :: Eq [a] => ...
g :: Ord (T a ()) => ...
class (Monad m) => MonadState s m | m -> s where ...
class Foo a b c | a b -> c where ...
</programlisting>
There should be more documentation, but there isn't (yet). Yell if you need it.
</para>
<para>
GHC imposes the following restrictions on the constraints in a type signature.
Consider the type:
In a class declaration, all of the class type variables must be reachable (in the sense
mentioned in <xref linkend="type-restrictions"/>)
from the free variables of each method type.
For example:
<programlisting>
forall tv1..tvn (c1, ...,cn) => type
class Coll s a where
empty :: s
insert :: s -> a -> s
</programlisting>
(Here, we write the "foralls" explicitly, although the Haskell source
language omits them; in Haskell 98, all the free type variables of an
explicit source-language type signature are universally quantified,
except for the class type variables in a class declaration. However,
in GHC, you can give the foralls if you want. See <xref linkend="universal-quantification"/>).
</para>
<para>
<orderedlist>
<listitem>
<para>
<emphasis>Each universally quantified type variable
<literal>tvi</literal> must be reachable from <literal>type</literal></emphasis>.
A type variable <literal>a</literal> is "reachable" if it it appears
in the same constraint as either a type variable free in in
<literal>type</literal>, or another reachable type variable.
A value with a type that does not obey
this reachability restriction cannot be used without introducing
ambiguity; that is why the type is rejected.
Here, for example, is an illegal type:
is not OK, because the type of <literal>empty</literal> doesn't mention
<literal>a</literal>. Functional dependencies can make the type variable
reachable:
<programlisting>
forall a. Eq a => Int
class Coll s a | s -> a where
empty :: s
insert :: s -> a -> s
</programlisting>
Alternatively <literal>Coll</literal> might be rewritten
When a value with this type was used, the constraint <literal>Eq tv</literal>
would be introduced where <literal>tv</literal> is a fresh type variable, and
(in the dictionary-translation implementation) the value would be
applied to a dictionary for <literal>Eq tv</literal>. The difficulty is that we
can never know which instance of <literal>Eq</literal> to use because we never
get any more information about <literal>tv</literal>.
</para>
<para>
Note
that the reachability condition is weaker than saying that <literal>a</literal> is
functionally dependent on a type variable free in
<literal>type</literal> (see <xref
linkend="functional-dependencies"/>). The reason for this is there
might be a "hidden" dependency, in a superclass perhaps. So
"reachable" is a conservative approximation to "functionally dependent".
For example, consider:
<programlisting>
class C a b | a -> b where ...
class C a b => D a b where ...
f :: forall a b. D a b => a -> a
class Coll s a where
empty :: s a
insert :: s a -> a -> s a
</programlisting>
This is fine, because in fact <literal>a</literal> does functionally determine <literal>b</literal>
but that is not immediately apparent from <literal>f</literal>'s type.
</para>
</listitem>
<listitem>
<para>
<emphasis>Every constraint <literal>ci</literal> must mention at least one of the
universally quantified type variables <literal>tvi</literal></emphasis>.
For example, this type is OK because <literal>C a b</literal> mentions the
universally quantified type variable <literal>b</literal>:
which makes the connection between the type of a collection of
<literal>a</literal>'s (namely <literal>(s a)</literal>) and the element type <literal>a</literal>.
Occasionally this really doesn't work, in which case you can split the
class like this:
<programlisting>
forall a. C a b => burble
</programlisting>
class CollE s where
empty :: s
The next type is illegal because the constraint <literal>Eq b</literal> does not
mention <literal>a</literal>:
class CollE s => Coll s a where
insert :: s -> a -> s
</programlisting>
</para>
</sect3>
<programlisting>
forall a. Eq b => burble
</programlisting>
The reason for this restriction is milder than the other one. The
excluded types are never useful or necessary (because the offending
context doesn't need to be witnessed at this point; it can be floated
out). Furthermore, floating them out increases sharing. Lastly,
excluding them is a conservative choice; it leaves a patch of
territory free in case we need it later.
</para>
</listitem>
</sect2>
</orderedlist>
<sect2 id="instance-decls">
<title>Instance declarations</title>
</para>
</sect3>
<sect3 id="instance-heads">
<title>Instance heads</title>
<sect3 id="hoist">
<title>For-all hoisting</title>
<para>
It is often convenient to use generalised type synonyms (see <xref linkend="type-synonyms"/>) at the right hand
end of an arrow, thus:
<programlisting>
type Discard a = forall b. a -> b -> a
g :: Int -> Discard Int
g x y z = x+y
</programlisting>
Simply expanding the type synonym would give
<programlisting>
g :: Int -> (forall b. Int -> b -> Int)
</programlisting>
but GHC "hoists" the <literal>forall</literal> to give the isomorphic type
<programlisting>
g :: forall b. Int -> Int -> b -> Int
</programlisting>
In general, the rule is this: <emphasis>to determine the type specified by any explicit
user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly
performs the transformation:</emphasis>
<programlisting>
<emphasis>type1</emphasis> -> forall a1..an. <emphasis>context2</emphasis> => <emphasis>type2</emphasis>
==>
forall a1..an. <emphasis>context2</emphasis> => <emphasis>type1</emphasis> -> <emphasis>type2</emphasis>
</programlisting>
(In fact, GHC tries to retain as much synonym information as possible for use in
error messages, but that is a usability issue.) This rule applies, of course, whether
or not the <literal>forall</literal> comes from a synonym. For example, here is another
valid way to write <literal>g</literal>'s type signature:
<programlisting>
g :: Int -> Int -> forall b. b -> Int
</programlisting>
The <emphasis>head</emphasis> of an instance declaration is the part to the
right of the "<literal>=&gt;</literal>". In Haskell 98 the head of an instance
declaration
must be of the form <literal>C (T a1 ... an)</literal>, where
<literal>C</literal> is the class, <literal>T</literal> is a type constructor,
and the <literal>a1 ... an</literal> are distinct type variables.
</para>
<para>
When doing this hoisting operation, GHC eliminates duplicate constraints. For
example:
<programlisting>
type Foo a = (?x::Int) => Bool -> a
g :: Foo (Foo Int)
</programlisting>
means
The <option>-fglasgow-exts</option> flag lifts this restriction and allows the
instance head to be of form <literal>C t1 ... tn</literal> where <literal>t1
... tn</literal> are arbitrary types (provided, of course, everything is
well-kinded). In particular, types <literal>ti</literal> can be type variables
or structured types, and can contain repeated occurrences of a single type
variable.
Examples:
<programlisting>
g :: (?x::Int) => Bool -> Bool -> Int
instance Eq (T a a) where ...
-- Repeated type variable
instance Eq (S [a]) where ...
-- Structured type
instance C Int [a] where ...
-- Multiple parameters
</programlisting>
</para>
</sect3>
</sect2>
<sect2 id="instance-decls">
<title>Instance declarations</title>
<sect3 id="instance-overlap">
<title>Overlapping instances</title>
<para>
......@@ -1892,7 +1775,7 @@ but this is not:
<programlisting>
instance F a where ...
</programlisting>
Note that instance heads <emphasis>may</emphasis> contain repeated type variables.
Note that instance heads may contain repeated type variables (<xref linkend="instance-heads"/>).
For example, this is OK:
<programlisting>
instance Stateful (ST s) (MutVar s) where ...
......@@ -1979,6 +1862,174 @@ allowing these idioms interesting idioms.
</sect3>
</sect2>
<sect2 id="type-restrictions">
<title>Type signatures</title>
<sect3><title>The context of a type signature</title>
<para>
Unlike Haskell 98, constraints in types do <emphasis>not</emphasis> have to be of
the form <emphasis>(class type-variable)</emphasis> or
<emphasis>(class (type-variable type-variable ...))</emphasis>. Thus,
these type signatures are perfectly OK
<programlisting>
g :: Eq [a] => ...
g :: Ord (T a ()) => ...
</programlisting>
</para>
<para>
GHC imposes the following restrictions on the constraints in a type signature.
Consider the type:
<programlisting>
forall tv1..tvn (c1, ...,cn) => type
</programlisting>
(Here, we write the "foralls" explicitly, although the Haskell source
language omits them; in Haskell 98, all the free type variables of an
explicit source-language type signature are universally quantified,
except for the class type variables in a class declaration. However,
in GHC, you can give the foralls if you want. See <xref linkend="universal-quantification"/>).
</para>
<para>
<orderedlist>
<listitem>
<para>
<emphasis>Each universally quantified type variable
<literal>tvi</literal> must be reachable from <literal>type</literal></emphasis>.
A type variable <literal>a</literal> is "reachable" if it it appears
in the same constraint as either a type variable free in in
<literal>type</literal>, or another reachable type variable.
A value with a type that does not obey
this reachability restriction cannot be used without introducing
ambiguity; that is why the type is rejected.
Here, for example, is an illegal type:
<programlisting>
forall a. Eq a => Int
</programlisting>
When a value with this type was used, the constraint <literal>Eq tv</literal>
would be introduced where <literal>tv</literal> is a fresh type variable, and
(in the dictionary-translation implementation) the value would be
applied to a dictionary for <literal>Eq tv</literal>. The difficulty is that we
can never know which instance of <literal>Eq</literal> to use because we never
get any more information about <literal>tv</literal>.
</para>
<para>
Note
that the reachability condition is weaker than saying that <literal>a</literal> is
functionally dependent on a type variable free in
<literal>type</literal> (see <xref
linkend="functional-dependencies"/>). The reason for this is there
might be a "hidden" dependency, in a superclass perhaps. So
"reachable" is a conservative approximation to "functionally dependent".
For example, consider:
<programlisting>
class C a b | a -> b where ...
class C a b => D a b where ...
f :: forall a b. D a b => a -> a
</programlisting>
This is fine, because in fact <literal>a</literal> does functionally determine <literal>b</literal>
but that is not immediately apparent from <literal>f</literal>'s type.
</para>
</listitem>
<listitem>
<para>
<emphasis>Every constraint <literal>ci</literal> must mention at least one of the
universally quantified type variables <literal>tvi</literal></emphasis>.
For example, this type is OK because <literal>C a b</literal> mentions the
universally quantified type variable <literal>b</literal>:
<programlisting>
forall a. C a b => burble
</programlisting>
The next type is illegal because the constraint <literal>Eq b</literal> does not
mention <literal>a</literal>:
<programlisting>
forall a. Eq b => burble
</programlisting>
The reason for this restriction is milder than the other one. The
excluded types are never useful or necessary (because the offending
context doesn't need to be witnessed at this point; it can be floated
out). Furthermore, floating them out increases sharing. Lastly,
excluding them is a conservative choice; it leaves a patch of
territory free in case we need it later.
</para>
</listitem>
</orderedlist>
</para>
</sect3>
<sect3 id="hoist">
<title>For-all hoisting</title>
<para>
It is often convenient to use generalised type synonyms (see <xref linkend="type-synonyms"/>) at the right hand
end of an arrow, thus:
<programlisting>
type Discard a = forall b. a -> b -> a
g :: Int -> Discard Int
g x y z = x+y
</programlisting>
Simply expanding the type synonym would give
<programlisting>
g :: Int -> (forall b. Int -> b -> Int)
</programlisting>
but GHC "hoists" the <literal>forall</literal> to give the isomorphic type
<programlisting>
g :: forall b. Int -> Int -> b -> Int
</programlisting>
In general, the rule is this: <emphasis>to determine the type specified by any explicit
user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly
performs the transformation:</emphasis>
<programlisting>
<emphasis>type1</emphasis> -> forall a1..an. <emphasis>context2</emphasis> => <emphasis>type2</emphasis>
==>
forall a1..an. <emphasis>context2</emphasis> => <emphasis>type1</emphasis> -> <emphasis>type2</emphasis>
</programlisting>
(In fact, GHC tries to retain as much synonym information as possible for use in
error messages, but that is a usability issue.) This rule applies, of course, whether
or not the <literal>forall</literal> comes from a synonym. For example, here is another
valid way to write <literal>g</literal>'s type signature:
<programlisting>
g :: Int -> Int -> forall b. b -> Int
</programlisting>
</para>
<para>
When doing this hoisting operation, GHC eliminates duplicate constraints. For
example:
<programlisting>
type Foo a = (?x::Int) => Bool -> a
g :: Foo (Foo Int)
</programlisting>
means
<programlisting>
g :: (?x::Int) => Bool -> Bool -> Int
</programlisting>
</para>
</sect3>
</sect2>
<sect2 id="implicit-parameters">
......@@ -2378,30 +2429,6 @@ and you'd be right. That is why they are an experimental feature.
</sect2>
<sect2 id="functional-dependencies">
<title>Functional dependencies
</title>
<para> Functional dependencies are implemented as described by Mark Jones
in &ldquo;<ulink url="http://www.cse.ogi.edu/~mpj/pubs/fundeps.html">Type Classes with Functional Dependencies</ulink>&rdquo;, Mark P. Jones,
In Proceedings of the 9th European Symposium on Programming,
ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782,
.
</para>
<para>
Functional dependencies are introduced by a vertical bar in the syntax of a
class declaration; e.g.
<programlisting>
class (Monad m) => MonadState s m | m -> s where ...
class Foo a b c | a b -> c where ...
</programlisting>
There should be more documentation, but there isn't (yet). Yell if you need it.
</para>
</sect2>
<sect2 id="sec-kinding">
<title>Explicitly-kinded quantification</title>
......
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