<sect1 id="type-extensions">
<title>Type system extensions</title>
-<sect2 id="nullary-types">
+
+<sect2>
+<title>Data types and type synonyms</title>
+
+<sect3 id="nullary-types">
<title>Data types with no constructors</title>
<para>With the <option>-fglasgow-exts</option> flag, GHC lets you declare
<para>Such data types have only one value, namely bottom.
Nevertheless, they can be useful when defining "phantom types".</para>
-</sect2>
+</sect3>
-<sect2 id="infix-tycons">
+<sect3 id="infix-tycons">
<title>Infix type constructors</title>
<para>
</itemizedlist>
</para>
-</sect2>
+</sect3>
-<sect2 id="sec-kinding">
-<title>Explicitly-kinded quantification</title>
+<sect3 id="type-synonyms">
+<title>Liberalised type synonyms</title>
<para>
-Haskell infers the kind of each type variable. Sometimes it is nice to be able
-to give the kind explicitly as (machine-checked) documentation,
-just as it is nice to give a type signature for a function. On some occasions,
-it is essential to do so. For example, in his paper "Restricted Data Types in Haskell" (Haskell Workshop 1999)
-John Hughes had to define the data type:
-<Screen>
- data Set cxt a = Set [a]
- | Unused (cxt a -> ())
-</Screen>
-The only use for the <literal>Unused</literal> constructor was to force the correct
-kind for the type variable <literal>cxt</literal>.
-</para>
-<para>
-GHC now instead allows you to specify the kind of a type variable directly, wherever
-a type variable is explicitly bound. Namely:
+Type synonmys are like macros at the type level, and
+GHC does validity checking on types <emphasis>only after expanding type synonyms</emphasis>.
+That means that GHC can be very much more liberal about type synonyms than Haskell 98:
<itemizedlist>
-<listitem><para><literal>data</literal> declarations:
-<Screen>
- data Set (cxt :: * -> *) a = Set [a]
-</Screen></para></listitem>
-<listitem><para><literal>type</literal> declarations:
-<Screen>
- type T (f :: * -> *) = f Int
-</Screen></para></listitem>
-<listitem><para><literal>class</literal> declarations:
-<Screen>
- class (Eq a) => C (f :: * -> *) a where ...
-</Screen></para></listitem>
-<listitem><para><literal>forall</literal>'s in type signatures:
-<Screen>
- f :: forall (cxt :: * -> *). Set cxt Int
-</Screen></para></listitem>
-</itemizedlist>
-</para>
+<listitem> <para>You can write a <literal>forall</literal> (including overloading)
+in a type synonym, thus:
+<programlisting>
+ type Discard a = forall b. Show b => a -> b -> (a, String)
-<para>
-The parentheses are required. Some of the spaces are required too, to
-separate the lexemes. If you write <literal>(f::*->*)</literal> you
-will get a parse error, because "<literal>::*->*</literal>" is a
-single lexeme in Haskell.
-</para>
+ f :: Discard a
+ f x y = (x, show y)
-<para>
-As part of the same extension, you can put kind annotations in types
-as well. Thus:
-<Screen>
- f :: (Int :: *) -> Int
- g :: forall a. a -> (a :: *)
-</Screen>
-The syntax is
-<Screen>
- atype ::= '(' ctype '::' kind ')
-</Screen>
-The parentheses are required.
+ g :: Discard Int -> (Int,Bool) -- A rank-2 type
+ g f = f Int True
+</programlisting>
</para>
-</sect2>
+</listitem>
+<listitem><para>
+You can write an unboxed tuple in a type synonym:
+<programlisting>
+ type Pr = (# Int, Int #)
-<sect2 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:
+ h :: Int -> Pr
+ h x = (# x, x #)
+</programlisting>
+</para></listitem>
+
+<listitem><para>
+You can apply a type synonym to a forall type:
<programlisting>
- class Seq s a where
- fromList :: [a] -> s a
- elem :: Eq a => a -> s a -> Bool
+ type Foo a = a -> a -> Bool
+
+ f :: Foo (forall b. b->b)
</programlisting>
-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>).
-</para>
-<para>
-With the <option>-fglasgow-exts</option> GHC lifts this restriction.
-</para>
+After expanding the synonym, <literal>f</literal> has the legal (in GHC) type:
+<programlisting>
+ f :: (forall b. b->b) -> (forall b. b->b) -> Bool
+</programlisting>
+</para></listitem>
-</sect2>
+<listitem><para>
+You can apply a type synonym to a partially applied type synonym:
+<programlisting>
+ type Generic i o = forall x. i x -> o x
+ type Id x = x
+
+ foo :: Generic Id []
+</programlisting>
+After epxanding the synonym, <literal>foo</literal> has the legal (in GHC) type:
+<programlisting>
+ foo :: forall x. x -> [x]
+</programlisting>
+</para></listitem>
-<sect2 id="multi-param-type-classes">
-<title>Multi-parameter type classes
-</title>
+</itemizedlist>
+</para>
<para>
-This section documents GHC's implementation of multi-parameter type
-classes. There's lots of background in the paper <ULink
-URL="http://research.microsoft.com/~simonpj/multi.ps.gz" >Type
-classes: exploring the design space</ULink > (Simon Peyton Jones, Mark
-Jones, Erik Meijer).
+GHC currently does kind checking before expanding synonyms (though even that
+could be changed.)
</para>
-
-
-<sect3 id="type-restrictions">
-<title>Types</title>
-
<para>
-GHC imposes the following restrictions on the form of a qualified
-type, whether declared in a type signature
-or inferred. Consider the type:
-
+After expanding type synonyms, GHC does validity checking on types, looking for
+the following mal-formedness which isn't detected simply by kind checking:
+<itemizedlist>
+<listitem><para>
+Type constructor applied to a type involving for-alls.
+</para></listitem>
+<listitem><para>
+Unboxed tuple on left of an arrow.
+</para></listitem>
+<listitem><para>
+Partially-applied type synonym.
+</para></listitem>
+</itemizedlist>
+So, for example,
+this will be rejected:
<programlisting>
- forall tv1..tvn (c1, ...,cn) => type
-</programlisting>
+ type Pr = (# Int, Int #)
-(Here, I write the "foralls" explicitly, although the Haskell source
-language omits them; in Haskell 1.4, 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">).
+ h :: Pr -> Int
+ h x = ...
+</programlisting>
+because GHC does not allow unboxed tuples on the left of a function arrow.
</para>
+</sect3>
-<para>
-<OrderedList>
-<listitem>
+<sect3 id="existential-quantification">
+<title>Existentially quantified data constructors
+</title>
<para>
- <emphasis>Each universally quantified type variable
-<literal>tvi</literal> must be reachable from <literal>type</literal></emphasis>.
-
-A type variable is "reachable" if it it is functionally dependent
-(see <xref linkend="functional-dependencies">)
-on the type variables free in <literal>type</literal>.
-The reason for this is that a value with a type that does not obey
-this restriction could not be used without introducing
-ambiguity.
-Here, for example, is an illegal type:
+The idea of using existential quantification in data type declarations
+was suggested by Laufer (I believe, thought doubtless someone will
+correct me), and implemented in Hope+. It's been in Lennart
+Augustsson's <Command>hbc</Command> Haskell compiler for several years, and
+proved very useful. Here's the idea. Consider the declaration:
+</para>
+<para>
<programlisting>
- forall a. Eq a => Int
+ data Foo = forall a. MkFoo a (a -> Bool)
+ | Nil
</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>
-</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>:
+The data type <literal>Foo</literal> has two constructors with types:
+</para>
+<para>
<programlisting>
- forall a. C a b => burble
+ MkFoo :: forall a. a -> (a -> Bool) -> Foo
+ Nil :: Foo
</programlisting>
+</para>
-The next type is illegal because the constraint <literal>Eq b</literal> does not
-mention <literal>a</literal>:
+<para>
+Notice that the type variable <literal>a</literal> in the type of <function>MkFoo</function>
+does not appear in the data type itself, which is plain <literal>Foo</literal>.
+For example, the following expression is fine:
+</para>
+<para>
<programlisting>
- forall a. Eq b => burble
+ [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo]
</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>
+Here, <literal>(MkFoo 3 even)</literal> packages an integer with a function
+<function>even</function> that maps an integer to <literal>Bool</literal>; and <function>MkFoo 'c'
+isUpper</function> packages a character with a compatible function. These
+two things are each of type <literal>Foo</literal> and can be put in a list.
</para>
-
<para>
-Unlike Haskell 1.4, constraints in types do <emphasis>not</emphasis> have to be of
-the form <emphasis>(class type-variables)</emphasis>. Thus, these type signatures
-are perfectly OK
+What can we do with a value of type <literal>Foo</literal>?. In particular,
+what happens when we pattern-match on <function>MkFoo</function>?
</para>
<para>
<programlisting>
- f :: Eq (m a) => [m a] -> [m a]
- g :: Eq [a] => ...
+ f (MkFoo val fn) = ???
</programlisting>
</para>
<para>
-This choice recovers principal types, a property that Haskell 1.4 does not have.
+Since all we know about <literal>val</literal> and <function>fn</function> is that they
+are compatible, the only (useful) thing we can do with them is to
+apply <function>fn</function> to <literal>val</literal> to get a boolean. For example:
</para>
-</sect3>
-
-<sect3>
-<title>Class declarations</title>
-
<para>
-<OrderedList>
-<listitem>
-
-<para>
- <emphasis>Multi-parameter type classes are permitted</emphasis>. For example:
-
-
<programlisting>
- class Collection c a where
- union :: c a -> c a -> c a
- ...etc.
+ f :: Foo -> Bool
+ f (MkFoo val fn) = fn val
</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>
-
+What this allows us to do is to package heterogenous values
+together with a bunch of functions that manipulate them, and then treat
+that collection of packages in a uniform manner. You can express
+quite a bit of object-oriented-like programming this way.
+</para>
-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>.)
+<sect4 id="existential">
+<title>Why existential?
+</title>
+<para>
+What has this to do with <emphasis>existential</emphasis> quantification?
+Simply that <function>MkFoo</function> has the (nearly) isomorphic type
</para>
-</listitem>
-<listitem>
<para>
- <emphasis>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:
-
<programlisting>
- class Functor (m k) => FiniteMap m k where
- ...
-
- class (Monad m, Monad (t m)) => Transform t m where
- lift :: m a -> (t m) a
+ MkFoo :: (exists a . (a, a -> Bool)) -> Foo
</programlisting>
-
</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 varibles of each method type
-</emphasis>. For example:
-
-
-<programlisting>
- class Coll s a where
- empty :: s
- insert :: s -> a -> s
-</programlisting>
+But Haskell programmers can safely think of the ordinary
+<emphasis>universally</emphasis> quantified type given above, thereby avoiding
+adding a new existential quantification construct.
+</para>
+</sect4>
-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.
+<sect4>
+<title>Type classes</title>
-Sometimes, offending class declarations exhibit misunderstandings. For
-example, <literal>Coll</literal> might be rewritten
+<para>
+An easy extension (implemented in <Command>hbc</Command>) is to allow
+arbitrary contexts before the constructor. For example:
+</para>
+<para>
<programlisting>
- class Coll s a where
- empty :: s a
- insert :: s a -> a -> s a
+data Baz = forall a. Eq a => Baz1 a a
+ | forall b. Show b => Baz2 b (b -> b)
</programlisting>
+</para>
-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:
+<para>
+The two constructors have the types you'd expect:
+</para>
+<para>
<programlisting>
- class CollE s where
- empty :: s
-
- class CollE s => Coll s a where
- insert :: s -> a -> s
+Baz1 :: forall a. Eq a => a -> a -> Baz
+Baz2 :: forall b. Show b => b -> (b -> b) -> Baz
</programlisting>
-
</para>
-</listitem>
-
-</OrderedList>
-
-</para>
-
-</sect3>
-
-<sect3 id="instance-decls">
-<title>Instance declarations</title>
<para>
-
-<OrderedList>
-<listitem>
+But when pattern matching on <function>Baz1</function> the matched values can be compared
+for equality, and when pattern matching on <function>Baz2</function> the first matched
+value can be converted to a string (as well as applying the function to it).
+So this program is legal:
+</para>
<para>
- <emphasis>Instance declarations may not overlap</emphasis>. The two instance
-declarations
-
<programlisting>
- instance context1 => C type1 where ...
- instance context2 => C type2 where ...
+ f :: Baz -> String
+ f (Baz1 p q) | p == q = "Yes"
+ | otherwise = "No"
+ f (Baz2 v fn) = show (fn v)
</programlisting>
-
-"overlap" if <literal>type1</literal> and <literal>type2</literal> unify
-
-However, if you give the command line option
-<option>-fallow-overlapping-instances</option><indexterm><primary>-fallow-overlapping-instances
-option</primary></indexterm> then overlapping instance declarations are permitted.
-However, GHC arranges never to commit to using an instance declaration
-if another instance declaration also applies, either now or later.
-
-<itemizedlist>
-<listitem>
+</para>
<para>
- EITHER <literal>type1</literal> and <literal>type2</literal> do not unify
+Operationally, in a dictionary-passing implementation, the
+constructors <function>Baz1</function> and <function>Baz2</function> must store the
+dictionaries for <literal>Eq</literal> and <literal>Show</literal> respectively, and
+extract it on pattern matching.
</para>
-</listitem>
-<listitem>
<para>
- OR <literal>type2</literal> is a substitution instance of <literal>type1</literal>
-(but not identical to <literal>type1</literal>), or vice versa.
+Notice the way that the syntax fits smoothly with that used for
+universal quantification earlier.
</para>
-</listitem>
-</itemizedlist>
-Notice that these rules
-<itemizedlist>
-<listitem>
-<para>
- make it clear which instance decl to use
-(pick the most specific one that matches)
+</sect4>
-</para>
-</listitem>
-<listitem>
+<sect4>
+<title>Restrictions</title>
<para>
- do not mention the contexts <literal>context1</literal>, <literal>context2</literal>
-Reason: you can pick which instance decl
-"matches" based on the type.
+There are several restrictions on the ways in which existentially-quantified
+constructors can be use.
</para>
-</listitem>
-</itemizedlist>
-However the rules are over-conservative. Two instance declarations can overlap,
-but it can still be clear in particular situations which to use. For example:
-<programlisting>
- instance C (Int,a) where ...
- instance C (a,Bool) where ...
-</programlisting>
-These are rejected by GHC's rules, but it is clear what to do when trying
-to solve the constraint <literal>C (Int,Int)</literal> because the second instance
-cannot apply. Yell if this restriction bites you.
-</para>
-<para>
-GHC is also conservative about committing to an overlapping instance. For example:
-<programlisting>
- class C a where { op :: a -> a }
- instance C [Int] where ...
- instance C a => C [a] where ...
-
- f :: C b => [b] -> [b]
- f x = op x
-</programlisting>
-From the RHS of f we get the constraint <literal>C [b]</literal>. But
-GHC does not commit to the second instance declaration, because in a paricular
-call of f, b might be instantiate to Int, so the first instance declaration
-would be appropriate. So GHC rejects the program. If you add <option>-fallow-incoherent-instances</option>
-GHC will instead silently pick the second instance, without complaining about
-the problem of subsequent instantiations.
-</para>
<para>
-Regrettably, GHC doesn't guarantee to detect overlapping instance
-declarations if they appear in different modules. GHC can "see" the
-instance declarations in the transitive closure of all the modules
-imported by the one being compiled, so it can "see" all instance decls
-when it is compiling <literal>Main</literal>. However, it currently chooses not
-to look at ones that can't possibly be of use in the module currently
-being compiled, in the interests of efficiency. (Perhaps we should
-change that decision, at least for <literal>Main</literal>.)
-</para>
-</listitem>
+<itemizedlist>
<listitem>
<para>
- <emphasis>There are no restrictions on the type in an instance
-<emphasis>head</emphasis>, except that at least one must not be a type variable</emphasis>.
-The instance "head" is the bit after the "=>" in an instance decl. For
-example, these are OK:
+ When pattern matching, each pattern match introduces a new,
+distinct, type for each existential type variable. These types cannot
+be unified with any other type, nor can they escape from the scope of
+the pattern match. For example, these fragments are incorrect:
<programlisting>
- instance C Int a where ...
-
- instance D (Int, Int) where ...
-
- instance E [[a]] where ...
+f1 (MkFoo a f) = a
</programlisting>
-Note that instance heads <emphasis>may</emphasis> contain repeated type variables.
-For example, this is OK:
+Here, the type bound by <function>MkFoo</function> "escapes", because <literal>a</literal>
+is the result of <function>f1</function>. One way to see why this is wrong is to
+ask what type <function>f1</function> has:
<programlisting>
- instance Stateful (ST s) (MutVar s) where ...
+ f1 :: Foo -> a -- Weird!
</programlisting>
-See <xref linkend="undecidable-instances"> for an experimental
-extension to lift this restriction.
-</para>
-</listitem>
-<listitem>
-<para>
- <emphasis>Unlike Haskell 1.4, instance heads may use type
-synonyms</emphasis>. As always, using a type synonym is just shorthand for
-writing the RHS of the type synonym definition. For example:
+What is this "<literal>a</literal>" in the result type? Clearly we don't mean
+this:
<programlisting>
- type Point = (Int,Int)
- instance C Point where ...
- instance C [Point] where ...
+ f1 :: forall a. Foo -> a -- Wrong!
</programlisting>
-is legal. However, if you added
+The original program is just plain wrong. Here's another sort of error
<programlisting>
- instance C (Int,Int) where ...
+ f2 (Baz1 a b) (Baz1 p q) = a==q
</programlisting>
-as well, then the compiler will complain about the overlapping
-(actually, identical) instance declarations. As always, type synonyms
-must be fully applied. You cannot, for example, write:
-
-
-<programlisting>
- type P a = [[a]]
- instance Monad P where ...
-</programlisting>
-
+It's ok to say <literal>a==b</literal> or <literal>p==q</literal>, but
+<literal>a==q</literal> is wrong because it equates the two distinct types arising
+from the two <function>Baz1</function> constructors.
-This design decision is independent of all the others, and easily
-reversed, but it makes sense to me.
</para>
</listitem>
<listitem>
<para>
-<emphasis>The types in an instance-declaration <emphasis>context</emphasis> must all
-be type variables</emphasis>. Thus
+You can't pattern-match on an existentially quantified
+constructor in a <literal>let</literal> or <literal>where</literal> group of
+bindings. So this is illegal:
<programlisting>
-instance C a b => Eq (a,b) where ...
+ f3 x = a==b where { Baz1 a b = x }
</programlisting>
+Instead, use a <literal>case</literal> expression:
-is OK, but
+<programlisting>
+ f3 x = case x of Baz1 a b -> a==b
+</programlisting>
+
+In general, you can only pattern-match
+on an existentially-quantified constructor in a <literal>case</literal> expression or
+in the patterns of a function definition.
+
+The reason for this restriction is really an implementation one.
+Type-checking binding groups is already a nightmare without
+existentials complicating the picture. Also an existential pattern
+binding at the top level of a module doesn't make sense, because it's
+not clear how to prevent the existentially-quantified type "escaping".
+So for now, there's a simple-to-state restriction. We'll see how
+annoying it is.
+
+</para>
+</listitem>
+<listitem>
+
+<para>
+You can't use existential quantification for <literal>newtype</literal>
+declarations. So this is illegal:
<programlisting>
-instance C Int b => Foo b where ...
+ newtype T = forall a. Ord a => MkT a
</programlisting>
-is not OK. See <xref linkend="undecidable-instances"> for an experimental
-extension to lift this restriction.
+Reason: a value of type <literal>T</literal> must be represented as a pair
+of a dictionary for <literal>Ord t</literal> and a value of type <literal>t</literal>.
+That contradicts the idea that <literal>newtype</literal> should have no
+concrete representation. You can get just the same efficiency and effect
+by using <literal>data</literal> instead of <literal>newtype</literal>. If there is no
+overloading involved, then there is more of a case for allowing
+an existentially-quantified <literal>newtype</literal>, because the <literal>data</literal>
+because the <literal>data</literal> version does carry an implementation cost,
+but single-field existentially quantified constructors aren't much
+use. So the simple restriction (no existential stuff on <literal>newtype</literal>)
+stands, unless there are convincing reasons to change it.
+
+
+</para>
+</listitem>
+<listitem>
+<para>
+ You can't use <literal>deriving</literal> to define instances of a
+data type with existentially quantified data constructors.
+
+Reason: in most cases it would not make sense. For example:#
+
+<programlisting>
+data T = forall a. MkT [a] deriving( Eq )
+</programlisting>
+
+To derive <literal>Eq</literal> in the standard way we would need to have equality
+between the single component of two <function>MkT</function> constructors:
+<programlisting>
+instance Eq T where
+ (MkT a) == (MkT b) = ???
+</programlisting>
+But <VarName>a</VarName> and <VarName>b</VarName> have distinct types, and so can't be compared.
+It's just about possible to imagine examples in which the derived instance
+would make sense, but it seems altogether simpler simply to prohibit such
+declarations. Define your own instances!
</para>
</listitem>
-</OrderedList>
+</itemizedlist>
</para>
+</sect4>
</sect3>
</sect2>
-<sect2 id="undecidable-instances">
-<title>Undecidable instances</title>
-<para>The rules for instance declarations state that:
-<itemizedlist>
-<listitem><para>At least one of the types in the <emphasis>head</emphasis> of
-an instance declaration <emphasis>must not</emphasis> be a type variable.
-</para></listitem>
-<listitem><para>All of the types in the <emphasis>context</emphasis> of
-an instance declaration <emphasis>must</emphasis> be type variables.
-</para></listitem>
-</itemizedlist>
-These restrictions ensure that
-context reduction terminates: each reduction step removes one type
-constructor. For example, the following would make the type checker
-loop if it wasn't excluded:
+
+<sect2 id="multi-param-type-classes">
+<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
+URL="http://research.microsoft.com/~simonpj/multi.ps.gz" >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>
+
+<para>
+ <emphasis>Multi-parameter type classes are permitted</emphasis>. For example:
+
+
<programlisting>
- instance C a => C a where ...
+ class Collection c a where
+ union :: c a -> c a -> c a
+ ...etc.
</programlisting>
-There are two situations in which the rule is a bit of a pain. First,
-if one allows overlapping instance declarations then it's quite
-convenient to have a "default instance" declaration that applies if
-something more specific does not:
+
+
+
+</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>
- instance C a where
- op = ... -- Default
+ class C a where {
+ op :: D b => a -> b -> b
+ }
+
+ class C a => D a where { ... }
</programlisting>
-Second, sometimes you might want to use the following to get the
-effect of a "class synonym":
+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>
+</listitem>
+<listitem>
+
+<para>
+ <emphasis>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:
<programlisting>
- class (C1 a, C2 a, C3 a) => C a where { }
+ class Functor (m k) => FiniteMap m k where
+ ...
- instance (C1 a, C2 a, C3 a) => C a where { }
+ class (Monad m, Monad (t m)) => Transform t m where
+ lift :: m a -> (t m) a
</programlisting>
-This allows you to write shorter signatures:
+</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 varibles of each method type
+</emphasis>. For example:
<programlisting>
- f :: C a => ...
+ class Coll s a where
+ empty :: s
+ insert :: s -> a -> s
</programlisting>
-instead of
+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
<programlisting>
- f :: (C1 a, C2 a, C3 a) => ...
+ class Coll s a where
+ empty :: s a
+ insert :: s a -> a -> s a
</programlisting>
-Voluminous correspondence on the Haskell mailing list has convinced me
-that it's worth experimenting with more liberal rules. If you use
-the experimental flag <option>-fallow-undecidable-instances</option>
-<indexterm><primary>-fallow-undecidable-instances
-option</primary></indexterm>, you can use arbitrary
-types in both an instance context and instance head. Termination is ensured by having a
-fixed-depth recursion stack. If you exceed the stack depth you get a
-sort of backtrace, and the opportunity to increase the stack depth
-with <option>-fcontext-stack</option><emphasis>N</emphasis>.
-</para>
-<para>
-I'm on the lookout for a less brutal solution: a simple rule that preserves decidability while
-allowing these idioms interesting idioms.
-</para>
-</sect2>
+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>
-<sect2 id="implicit-parameters">
-<title>Implicit parameters
-</title>
-<para> Implicit paramters are implemented as described in
-"Implicit parameters: dynamic scoping with static types",
-J Lewis, MB Shields, E Meijer, J Launchbury,
-27th ACM Symposium on Principles of Programming Languages (POPL'00),
-Boston, Jan 2000.
</para>
-<para>(Most of the following, stil rather incomplete, documentation is due to Jeff Lewis.)</para>
-<para>
-A variable is called <emphasis>dynamically bound</emphasis> when it is bound by the calling
-context of a function and <emphasis>statically bound</emphasis> when bound by the callee's
-context. In Haskell, all variables are statically bound. Dynamic
-binding of variables is a notion that goes back to Lisp, but was later
-discarded in more modern incarnations, such as Scheme. Dynamic binding
-can be very confusing in an untyped language, and unfortunately, typed
-languages, in particular Hindley-Milner typed languages like Haskell,
-only support static scoping of variables.
+</listitem>
+
+</OrderedList>
</para>
+
+<sect3 id="class-method-types">
+<title>Class method types</title>
<para>
-However, by a simple extension to the type class system of Haskell, we
-can support dynamic binding. Basically, we express the use of a
-dynamically bound variable as a constraint on the type. These
-constraints lead to types of the form <literal>(?x::t') => t</literal>, which says "this
-function uses a dynamically-bound variable <literal>?x</literal>
-of type <literal>t'</literal>". For
-example, the following expresses the type of a sort function,
-implicitly parameterized by a comparison function named <literal>cmp</literal>.
+Haskell 98 prohibits class method types to mention constraints on the
+class type variable, thus:
<programlisting>
- sort :: (?cmp :: a -> a -> Bool) => [a] -> [a]
+ class Seq s a where
+ fromList :: [a] -> s a
+ elem :: Eq a => a -> s a -> Bool
</programlisting>
-The dynamic binding constraints are just a new form of predicate in the type class system.
+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>).
</para>
<para>
-An implicit parameter occurs in an expression using the special form <literal>?x</literal>,
-where <literal>x</literal> is
-any valid identifier (e.g. <literal>ord ?x</literal> is a valid expression).
-Use of this construct also introduces a new
-dynamic-binding constraint in the type of the expression.
-For example, the following definition
-shows how we can define an implicitly parameterized sort function in
-terms of an explicitly parameterized <literal>sortBy</literal> function:
-<programlisting>
- sortBy :: (a -> a -> Bool) -> [a] -> [a]
-
- sort :: (?cmp :: a -> a -> Bool) => [a] -> [a]
- sort = sortBy ?cmp
-</programlisting>
+With the <option>-fglasgow-exts</option> GHC lifts this restriction.
</para>
-<sect3>
-<title>Implicit-parameter type constraints</title>
+</sect3>
+
+</sect2>
+
+<sect2 id="type-restrictions">
+<title>Type signatures</title>
+
+<sect3><title>The context of a type signature</title>
<para>
-Dynamic binding constraints behave just like other type class
-constraints in that they are automatically propagated. Thus, when a
-function is used, its implicit parameters are inherited by the
-function that called it. For example, our <literal>sort</literal> function might be used
-to pick out the least value in a list:
+Unlike Haskell 1.4, constraints in types do <emphasis>not</emphasis> have to be of
+the form <emphasis>(class type-variables)</emphasis>. Thus, these type signatures
+are perfectly OK
<programlisting>
- least :: (?cmp :: a -> a -> Bool) => [a] -> a
- least xs = fst (sort xs)
+ f :: Eq (m a) => [m a] -> [m a]
+ g :: Eq [a] => ...
</programlisting>
-Without lifting a finger, the <literal>?cmp</literal> parameter is
-propagated to become a parameter of <literal>least</literal> as well. With explicit
-parameters, the default is that parameters must always be explicit
-propagated. With implicit parameters, the default is to always
-propagate them.
+This choice recovers principal types, a property that Haskell 1.4 does not have.
</para>
<para>
-An implicit-parameter type constraint differs from other type class constraints in the
-following way: All uses of a particular implicit parameter must have
-the same type. This means that the type of <literal>(?x, ?x)</literal>
-is <literal>(?x::a) => (a,a)</literal>, and not
-<literal>(?x::a, ?x::b) => (a, b)</literal>, as would be the case for type
-class constraints.
-</para>
+GHC imposes the following restrictions on the constraints in a type signature.
+Consider the type:
-<para> You can't have an implicit parameter in the context of a class or instance
-declaration. For example, both these declarations are illegal:
<programlisting>
- class (?x::Int) => C a where ...
- instance (?x::a) => Foo [a] where ...
+ forall tv1..tvn (c1, ...,cn) => type
</programlisting>
-Reason: exactly which implicit parameter you pick up depends on exactly where
-you invoke a function. But the ``invocation'' of instance declarations is done
-behind the scenes by the compiler, so it's hard to figure out exactly where it is done.
-Easiest thing is to outlaw the offending types.</para>
-<para>
-Implicit-parameter constraints do not cause ambiguity. For example, consider:
-<programlisting>
- f :: (?x :: [a]) => Int -> Int
- f n = n + length ?x
- g :: (Read a, Show a) => String -> String
- g s = show (read s)
-</programlisting>
-Here, <literal>g</literal> has an ambiguous type, and is rejected, but <literal>f</literal>
-is fine. The binding for <literal>?x</literal> at <literal>f</literal>'s call site is
-quite unambiguous, and fixes the type <literal>a</literal>.
+(Here, we write the "foralls" explicitly, although the Haskell source
+language omits them; in Haskell 1.4, 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>
-</sect3>
-
-<sect3>
-<title>Implicit-parameter bindings</title>
<para>
-An implicit parameter is <emphasis>bound</emphasis> using the standard
-<literal>let</literal> or <literal>where</literal> binding forms.
-For example, we define the <literal>min</literal> function by binding
-<literal>cmp</literal>.
-<programlisting>
- min :: [a] -> a
- min = let ?cmp = (<=) in least
-</programlisting>
-</para>
+
+<OrderedList>
+<listitem>
+
<para>
-A group of implicit-parameter bindings may occur anywhere a normal group of Haskell
-bindings can occur, except at top level. That is, they can occur in a <literal>let</literal>
-(including in a list comprehension, or do-notation, or pattern guards),
-or a <literal>where</literal> clause.
-Note the following points:
-<itemizedlist>
-<listitem><para>
-An implicit-parameter binding group must be a
-collection of simple bindings to implicit-style variables (no
-function-style bindings, and no type signatures); these bindings are
-neither polymorphic or recursive.
-</para></listitem>
-<listitem><para>
-You may not mix implicit-parameter bindings with ordinary bindings in a
-single <literal>let</literal>
-expression; use two nested <literal>let</literal>s instead.
-(In the case of <literal>where</literal> you are stuck, since you can't nest <literal>where</literal> clauses.)
-</para></listitem>
+ <emphasis>Each universally quantified type variable
+<literal>tvi</literal> must be reachable from <literal>type</literal></emphasis>.
+
+A type variable is "reachable" if it it is functionally dependent
+(see <xref linkend="functional-dependencies">)
+on the type variables free in <literal>type</literal>.
+The reason for this is that a value with a type that does not obey
+this restriction could not be used without introducing
+ambiguity.
+Here, for example, is an illegal type:
+
-<listitem><para>
-You may put multiple implicit-parameter bindings in a
-single binding group; but they are <emphasis>not</emphasis> treated
-as a mutually recursive group (as ordinary <literal>let</literal> bindings are).
-Instead they are treated as a non-recursive group, simultaneously binding all the implicit
-parameter. The bindings are not nested, and may be re-ordered without changing
-the meaning of the program.
-For example, consider:
-<programlisting>
- f t = let { ?x = t; ?y = ?x+(1::Int) } in ?x + ?y
-</programlisting>
-The use of <literal>?x</literal> in the binding for <literal>?y</literal> does not "see"
-the binding for <literal>?x</literal>, so the type of <literal>f</literal> is
<programlisting>
- f :: (?x::Int) => Int -> Int
+ forall a. Eq a => Int
</programlisting>
-</para></listitem>
-</itemizedlist>
-</para>
-</sect3>
-</sect2>
-<sect2 id="linear-implicit-parameters">
-<title>Linear implicit parameters
-</title>
-<para>
-Linear implicit parameters are an idea developed by Koen Claessen,
-Mark Shields, and Simon PJ. They address the long-standing
-problem that monads seem over-kill for certain sorts of problem, notably:
-</para>
-<itemizedlist>
-<listitem> <para> distributing a supply of unique names </para> </listitem>
-<listitem> <para> distributing a suppply of random numbers </para> </listitem>
-<listitem> <para> distributing an oracle (as in QuickCheck) </para> </listitem>
-</itemizedlist>
+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>
-Linear implicit parameters are just like ordinary implicit parameters,
-except that they are "linear" -- that is, they cannot be copied, and
-must be explicitly "split" instead. Linear implicit parameters are
-written '<literal>%x</literal>' instead of '<literal>?x</literal>'.
-(The '/' in the '%' suggests the split!)
</para>
-<para>
-For example:
-<programlisting>
- import GHC.Exts( Splittable )
+</listitem>
+<listitem>
- data NameSupply = ...
-
- splitNS :: NameSupply -> (NameSupply, NameSupply)
- newName :: NameSupply -> Name
+<para>
+ <emphasis>Every constraint <literal>ci</literal> must mention at least one of the
+universally quantified type variables <literal>tvi</literal></emphasis>.
- instance Splittable NameSupply where
- split = splitNS
+For example, this type is OK because <literal>C a b</literal> mentions the
+universally quantified type variable <literal>b</literal>:
- f :: (%ns :: NameSupply) => Env -> Expr -> Expr
- f env (Lam x e) = Lam x' (f env e)
- where
- x' = newName %ns
- env' = extend env x x'
- ...more equations for f...
-</programlisting>
-Notice that the implicit parameter %ns is consumed
-<itemizedlist>
-<listitem> <para> once by the call to <literal>newName</literal> </para> </listitem>
-<listitem> <para> once by the recursive call to <literal>f</literal> </para></listitem>
-</itemizedlist>
-</para>
-<para>
-So the translation done by the type checker makes
-the parameter explicit:
-<programlisting>
- f :: NameSupply -> Env -> Expr -> Expr
- f ns env (Lam x e) = Lam x' (f ns1 env e)
- where
- (ns1,ns2) = splitNS ns
- x' = newName ns2
- env = extend env x x'
-</programlisting>
-Notice the call to 'split' introduced by the type checker.
-How did it know to use 'splitNS'? Because what it really did
-was to introduce a call to the overloaded function 'split',
-defined by the class <literal>Splittable</literal>:
-<programlisting>
- class Splittable a where
- split :: a -> (a,a)
-</programlisting>
-The instance for <literal>Splittable NameSupply</literal> tells GHC how to implement
-split for name supplies. But we can simply write
<programlisting>
- g x = (x, %ns, %ns)
+ forall a. C a b => burble
</programlisting>
-and GHC will infer
+
+
+The next type is illegal because the constraint <literal>Eq b</literal> does not
+mention <literal>a</literal>:
+
+
<programlisting>
- g :: (Splittable a, %ns :: a) => b -> (b,a,a)
+ forall a. Eq b => burble
</programlisting>
-The <literal>Splittable</literal> class is built into GHC. It's exported by module
-<literal>GHC.Exts</literal>.
+
+
+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>
-<para>
-Other points:
-<itemizedlist>
-<listitem> <para> '<literal>?x</literal>' and '<literal>%x</literal>'
-are entirely distinct implicit parameters: you
- can use them together and they won't intefere with each other. </para>
</listitem>
-<listitem> <para> You can bind linear implicit parameters in 'with' clauses. </para> </listitem>
+</OrderedList>
-<listitem> <para>You cannot have implicit parameters (whether linear or not)
- in the context of a class or instance declaration. </para></listitem>
-</itemizedlist>
</para>
+</sect3>
-<sect3><title>Warnings</title>
-
+<sect3 id="hoist">
+<title>For-all hoisting</title>
<para>
-The monomorphism restriction is even more important than usual.
-Consider the example above:
+It is often convenient to use generalised type synonyms (see <xref linkend="type-synonyms">) at the right hand
+end of an arrow, thus:
<programlisting>
- f :: (%ns :: NameSupply) => Env -> Expr -> Expr
- f env (Lam x e) = Lam x' (f env e)
- where
- x' = newName %ns
- env' = extend env x x'
+ type Discard a = forall b. a -> b -> a
+
+ g :: Int -> Discard Int
+ g x y z = x+y
</programlisting>
-If we replaced the two occurrences of x' by (newName %ns), which is
-usually a harmless thing to do, we get:
+Simply expanding the type synonym would give
<programlisting>
- f :: (%ns :: NameSupply) => Env -> Expr -> Expr
- f env (Lam x e) = Lam (newName %ns) (f env e)
- where
- env' = extend env x (newName %ns)
+ g :: Int -> (forall b. Int -> b -> Int)
</programlisting>
-But now the name supply is consumed in <emphasis>three</emphasis> places
-(the two calls to newName,and the recursive call to f), so
-the result is utterly different. Urk! We don't even have
-the beta rule.
-</para>
-<para>
-Well, this is an experimental change. With implicit
-parameters we have already lost beta reduction anyway, and
-(as John Launchbury puts it) we can't sensibly reason about
-Haskell programs without knowing their typing.
-</para>
-
-</sect3>
-
-<sect3><title>Recursive functions</title>
-<para>Linear implicit parameters can be particularly tricky when you have a recursive function
-Consider
+but GHC "hoists" the <literal>forall</literal> to give the isomorphic type
<programlisting>
- foo :: %x::T => Int -> [Int]
- foo 0 = []
- foo n = %x : foo (n-1)
+ g :: forall b. Int -> Int -> b -> Int
</programlisting>
-where T is some type in class Splittable.</para>
-<para>
-Do you get a list of all the same T's or all different T's
-(assuming that split gives two distinct T's back)?
-</para><para>
-If you supply the type signature, taking advantage of polymorphic
-recursion, you get what you'd probably expect. Here's the
-translated term, where the implicit param is made explicit:
+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>
- foo x 0 = []
- foo x n = let (x1,x2) = split x
- in x1 : foo x2 (n-1)
+ type Foo a = (?x::Int) => Bool -> a
+ g :: Foo (Foo Int)
</programlisting>
-But if you don't supply a type signature, GHC uses the Hindley
-Milner trick of using a single monomorphic instance of the function
-for the recursive calls. That is what makes Hindley Milner type inference
-work. So the translation becomes
+means
<programlisting>
- foo x = let
- foom 0 = []
- foom n = x : foom (n-1)
- in
- foom
+ g :: (?x::Int) => Bool -> Bool -> Int
</programlisting>
-Result: 'x' is not split, and you get a list of identical T's. So the
-semantics of the program depends on whether or not foo has a type signature.
-Yikes!
-</para><para>
-You may say that this is a good reason to dislike linear implicit parameters
-and you'd be right. That is why they are an experimental feature.
</para>
</sect3>
+
</sect2>
-<sect2 id="functional-dependencies">
-<title>Functional dependencies
-</title>
+<sect2 id="instance-decls">
+<title>Instance declarations</title>
-<para> Functional dependencies are implemented as described by Mark Jones
-in “<ulink url="http://www.cse.ogi.edu/~mpj/pubs/fundeps.html">Type Classes with Functional Dependencies</ulink>”, Mark P. Jones,
-In Proceedings of the 9th European Symposium on Programming,
-ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782,
-.
-</para>
+<sect3>
+<title>Overlapping instances</title>
<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 ...
+In general, <emphasis>instance declarations may not overlap</emphasis>. The two instance
+declarations
- class Foo a b c | a b -> c where ...
+
+<programlisting>
+ instance context1 => C type1 where ...
+ instance context2 => C type2 where ...
</programlisting>
-There should be more documentation, but there isn't (yet). Yell if you need it.
-</para>
-</sect2>
-<sect2 id="universal-quantification">
-<title>Arbitrary-rank polymorphism
-</title>
+"overlap" if <literal>type1</literal> and <literal>type2</literal> unify
+
+However, if you give the command line option
+<option>-fallow-overlapping-instances</option><indexterm><primary>-fallow-overlapping-instances
+option</primary></indexterm> then overlapping instance declarations are permitted.
+However, GHC arranges never to commit to using an instance declaration
+if another instance declaration also applies, either now or later.
+
+<itemizedlist>
+<listitem>
<para>
-Haskell type signatures are implicitly quantified. The new keyword <literal>forall</literal>
-allows us to say exactly what this means. For example:
+ EITHER <literal>type1</literal> and <literal>type2</literal> do not unify
</para>
+</listitem>
+<listitem>
+
<para>
-<programlisting>
- g :: b -> b
-</programlisting>
-means this:
-<programlisting>
- g :: forall b. (b -> b)
-</programlisting>
-The two are treated identically.
+ OR <literal>type2</literal> is a substitution instance of <literal>type1</literal>
+(but not identical to <literal>type1</literal>), or vice versa.
</para>
+</listitem>
+</itemizedlist>
+Notice that these rules
+<itemizedlist>
+<listitem>
<para>
-However, GHC's type system supports <emphasis>arbitrary-rank</emphasis>
-explicit universal quantification in
-types.
-For example, all the following types are legal:
-<programlisting>
- f1 :: forall a b. a -> b -> a
- g1 :: forall a b. (Ord a, Eq b) => a -> b -> a
-
- f2 :: (forall a. a->a) -> Int -> Int
- g2 :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int
+ make it clear which instance decl to use
+(pick the most specific one that matches)
- f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool
-</programlisting>
-Here, <literal>f1</literal> and <literal>g1</literal> are rank-1 types, and
-can be written in standard Haskell (e.g. <literal>f1 :: a->b->a</literal>).
-The <literal>forall</literal> makes explicit the universal quantification that
-is implicitly added by Haskell.
</para>
+</listitem>
+<listitem>
+
<para>
-The functions <literal>f2</literal> and <literal>g2</literal> have rank-2 types;
-the <literal>forall</literal> is on the left of a function arrrow. As <literal>g2</literal>
-shows, the polymorphic type on the left of the function arrow can be overloaded.
+ do not mention the contexts <literal>context1</literal>, <literal>context2</literal>
+Reason: you can pick which instance decl
+"matches" based on the type.
</para>
-<para>
-The functions <literal>f3</literal> and <literal>g3</literal> have rank-3 types;
-they have rank-2 types on the left of a function arrow.
+</listitem>
+
+</itemizedlist>
+However the rules are over-conservative. Two instance declarations can overlap,
+but it can still be clear in particular situations which to use. For example:
+<programlisting>
+ instance C (Int,a) where ...
+ instance C (a,Bool) where ...
+</programlisting>
+These are rejected by GHC's rules, but it is clear what to do when trying
+to solve the constraint <literal>C (Int,Int)</literal> because the second instance
+cannot apply. Yell if this restriction bites you.
</para>
<para>
-GHC allows types of arbitrary rank; you can nest <literal>forall</literal>s
-arbitrarily deep in function arrows. (GHC used to be restricted to rank 2, but
-that restriction has now been lifted.)
-In particular, a forall-type (also called a "type scheme"),
-including an operational type class context, is legal:
-<itemizedlist>
-<listitem> <para> On the left of a function arrow </para> </listitem>
-<listitem> <para> On the right of a function arrow (see <xref linkend="hoist">) </para> </listitem>
-<listitem> <para> As the argument of a constructor, or type of a field, in a data type declaration. For
-example, any of the <literal>f1,f2,f3,g1,g2,g3</literal> above would be valid
-field type signatures.</para> </listitem>
-<listitem> <para> As the type of an implicit parameter </para> </listitem>
-<listitem> <para> In a pattern type signature (see <xref linkend="scoped-type-variables">) </para> </listitem>
-</itemizedlist>
-There is one place you cannot put a <literal>forall</literal>:
-you cannot instantiate a type variable with a forall-type. So you cannot
-make a forall-type the argument of a type constructor. So these types are illegal:
+GHC is also conservative about committing to an overlapping instance. For example:
<programlisting>
- x1 :: [forall a. a->a]
- x2 :: (forall a. a->a, Int)
- x3 :: Maybe (forall a. a->a)
+ class C a where { op :: a -> a }
+ instance C [Int] where ...
+ instance C a => C [a] where ...
+
+ f :: C b => [b] -> [b]
+ f x = op x
</programlisting>
-Of course <literal>forall</literal> becomes a keyword; you can't use <literal>forall</literal> as
-a type variable any more!
+From the RHS of f we get the constraint <literal>C [b]</literal>. But
+GHC does not commit to the second instance declaration, because in a paricular
+call of f, b might be instantiate to Int, so the first instance declaration
+would be appropriate. So GHC rejects the program. If you add <option>-fallow-incoherent-instances</option>
+GHC will instead silently pick the second instance, without complaining about
+the problem of subsequent instantiations.
</para>
-
-
-<sect3 id="univ">
-<title>Examples
-</title>
-
<para>
-In a <literal>data</literal> or <literal>newtype</literal> declaration one can quantify
-the types of the constructor arguments. Here are several examples:
+Regrettably, GHC doesn't guarantee to detect overlapping instance
+declarations if they appear in different modules. GHC can "see" the
+instance declarations in the transitive closure of all the modules
+imported by the one being compiled, so it can "see" all instance decls
+when it is compiling <literal>Main</literal>. However, it currently chooses not
+to look at ones that can't possibly be of use in the module currently
+being compiled, in the interests of efficiency. (Perhaps we should
+change that decision, at least for <literal>Main</literal>.)
</para>
+</sect3>
+
+<sect3>
+<title>Type synonyms in the instance head</title>
<para>
+<emphasis>Unlike Haskell 1.4, instance heads may use type
+synonyms</emphasis>. (The instance "head" is the bit after the "=>" in an instance decl.)
+As always, using a type synonym is just shorthand for
+writing the RHS of the type synonym definition. For example:
+
<programlisting>
-data T a = T1 (forall b. b -> b -> b) a
+ type Point = (Int,Int)
+ instance C Point where ...
+ instance C [Point] where ...
+</programlisting>
-data MonadT m = MkMonad { return :: forall a. a -> m a,
- bind :: forall a b. m a -> (a -> m b) -> m b
- }
-newtype Swizzle = MkSwizzle (Ord a => [a] -> [a])
+is legal. However, if you added
+
+
+<programlisting>
+ instance C (Int,Int) where ...
</programlisting>
-</para>
-<para>
-The constructors have rank-2 types:
-</para>
+as well, then the compiler will complain about the overlapping
+(actually, identical) instance declarations. As always, type synonyms
+must be fully applied. You cannot, for example, write:
-<para>
<programlisting>
-T1 :: forall a. (forall b. b -> b -> b) -> a -> T a
-MkMonad :: forall m. (forall a. a -> m a)
- -> (forall a b. m a -> (a -> m b) -> m b)
- -> MonadT m
-MkSwizzle :: (Ord a => [a] -> [a]) -> Swizzle
+ type P a = [[a]]
+ instance Monad P where ...
</programlisting>
+
+This design decision is independent of all the others, and easily
+reversed, but it makes sense to me.
+
</para>
+</sect3>
-<para>
-Notice that you don't need to use a <literal>forall</literal> if there's an
-explicit context. For example in the first argument of the
-constructor <function>MkSwizzle</function>, an implicit "<literal>forall a.</literal>" is
-prefixed to the argument type. The implicit <literal>forall</literal>
-quantifies all type variables that are not already in scope, and are
-mentioned in the type quantified over.
+<sect3 id="undecidable-instances">
+<title>Undecidable instances</title>
+
+<para>An instance declaration must normally obey the following rules:
+<orderedlist>
+<listitem><para>At least one of the types in the <emphasis>head</emphasis> of
+an instance declaration <emphasis>must not</emphasis> be a type variable.
+For example, these are OK:
+
+<programlisting>
+ instance C Int a where ...
+
+ instance D (Int, Int) where ...
+
+ instance E [[a]] where ...
+</programlisting>
+but this is not:
+<programlisting>
+ instance F a where ...
+</programlisting>
+Note that instance heads <emphasis>may</emphasis> contain repeated type variables.
+For example, this is OK:
+<programlisting>
+ instance Stateful (ST s) (MutVar s) where ...
+</programlisting>
</para>
+</listitem>
-<para>
-As for type signatures, implicit quantification happens for non-overloaded
-types too. So if you write this:
+<listitem>
+<para>All of the types in the <emphasis>context</emphasis> of
+an instance declaration <emphasis>must</emphasis> be type variables.
+Thus
+<programlisting>
+instance C a b => Eq (a,b) where ...
+</programlisting>
+is OK, but
+<programlisting>
+instance C Int b => Foo b where ...
+</programlisting>
+is not OK.
+</para>
+</listitem>
+</OrderedList>
+These restrictions ensure that
+context reduction terminates: each reduction step removes one type
+constructor. For example, the following would make the type checker
+loop if it wasn't excluded:
<programlisting>
- data T a = MkT (Either a b) (b -> b)
+ instance C a => C a where ...
</programlisting>
+There are two situations in which the rule is a bit of a pain. First,
+if one allows overlapping instance declarations then it's quite
+convenient to have a "default instance" declaration that applies if
+something more specific does not:
-it's just as if you had written this:
<programlisting>
- data T a = MkT (forall b. Either a b) (forall b. b -> b)
+ instance C a where
+ op = ... -- Default
</programlisting>
-That is, since the type variable <literal>b</literal> isn't in scope, it's
-implicitly universally quantified. (Arguably, it would be better
-to <emphasis>require</emphasis> explicit quantification on constructor arguments
-where that is what is wanted. Feedback welcomed.)
-</para>
-<para>
-You construct values of types <literal>T1, MonadT, Swizzle</literal> by applying
-the constructor to suitable values, just as usual. For example,
-</para>
+Second, sometimes you might want to use the following to get the
+effect of a "class synonym":
-<para>
<programlisting>
- a1 :: T Int
- a1 = T1 (\xy->x) 3
-
- a2, a3 :: Swizzle
- a2 = MkSwizzle sort
- a3 = MkSwizzle reverse
-
- a4 :: MonadT Maybe
- a4 = let r x = Just x
- b m k = case m of
- Just y -> k y
- Nothing -> Nothing
- in
- MkMonad r b
+ class (C1 a, C2 a, C3 a) => C a where { }
- mkTs :: (forall b. b -> b -> b) -> a -> [T a]
- mkTs f x y = [T1 f x, T1 f y]
+ instance (C1 a, C2 a, C3 a) => C a where { }
</programlisting>
-</para>
-
-<para>
-The type of the argument can, as usual, be more general than the type
-required, as <literal>(MkSwizzle reverse)</literal> shows. (<function>reverse</function>
-does not need the <literal>Ord</literal> constraint.)
-</para>
-<para>
-When you use pattern matching, the bound variables may now have
-polymorphic types. For example:
-</para>
+This allows you to write shorter signatures:
-<para>
<programlisting>
- f :: T a -> a -> (a, Char)
- f (T1 w k) x = (w k x, w 'c' 'd')
+ f :: C a => ...
+</programlisting>
- g :: (Ord a, Ord b) => Swizzle -> [a] -> (a -> b) -> [b]
- g (MkSwizzle s) xs f = s (map f (s xs))
- h :: MonadT m -> [m a] -> m [a]
- h m [] = return m []
- h m (x:xs) = bind m x $ \y ->
- bind m (h m xs) $ \ys ->
- return m (y:ys)
+instead of
+
+
+<programlisting>
+ f :: (C1 a, C2 a, C3 a) => ...
</programlisting>
-</para>
+Voluminous correspondence on the Haskell mailing list has convinced me
+that it's worth experimenting with more liberal rules. If you use
+the experimental flag <option>-fallow-undecidable-instances</option>
+<indexterm><primary>-fallow-undecidable-instances
+option</primary></indexterm>, you can use arbitrary
+types in both an instance context and instance head. Termination is ensured by having a
+fixed-depth recursion stack. If you exceed the stack depth you get a
+sort of backtrace, and the opportunity to increase the stack depth
+with <option>-fcontext-stack</option><emphasis>N</emphasis>.
+</para>
<para>
-In the function <function>h</function> we use the record selectors <literal>return</literal>
-and <literal>bind</literal> to extract the polymorphic bind and return functions
-from the <literal>MonadT</literal> data structure, rather than using pattern
-matching.
+I'm on the lookout for a less brutal solution: a simple rule that preserves decidability while
+allowing these idioms interesting idioms.
</para>
</sect3>
-<sect3>
-<title>Type inference</title>
-<para>
-In general, type inference for arbitrary-rank types is undecideable.
-GHC uses an algorithm proposed by Odersky and Laufer ("Putting type annotations to work", POPL'96)
-to get a decidable algorithm by requiring some help from the programmer.
-We do not yet have a formal specification of "some help" but the rule is this:
+</sect2>
+
+<sect2 id="implicit-parameters">
+<title>Implicit parameters</title>
+
+<para> Implicit paramters are implemented as described in
+"Implicit parameters: dynamic scoping with static types",
+J Lewis, MB Shields, E Meijer, J Launchbury,
+27th ACM Symposium on Principles of Programming Languages (POPL'00),
+Boston, Jan 2000.
</para>
+<para>(Most of the following, stil rather incomplete, documentation is due to Jeff Lewis.)</para>
<para>
-<emphasis>For a lambda-bound or case-bound variable, x, either the programmer
-provides an explicit polymorphic type for x, or GHC's type inference will assume
-that x's type has no foralls in it</emphasis>.
+A variable is called <emphasis>dynamically bound</emphasis> when it is bound by the calling
+context of a function and <emphasis>statically bound</emphasis> when bound by the callee's
+context. In Haskell, all variables are statically bound. Dynamic
+binding of variables is a notion that goes back to Lisp, but was later
+discarded in more modern incarnations, such as Scheme. Dynamic binding
+can be very confusing in an untyped language, and unfortunately, typed
+languages, in particular Hindley-Milner typed languages like Haskell,
+only support static scoping of variables.
</para>
<para>
-What does it mean to "provide" an explicit type for x? You can do that by
-giving a type signature for x directly, using a pattern type signature
-(<xref linkend="scoped-type-variables">), thus:
-<programlisting>
- \ f :: (forall a. a->a) -> (f True, f 'c')
-</programlisting>
-Alternatively, you can give a type signature to the enclosing
-context, which GHC can "push down" to find the type for the variable:
-<programlisting>
- (\ f -> (f True, f 'c')) :: (forall a. a->a) -> (Bool,Char)
-</programlisting>
-Here the type signature on the expression can be pushed inwards
-to give a type signature for f. Similarly, and more commonly,
-one can give a type signature for the function itself:
-<programlisting>
- h :: (forall a. a->a) -> (Bool,Char)
- h f = (f True, f 'c')
-</programlisting>
-You don't need to give a type signature if the lambda bound variable
-is a constructor argument. Here is an example we saw earlier:
+However, by a simple extension to the type class system of Haskell, we
+can support dynamic binding. Basically, we express the use of a
+dynamically bound variable as a constraint on the type. These
+constraints lead to types of the form <literal>(?x::t') => t</literal>, which says "this
+function uses a dynamically-bound variable <literal>?x</literal>
+of type <literal>t'</literal>". For
+example, the following expresses the type of a sort function,
+implicitly parameterized by a comparison function named <literal>cmp</literal>.
<programlisting>
- f :: T a -> a -> (a, Char)
- f (T1 w k) x = (w k x, w 'c' 'd')
+ sort :: (?cmp :: a -> a -> Bool) => [a] -> [a]
</programlisting>
-Here we do not need to give a type signature to <literal>w</literal>, because
-it is an argument of constructor <literal>T1</literal> and that tells GHC all
-it needs to know.
+The dynamic binding constraints are just a new form of predicate in the type class system.
</para>
-
-</sect3>
-
-
-<sect3 id="implicit-quant">
-<title>Implicit quantification</title>
-
<para>
-GHC performs implicit quantification as follows. <emphasis>At the top level (only) of
-user-written types, if and only if there is no explicit <literal>forall</literal>,
-GHC finds all the type variables mentioned in the type that are not already
-in scope, and universally quantifies them.</emphasis> For example, the following pairs are
-equivalent:
+An implicit parameter occurs in an expression using the special form <literal>?x</literal>,
+where <literal>x</literal> is
+any valid identifier (e.g. <literal>ord ?x</literal> is a valid expression).
+Use of this construct also introduces a new
+dynamic-binding constraint in the type of the expression.
+For example, the following definition
+shows how we can define an implicitly parameterized sort function in
+terms of an explicitly parameterized <literal>sortBy</literal> function:
<programlisting>
- f :: a -> a
- f :: forall a. a -> a
+ sortBy :: (a -> a -> Bool) -> [a] -> [a]
- g (x::a) = let
- h :: a -> b -> b
- h x y = y
- in ...
- g (x::a) = let
- h :: forall b. a -> b -> b
- h x y = y
- in ...
+ sort :: (?cmp :: a -> a -> Bool) => [a] -> [a]
+ sort = sortBy ?cmp
</programlisting>
</para>
+
+<sect3>
+<title>Implicit-parameter type constraints</title>
<para>
-Notice that GHC does <emphasis>not</emphasis> find the innermost possible quantification
-point. For example:
+Dynamic binding constraints behave just like other type class
+constraints in that they are automatically propagated. Thus, when a
+function is used, its implicit parameters are inherited by the
+function that called it. For example, our <literal>sort</literal> function might be used
+to pick out the least value in a list:
<programlisting>
- f :: (a -> a) -> Int
- -- MEANS
- f :: forall a. (a -> a) -> Int
- -- NOT
- f :: (forall a. a -> a) -> Int
-
-
- g :: (Ord a => a -> a) -> Int
- -- MEANS the illegal type
- g :: forall a. (Ord a => a -> a) -> Int
- -- NOT
- g :: (forall a. Ord a => a -> a) -> Int
+ least :: (?cmp :: a -> a -> Bool) => [a] -> a
+ least xs = fst (sort xs)
</programlisting>
-The latter produces an illegal type, which you might think is silly,
-but at least the rule is simple. If you want the latter type, you
-can write your for-alls explicitly. Indeed, doing so is strongly advised
-for rank-2 types.
+Without lifting a finger, the <literal>?cmp</literal> parameter is
+propagated to become a parameter of <literal>least</literal> as well. With explicit
+parameters, the default is that parameters must always be explicit
+propagated. With implicit parameters, the default is to always
+propagate them.
+</para>
+<para>
+An implicit-parameter type constraint differs from other type class constraints in the
+following way: All uses of a particular implicit parameter must have
+the same type. This means that the type of <literal>(?x, ?x)</literal>
+is <literal>(?x::a) => (a,a)</literal>, and not
+<literal>(?x::a, ?x::b) => (a, b)</literal>, as would be the case for type
+class constraints.
</para>
-</sect3>
-</sect2>
-
-<sect2 id="type-synonyms">
-<title>Liberalised type synonyms
-</title>
+<para> You can't have an implicit parameter in the context of a class or instance
+declaration. For example, both these declarations are illegal:
+<programlisting>
+ class (?x::Int) => C a where ...
+ instance (?x::a) => Foo [a] where ...
+</programlisting>
+Reason: exactly which implicit parameter you pick up depends on exactly where
+you invoke a function. But the ``invocation'' of instance declarations is done
+behind the scenes by the compiler, so it's hard to figure out exactly where it is done.
+Easiest thing is to outlaw the offending types.</para>
<para>
-Type synonmys are like macros at the type level, and
-GHC does validity checking on types <emphasis>only after expanding type synonyms</emphasis>.
-That means that GHC can be very much more liberal about type synonyms than Haskell 98:
-<itemizedlist>
-<listitem> <para>You can write a <literal>forall</literal> (including overloading)
-in a type synonym, thus:
+Implicit-parameter constraints do not cause ambiguity. For example, consider:
<programlisting>
- type Discard a = forall b. Show b => a -> b -> (a, String)
-
- f :: Discard a
- f x y = (x, show y)
+ f :: (?x :: [a]) => Int -> Int
+ f n = n + length ?x
- g :: Discard Int -> (Int,Bool) -- A rank-2 type
- g f = f Int True
+ g :: (Read a, Show a) => String -> String
+ g s = show (read s)
</programlisting>
+Here, <literal>g</literal> has an ambiguous type, and is rejected, but <literal>f</literal>
+is fine. The binding for <literal>?x</literal> at <literal>f</literal>'s call site is
+quite unambiguous, and fixes the type <literal>a</literal>.
</para>
-</listitem>
+</sect3>
-<listitem><para>
-You can write an unboxed tuple in a type synonym:
-<programlisting>
- type Pr = (# Int, Int #)
+<sect3>
+<title>Implicit-parameter bindings</title>
- h :: Int -> Pr
- h x = (# x, x #)
+<para>
+An implicit parameter is <emphasis>bound</emphasis> using the standard
+<literal>let</literal> or <literal>where</literal> binding forms.
+For example, we define the <literal>min</literal> function by binding
+<literal>cmp</literal>.
+<programlisting>
+ min :: [a] -> a
+ min = let ?cmp = (<=) in least
</programlisting>
+</para>
+<para>
+A group of implicit-parameter bindings may occur anywhere a normal group of Haskell
+bindings can occur, except at top level. That is, they can occur in a <literal>let</literal>
+(including in a list comprehension, or do-notation, or pattern guards),
+or a <literal>where</literal> clause.
+Note the following points:
+<itemizedlist>
+<listitem><para>
+An implicit-parameter binding group must be a
+collection of simple bindings to implicit-style variables (no
+function-style bindings, and no type signatures); these bindings are
+neither polymorphic or recursive.
</para></listitem>
-
<listitem><para>
-You can apply a type synonym to a forall type:
-<programlisting>
- type Foo a = a -> a -> Bool
-
- f :: Foo (forall b. b->b)
-</programlisting>
-After expanding the synonym, <literal>f</literal> has the legal (in GHC) type:
-<programlisting>
- f :: (forall b. b->b) -> (forall b. b->b) -> Bool
-</programlisting>
+You may not mix implicit-parameter bindings with ordinary bindings in a
+single <literal>let</literal>
+expression; use two nested <literal>let</literal>s instead.
+(In the case of <literal>where</literal> you are stuck, since you can't nest <literal>where</literal> clauses.)
</para></listitem>
<listitem><para>
-You can apply a type synonym to a partially applied type synonym:
+You may put multiple implicit-parameter bindings in a
+single binding group; but they are <emphasis>not</emphasis> treated
+as a mutually recursive group (as ordinary <literal>let</literal> bindings are).
+Instead they are treated as a non-recursive group, simultaneously binding all the implicit
+parameter. The bindings are not nested, and may be re-ordered without changing
+the meaning of the program.
+For example, consider:
<programlisting>
- type Generic i o = forall x. i x -> o x
- type Id x = x
-
- foo :: Generic Id []
+ f t = let { ?x = t; ?y = ?x+(1::Int) } in ?x + ?y
</programlisting>
-After epxanding the synonym, <literal>foo</literal> has the legal (in GHC) type:
+The use of <literal>?x</literal> in the binding for <literal>?y</literal> does not "see"
+the binding for <literal>?x</literal>, so the type of <literal>f</literal> is
<programlisting>
- foo :: forall x. x -> [x]
+ f :: (?x::Int) => Int -> Int
</programlisting>
</para></listitem>
-
</itemizedlist>
</para>
+</sect3>
+</sect2>
+
+<sect2 id="linear-implicit-parameters">
+<title>Linear implicit parameters</title>
<para>
-GHC currently does kind checking before expanding synonyms (though even that
-could be changed.)
+Linear implicit parameters are an idea developed by Koen Claessen,
+Mark Shields, and Simon PJ. They address the long-standing
+problem that monads seem over-kill for certain sorts of problem, notably:
</para>
-<para>
-After expanding type synonyms, GHC does validity checking on types, looking for
-the following mal-formedness which isn't detected simply by kind checking:
<itemizedlist>
-<listitem><para>
-Type constructor applied to a type involving for-alls.
-</para></listitem>
-<listitem><para>
-Unboxed tuple on left of an arrow.
-</para></listitem>
-<listitem><para>
-Partially-applied type synonym.
-</para></listitem>
+<listitem> <para> distributing a supply of unique names </para> </listitem>
+<listitem> <para> distributing a suppply of random numbers </para> </listitem>
+<listitem> <para> distributing an oracle (as in QuickCheck) </para> </listitem>
</itemizedlist>
-So, for example,
-this will be rejected:
+
+<para>
+Linear implicit parameters are just like ordinary implicit parameters,
+except that they are "linear" -- that is, they cannot be copied, and
+must be explicitly "split" instead. Linear implicit parameters are
+written '<literal>%x</literal>' instead of '<literal>?x</literal>'.
+(The '/' in the '%' suggests the split!)
+</para>
+<para>
+For example:
<programlisting>
- type Pr = (# Int, Int #)
+ import GHC.Exts( Splittable )
- h :: Pr -> Int
- h x = ...
+ data NameSupply = ...
+
+ splitNS :: NameSupply -> (NameSupply, NameSupply)
+ newName :: NameSupply -> Name
+
+ instance Splittable NameSupply where
+ split = splitNS
+
+
+ f :: (%ns :: NameSupply) => Env -> Expr -> Expr
+ f env (Lam x e) = Lam x' (f env e)
+ where
+ x' = newName %ns
+ env' = extend env x x'
+ ...more equations for f...
</programlisting>
-because GHC does not allow unboxed tuples on the left of a function arrow.
+Notice that the implicit parameter %ns is consumed
+<itemizedlist>
+<listitem> <para> once by the call to <literal>newName</literal> </para> </listitem>
+<listitem> <para> once by the recursive call to <literal>f</literal> </para></listitem>
+</itemizedlist>
</para>
-</sect2>
-
-<sect2 id="hoist">
-<title>For-all hoisting</title>
<para>
-It is often convenient to use generalised type synonyms at the right hand
-end of an arrow, thus:
+So the translation done by the type checker makes
+the parameter explicit:
<programlisting>
- type Discard a = forall b. a -> b -> a
-
- g :: Int -> Discard Int
- g x y z = x+y
+ f :: NameSupply -> Env -> Expr -> Expr
+ f ns env (Lam x e) = Lam x' (f ns1 env e)
+ where
+ (ns1,ns2) = splitNS ns
+ x' = newName ns2
+ env = extend env x x'
</programlisting>
-Simply expanding the type synonym would give
+Notice the call to 'split' introduced by the type checker.
+How did it know to use 'splitNS'? Because what it really did
+was to introduce a call to the overloaded function 'split',
+defined by the class <literal>Splittable</literal>:
<programlisting>
- g :: Int -> (forall b. Int -> b -> Int)
+ class Splittable a where
+ split :: a -> (a,a)
</programlisting>
-but GHC "hoists" the <literal>forall</literal> to give the isomorphic type
+The instance for <literal>Splittable NameSupply</literal> tells GHC how to implement
+split for name supplies. But we can simply write
<programlisting>
- g :: forall b. Int -> Int -> b -> Int
+ g x = (x, %ns, %ns)
</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>
+and GHC will infer
<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>
+ g :: (Splittable a, %ns :: a) => b -> (b,a,a)
</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:
+The <literal>Splittable</literal> class is built into GHC. It's exported by module
+<literal>GHC.Exts</literal>.
+</para>
+<para>
+Other points:
+<itemizedlist>
+<listitem> <para> '<literal>?x</literal>' and '<literal>%x</literal>'
+are entirely distinct implicit parameters: you
+ can use them together and they won't intefere with each other. </para>
+</listitem>
+
+<listitem> <para> You can bind linear implicit parameters in 'with' clauses. </para> </listitem>
+
+<listitem> <para>You cannot have implicit parameters (whether linear or not)
+ in the context of a class or instance declaration. </para></listitem>
+</itemizedlist>
+</para>
+
+<sect3><title>Warnings</title>
+
+<para>
+The monomorphism restriction is even more important than usual.
+Consider the example above:
<programlisting>
- g :: Int -> Int -> forall b. b -> Int
+ f :: (%ns :: NameSupply) => Env -> Expr -> Expr
+ f env (Lam x e) = Lam x' (f env e)
+ where
+ x' = newName %ns
+ env' = extend env x x'
+</programlisting>
+If we replaced the two occurrences of x' by (newName %ns), which is
+usually a harmless thing to do, we get:
+<programlisting>
+ f :: (%ns :: NameSupply) => Env -> Expr -> Expr
+ f env (Lam x e) = Lam (newName %ns) (f env e)
+ where
+ env' = extend env x (newName %ns)
</programlisting>
+But now the name supply is consumed in <emphasis>three</emphasis> places
+(the two calls to newName,and the recursive call to f), so
+the result is utterly different. Urk! We don't even have
+the beta rule.
</para>
<para>
-When doing this hoisting operation, GHC eliminates duplicate constraints. For
-example:
+Well, this is an experimental change. With implicit
+parameters we have already lost beta reduction anyway, and
+(as John Launchbury puts it) we can't sensibly reason about
+Haskell programs without knowing their typing.
+</para>
+
+</sect3>
+
+<sect3><title>Recursive functions</title>
+<para>Linear implicit parameters can be particularly tricky when you have a recursive function
+Consider
<programlisting>
- type Foo a = (?x::Int) => Bool -> a
- g :: Foo (Foo Int)
+ foo :: %x::T => Int -> [Int]
+ foo 0 = []
+ foo n = %x : foo (n-1)
</programlisting>
-means
+where T is some type in class Splittable.</para>
+<para>
+Do you get a list of all the same T's or all different T's
+(assuming that split gives two distinct T's back)?
+</para><para>
+If you supply the type signature, taking advantage of polymorphic
+recursion, you get what you'd probably expect. Here's the
+translated term, where the implicit param is made explicit:
<programlisting>
- g :: (?x::Int) => Bool -> Bool -> Int
+ foo x 0 = []
+ foo x n = let (x1,x2) = split x
+ in x1 : foo x2 (n-1)
+</programlisting>
+But if you don't supply a type signature, GHC uses the Hindley
+Milner trick of using a single monomorphic instance of the function
+for the recursive calls. That is what makes Hindley Milner type inference
+work. So the translation becomes
+<programlisting>
+ foo x = let
+ foom 0 = []
+ foom n = x : foom (n-1)
+ in
+ foom
</programlisting>
+Result: 'x' is not split, and you get a list of identical T's. So the
+semantics of the program depends on whether or not foo has a type signature.
+Yikes!
+</para><para>
+You may say that this is a good reason to dislike linear implicit parameters
+and you'd be right. That is why they are an experimental feature.
</para>
-</sect2>
+</sect3>
+</sect2>
-<sect2 id="existential-quantification">
-<title>Existentially quantified data constructors
+<sect2 id="functional-dependencies">
+<title>Functional dependencies
</title>
-<para>
-The idea of using existential quantification in data type declarations
-was suggested by Laufer (I believe, thought doubtless someone will
-correct me), and implemented in Hope+. It's been in Lennart
-Augustsson's <Command>hbc</Command> Haskell compiler for several years, and
-proved very useful. Here's the idea. Consider the declaration:
+<para> Functional dependencies are implemented as described by Mark Jones
+in “<ulink url="http://www.cse.ogi.edu/~mpj/pubs/fundeps.html">Type Classes with Functional Dependencies</ulink>”, 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>
- data Foo = forall a. MkFoo a (a -> Bool)
- | Nil
-</programlisting>
-
-</para>
-
-<para>
-The data type <literal>Foo</literal> has two constructors with types:
-</para>
-
-<para>
+ class (Monad m) => MonadState s m | m -> s where ...
-<programlisting>
- MkFoo :: forall a. a -> (a -> Bool) -> Foo
- Nil :: Foo
+ class Foo a b c | a b -> c where ...
</programlisting>
-
-</para>
-
-<para>
-Notice that the type variable <literal>a</literal> in the type of <function>MkFoo</function>
-does not appear in the data type itself, which is plain <literal>Foo</literal>.
-For example, the following expression is fine:
+There should be more documentation, but there isn't (yet). Yell if you need it.
</para>
+</sect2>
-<para>
-
-<programlisting>
- [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo]
-</programlisting>
-</para>
-<para>
-Here, <literal>(MkFoo 3 even)</literal> packages an integer with a function
-<function>even</function> that maps an integer to <literal>Bool</literal>; and <function>MkFoo 'c'
-isUpper</function> packages a character with a compatible function. These
-two things are each of type <literal>Foo</literal> and can be put in a list.
-</para>
+<sect2 id="sec-kinding">
+<title>Explicitly-kinded quantification</title>
<para>
-What can we do with a value of type <literal>Foo</literal>?. In particular,
-what happens when we pattern-match on <function>MkFoo</function>?
+Haskell infers the kind of each type variable. Sometimes it is nice to be able
+to give the kind explicitly as (machine-checked) documentation,
+just as it is nice to give a type signature for a function. On some occasions,
+it is essential to do so. For example, in his paper "Restricted Data Types in Haskell" (Haskell Workshop 1999)
+John Hughes had to define the data type:
+<Screen>
+ data Set cxt a = Set [a]
+ | Unused (cxt a -> ())
+</Screen>
+The only use for the <literal>Unused</literal> constructor was to force the correct
+kind for the type variable <literal>cxt</literal>.
</para>
-
<para>
-
-<programlisting>
- f (MkFoo val fn) = ???
-</programlisting>
-
+GHC now instead allows you to specify the kind of a type variable directly, wherever
+a type variable is explicitly bound. Namely:
+<itemizedlist>
+<listitem><para><literal>data</literal> declarations:
+<Screen>
+ data Set (cxt :: * -> *) a = Set [a]
+</Screen></para></listitem>
+<listitem><para><literal>type</literal> declarations:
+<Screen>
+ type T (f :: * -> *) = f Int
+</Screen></para></listitem>
+<listitem><para><literal>class</literal> declarations:
+<Screen>
+ class (Eq a) => C (f :: * -> *) a where ...
+</Screen></para></listitem>
+<listitem><para><literal>forall</literal>'s in type signatures:
+<Screen>
+ f :: forall (cxt :: * -> *). Set cxt Int
+</Screen></para></listitem>
+</itemizedlist>
</para>
<para>
-Since all we know about <literal>val</literal> and <function>fn</function> is that they
-are compatible, the only (useful) thing we can do with them is to
-apply <function>fn</function> to <literal>val</literal> to get a boolean. For example:
+The parentheses are required. Some of the spaces are required too, to
+separate the lexemes. If you write <literal>(f::*->*)</literal> you
+will get a parse error, because "<literal>::*->*</literal>" is a
+single lexeme in Haskell.
</para>
<para>
-
-<programlisting>
- f :: Foo -> Bool
- f (MkFoo val fn) = fn val
-</programlisting>
-
+As part of the same extension, you can put kind annotations in types
+as well. Thus:
+<Screen>
+ f :: (Int :: *) -> Int
+ g :: forall a. a -> (a :: *)
+</Screen>
+The syntax is
+<Screen>
+ atype ::= '(' ctype '::' kind ')
+</Screen>
+The parentheses are required.
</para>
+</sect2>
-<para>
-What this allows us to do is to package heterogenous values
-together with a bunch of functions that manipulate them, and then treat
-that collection of packages in a uniform manner. You can express
-quite a bit of object-oriented-like programming this way.
-</para>
-<sect3 id="existential">
-<title>Why existential?
+<sect2 id="universal-quantification">
+<title>Arbitrary-rank polymorphism
</title>
<para>
-What has this to do with <emphasis>existential</emphasis> quantification?
-Simply that <function>MkFoo</function> has the (nearly) isomorphic type
+Haskell type signatures are implicitly quantified. The new keyword <literal>forall</literal>
+allows us to say exactly what this means. For example:
</para>
-
<para>
-
<programlisting>
- MkFoo :: (exists a . (a, a -> Bool)) -> Foo
+ g :: b -> b
</programlisting>
-
-</para>
-
-<para>
-But Haskell programmers can safely think of the ordinary
-<emphasis>universally</emphasis> quantified type given above, thereby avoiding
-adding a new existential quantification construct.
-</para>
-
-</sect3>
-
-<sect3>
-<title>Type classes</title>
-
-<para>
-An easy extension (implemented in <Command>hbc</Command>) is to allow
-arbitrary contexts before the constructor. For example:
-</para>
-
-<para>
-
+means this:
<programlisting>
-data Baz = forall a. Eq a => Baz1 a a
- | forall b. Show b => Baz2 b (b -> b)
+ g :: forall b. (b -> b)
</programlisting>
-
-</para>
-
-<para>
-The two constructors have the types you'd expect:
+The two are treated identically.
</para>
<para>
-
+However, GHC's type system supports <emphasis>arbitrary-rank</emphasis>
+explicit universal quantification in
+types.
+For example, all the following types are legal:
<programlisting>
-Baz1 :: forall a. Eq a => a -> a -> Baz
-Baz2 :: forall b. Show b => b -> (b -> b) -> Baz
-</programlisting>
+ f1 :: forall a b. a -> b -> a
+ g1 :: forall a b. (Ord a, Eq b) => a -> b -> a
-</para>
+ f2 :: (forall a. a->a) -> Int -> Int
+ g2 :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int
-<para>
-But when pattern matching on <function>Baz1</function> the matched values can be compared
-for equality, and when pattern matching on <function>Baz2</function> the first matched
-value can be converted to a string (as well as applying the function to it).
-So this program is legal:
+ f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool
+</programlisting>
+Here, <literal>f1</literal> and <literal>g1</literal> are rank-1 types, and
+can be written in standard Haskell (e.g. <literal>f1 :: a->b->a</literal>).
+The <literal>forall</literal> makes explicit the universal quantification that
+is implicitly added by Haskell.
</para>
-
<para>
-
-<programlisting>
- f :: Baz -> String
- f (Baz1 p q) | p == q = "Yes"
- | otherwise = "No"
- f (Baz2 v fn) = show (fn v)
-</programlisting>
-
+The functions <literal>f2</literal> and <literal>g2</literal> have rank-2 types;
+the <literal>forall</literal> is on the left of a function arrrow. As <literal>g2</literal>
+shows, the polymorphic type on the left of the function arrow can be overloaded.
</para>
-
<para>
-Operationally, in a dictionary-passing implementation, the
-constructors <function>Baz1</function> and <function>Baz2</function> must store the
-dictionaries for <literal>Eq</literal> and <literal>Show</literal> respectively, and
-extract it on pattern matching.
+The functions <literal>f3</literal> and <literal>g3</literal> have rank-3 types;
+they have rank-2 types on the left of a function arrow.
</para>
-
<para>
-Notice the way that the syntax fits smoothly with that used for
-universal quantification earlier.
+GHC allows types of arbitrary rank; you can nest <literal>forall</literal>s
+arbitrarily deep in function arrows. (GHC used to be restricted to rank 2, but
+that restriction has now been lifted.)
+In particular, a forall-type (also called a "type scheme"),
+including an operational type class context, is legal:
+<itemizedlist>
+<listitem> <para> On the left of a function arrow </para> </listitem>
+<listitem> <para> On the right of a function arrow (see <xref linkend="hoist">) </para> </listitem>
+<listitem> <para> As the argument of a constructor, or type of a field, in a data type declaration. For
+example, any of the <literal>f1,f2,f3,g1,g2,g3</literal> above would be valid
+field type signatures.</para> </listitem>
+<listitem> <para> As the type of an implicit parameter </para> </listitem>
+<listitem> <para> In a pattern type signature (see <xref linkend="scoped-type-variables">) </para> </listitem>
+</itemizedlist>
+There is one place you cannot put a <literal>forall</literal>:
+you cannot instantiate a type variable with a forall-type. So you cannot
+make a forall-type the argument of a type constructor. So these types are illegal:
+<programlisting>
+ x1 :: [forall a. a->a]
+ x2 :: (forall a. a->a, Int)
+ x3 :: Maybe (forall a. a->a)
+</programlisting>
+Of course <literal>forall</literal> becomes a keyword; you can't use <literal>forall</literal> as
+a type variable any more!
</para>
-</sect3>
-<sect3>
-<title>Restrictions</title>
+<sect3 id="univ">
+<title>Examples
+</title>
<para>
-There are several restrictions on the ways in which existentially-quantified
-constructors can be use.
+In a <literal>data</literal> or <literal>newtype</literal> declaration one can quantify
+the types of the constructor arguments. Here are several examples:
</para>
<para>
-<itemizedlist>
-<listitem>
-
-<para>
- When pattern matching, each pattern match introduces a new,
-distinct, type for each existential type variable. These types cannot
-be unified with any other type, nor can they escape from the scope of
-the pattern match. For example, these fragments are incorrect:
+<programlisting>
+data T a = T1 (forall b. b -> b -> b) a
+data MonadT m = MkMonad { return :: forall a. a -> m a,
+ bind :: forall a b. m a -> (a -> m b) -> m b
+ }
-<programlisting>
-f1 (MkFoo a f) = a
+newtype Swizzle = MkSwizzle (Ord a => [a] -> [a])
</programlisting>
+</para>
-Here, the type bound by <function>MkFoo</function> "escapes", because <literal>a</literal>
-is the result of <function>f1</function>. One way to see why this is wrong is to
-ask what type <function>f1</function> has:
+<para>
+The constructors have rank-2 types:
+</para>
+<para>
<programlisting>
- f1 :: Foo -> a -- Weird!
+T1 :: forall a. (forall b. b -> b -> b) -> a -> T a
+MkMonad :: forall m. (forall a. a -> m a)
+ -> (forall a b. m a -> (a -> m b) -> m b)
+ -> MonadT m
+MkSwizzle :: (Ord a => [a] -> [a]) -> Swizzle
</programlisting>
+</para>
-What is this "<literal>a</literal>" in the result type? Clearly we don't mean
-this:
+<para>
+Notice that you don't need to use a <literal>forall</literal> if there's an
+explicit context. For example in the first argument of the
+constructor <function>MkSwizzle</function>, an implicit "<literal>forall a.</literal>" is
+prefixed to the argument type. The implicit <literal>forall</literal>
+quantifies all type variables that are not already in scope, and are
+mentioned in the type quantified over.
+</para>
+<para>
+As for type signatures, implicit quantification happens for non-overloaded
+types too. So if you write this:
<programlisting>
- f1 :: forall a. Foo -> a -- Wrong!
+ data T a = MkT (Either a b) (b -> b)
</programlisting>
-
-The original program is just plain wrong. Here's another sort of error
-
+it's just as if you had written this:
<programlisting>
- f2 (Baz1 a b) (Baz1 p q) = a==q
+ data T a = MkT (forall b. Either a b) (forall b. b -> b)
</programlisting>
-
-It's ok to say <literal>a==b</literal> or <literal>p==q</literal>, but
-<literal>a==q</literal> is wrong because it equates the two distinct types arising
-from the two <function>Baz1</function> constructors.
-
-
+That is, since the type variable <literal>b</literal> isn't in scope, it's
+implicitly universally quantified. (Arguably, it would be better
+to <emphasis>require</emphasis> explicit quantification on constructor arguments
+where that is what is wanted. Feedback welcomed.)
</para>
-</listitem>
-<listitem>
<para>
-You can't pattern-match on an existentially quantified
-constructor in a <literal>let</literal> or <literal>where</literal> group of
-bindings. So this is illegal:
+You construct values of types <literal>T1, MonadT, Swizzle</literal> by applying
+the constructor to suitable values, just as usual. For example,
+</para>
+<para>
<programlisting>
- f3 x = a==b where { Baz1 a b = x }
-</programlisting>
-
-Instead, use a <literal>case</literal> expression:
+ a1 :: T Int
+ a1 = T1 (\xy->x) 3
+
+ a2, a3 :: Swizzle
+ a2 = MkSwizzle sort
+ a3 = MkSwizzle reverse
+
+ a4 :: MonadT Maybe
+ a4 = let r x = Just x
+ b m k = case m of
+ Just y -> k y
+ Nothing -> Nothing
+ in
+ MkMonad r b
-<programlisting>
- f3 x = case x of Baz1 a b -> a==b
+ mkTs :: (forall b. b -> b -> b) -> a -> [T a]
+ mkTs f x y = [T1 f x, T1 f y]
</programlisting>
-In general, you can only pattern-match
-on an existentially-quantified constructor in a <literal>case</literal> expression or
-in the patterns of a function definition.
-
-The reason for this restriction is really an implementation one.
-Type-checking binding groups is already a nightmare without
-existentials complicating the picture. Also an existential pattern
-binding at the top level of a module doesn't make sense, because it's
-not clear how to prevent the existentially-quantified type "escaping".
-So for now, there's a simple-to-state restriction. We'll see how
-annoying it is.
+</para>
+<para>
+The type of the argument can, as usual, be more general than the type
+required, as <literal>(MkSwizzle reverse)</literal> shows. (<function>reverse</function>
+does not need the <literal>Ord</literal> constraint.)
</para>
-</listitem>
-<listitem>
<para>
-You can't use existential quantification for <literal>newtype</literal>
-declarations. So this is illegal:
+When you use pattern matching, the bound variables may now have
+polymorphic types. For example:
+</para>
+<para>
<programlisting>
- newtype T = forall a. Ord a => MkT a
-</programlisting>
-
+ f :: T a -> a -> (a, Char)
+ f (T1 w k) x = (w k x, w 'c' 'd')
-Reason: a value of type <literal>T</literal> must be represented as a pair
-of a dictionary for <literal>Ord t</literal> and a value of type <literal>t</literal>.
-That contradicts the idea that <literal>newtype</literal> should have no
-concrete representation. You can get just the same efficiency and effect
-by using <literal>data</literal> instead of <literal>newtype</literal>. If there is no
-overloading involved, then there is more of a case for allowing
-an existentially-quantified <literal>newtype</literal>, because the <literal>data</literal>
-because the <literal>data</literal> version does carry an implementation cost,
-but single-field existentially quantified constructors aren't much
-use. So the simple restriction (no existential stuff on <literal>newtype</literal>)
-stands, unless there are convincing reasons to change it.
+ g :: (Ord a, Ord b) => Swizzle -> [a] -> (a -> b) -> [b]
+ g (MkSwizzle s) xs f = s (map f (s xs))
+ h :: MonadT m -> [m a] -> m [a]
+ h m [] = return m []
+ h m (x:xs) = bind m x $ \y ->
+ bind m (h m xs) $ \ys ->
+ return m (y:ys)
+</programlisting>
</para>
-</listitem>
-<listitem>
<para>
- You can't use <literal>deriving</literal> to define instances of a
-data type with existentially quantified data constructors.
+In the function <function>h</function> we use the record selectors <literal>return</literal>
+and <literal>bind</literal> to extract the polymorphic bind and return functions
+from the <literal>MonadT</literal> data structure, rather than using pattern
+matching.
+</para>
+</sect3>
-Reason: in most cases it would not make sense. For example:#
+<sect3>
+<title>Type inference</title>
+<para>
+In general, type inference for arbitrary-rank types is undecideable.
+GHC uses an algorithm proposed by Odersky and Laufer ("Putting type annotations to work", POPL'96)
+to get a decidable algorithm by requiring some help from the programmer.
+We do not yet have a formal specification of "some help" but the rule is this:
+</para>
+<para>
+<emphasis>For a lambda-bound or case-bound variable, x, either the programmer
+provides an explicit polymorphic type for x, or GHC's type inference will assume
+that x's type has no foralls in it</emphasis>.
+</para>
+<para>
+What does it mean to "provide" an explicit type for x? You can do that by
+giving a type signature for x directly, using a pattern type signature
+(<xref linkend="scoped-type-variables">), thus:
<programlisting>
-data T = forall a. MkT [a] deriving( Eq )
+ \ f :: (forall a. a->a) -> (f True, f 'c')
+</programlisting>
+Alternatively, you can give a type signature to the enclosing
+context, which GHC can "push down" to find the type for the variable:
+<programlisting>
+ (\ f -> (f True, f 'c')) :: (forall a. a->a) -> (Bool,Char)
+</programlisting>
+Here the type signature on the expression can be pushed inwards
+to give a type signature for f. Similarly, and more commonly,
+one can give a type signature for the function itself:
+<programlisting>
+ h :: (forall a. a->a) -> (Bool,Char)
+ h f = (f True, f 'c')
+</programlisting>
+You don't need to give a type signature if the lambda bound variable
+is a constructor argument. Here is an example we saw earlier:
+<programlisting>
+ f :: T a -> a -> (a, Char)
+ f (T1 w k) x = (w k x, w 'c' 'd')
</programlisting>
+Here we do not need to give a type signature to <literal>w</literal>, because
+it is an argument of constructor <literal>T1</literal> and that tells GHC all
+it needs to know.
+</para>
-To derive <literal>Eq</literal> in the standard way we would need to have equality
-between the single component of two <function>MkT</function> constructors:
+</sect3>
+
+
+<sect3 id="implicit-quant">
+<title>Implicit quantification</title>
+<para>
+GHC performs implicit quantification as follows. <emphasis>At the top level (only) of
+user-written types, if and only if there is no explicit <literal>forall</literal>,
+GHC finds all the type variables mentioned in the type that are not already
+in scope, and universally quantifies them.</emphasis> For example, the following pairs are
+equivalent:
<programlisting>
-instance Eq T where
- (MkT a) == (MkT b) = ???
-</programlisting>
+ f :: a -> a
+ f :: forall a. a -> a
-But <VarName>a</VarName> and <VarName>b</VarName> have distinct types, and so can't be compared.
-It's just about possible to imagine examples in which the derived instance
-would make sense, but it seems altogether simpler simply to prohibit such
-declarations. Define your own instances!
+ g (x::a) = let
+ h :: a -> b -> b
+ h x y = y
+ in ...
+ g (x::a) = let
+ h :: forall b. a -> b -> b
+ h x y = y
+ in ...
+</programlisting>
</para>
-</listitem>
+<para>
+Notice that GHC does <emphasis>not</emphasis> find the innermost possible quantification
+point. For example:
+<programlisting>
+ f :: (a -> a) -> Int
+ -- MEANS
+ f :: forall a. (a -> a) -> Int
+ -- NOT
+ f :: (forall a. a -> a) -> Int
-</itemizedlist>
+ g :: (Ord a => a -> a) -> Int
+ -- MEANS the illegal type
+ g :: forall a. (Ord a => a -> a) -> Int
+ -- NOT
+ g :: (forall a. Ord a => a -> a) -> Int
+</programlisting>
+The latter produces an illegal type, which you might think is silly,
+but at least the rule is simple. If you want the latter type, you
+can write your for-alls explicitly. Indeed, doing so is strongly advised
+for rank-2 types.
</para>
-
</sect3>
-
</sect2>
+
+
+
<sect2 id="scoped-type-variables">
<title>Scoped type variables
</title>
;;; sgml-parent-document: ("users_guide.sgml" "book" "chapter" "sect1") ***
;;; End: ***
-->
+
projects / ghc-hetmet.git / commitdiff