glasgow_exts.sgml

<para>
<indexterm><primary>language, GHC</primary></indexterm>
<indexterm><primary>extensions, GHC</primary></indexterm>
As with all known Haskell systems, GHC implements some extensions to
the language.  To use them, you'll need to give a <option>-fglasgow-exts</option>
<indexterm><primary>-fglasgow-exts option</primary></indexterm> option.
</para>

<para>
Virtually all of the Glasgow extensions serve to give you access to
the underlying facilities with which we implement Haskell.  Thus, you
can get at the Raw Iron, if you are willing to write some non-standard
code at a more primitive level.  You need not be &ldquo;stuck&rdquo; on
performance because of the implementation costs of Haskell's
&ldquo;high-level&rdquo; features&mdash;you can always code &ldquo;under&rdquo; them.  In an extreme case, you can write all your time-critical code in C, and then just glue it together with Haskell!
</para>

<para>
Before you get too carried away working at the lowest level (e.g.,
sloshing <literal>MutableByteArray&num;</literal>s around your
program), you may wish to check if there are libraries that provide a
&ldquo;Haskellised veneer&rdquo; over the features you want.  The
separate libraries documentation describes all the libraries that come
with GHC.
</para>

<!-- LANGUAGE OPTIONS -->
  <sect1 id="options-language">
    <title>Language options</title>

    <indexterm><primary>language</primary><secondary>option</secondary>
    </indexterm>
    <indexterm><primary>options</primary><secondary>language</secondary>
    </indexterm>
    <indexterm><primary>extensions</primary><secondary>options controlling</secondary>
    </indexterm>

    <para> These flags control what variation of the language are
    permitted.  Leaving out all of them gives you standard Haskell
    98.</para>

    <variablelist>

      <varlistentry>
	<term><option>-fglasgow-exts</option>:</term>
	<indexterm><primary><option>-fglasgow-exts</option></primary></indexterm>
	<listitem>
	  <para>This simultaneously enables all of the extensions to
          Haskell 98 described in <xref
          linkend="ghc-language-features">, except where otherwise
          noted. </para>
	</listitem>
      </varlistentry>

      <varlistentry>
	<term><option>-ffi</option> and <option>-fffi</option>:</term>
	<indexterm><primary><option>-ffi</option></primary></indexterm>
	<indexterm><primary><option>-fffi</option></primary></indexterm>
	<listitem>
	  <para>This option enables the language extension defined in the
	  Haskell 98 Foreign Function Interface Addendum plus deprecated
	  syntax of previous versions of the FFI for backwards
	  compatibility.</para> 
	</listitem>
      </varlistentry>

      <varlistentry>
	<term><option>-fwith</option>:</term>
	<indexterm><primary><option>-fwith</option></primary></indexterm>
	<listitem>
	  <para>This option enables the deprecated <literal>with</literal>
	  keyword for implicit parameters; it is merely provided for backwards
	  compatibility.
          It is independent of the <option>-fglasgow-exts</option>
          flag. </para>
	</listitem>
      </varlistentry>

      <varlistentry>
	<term><option>-fno-monomorphism-restriction</option>:</term>
	<indexterm><primary><option>-fno-monomorphism-restriction</option></primary></indexterm>
	<listitem>
	  <para> Switch off the Haskell 98 monomorphism restriction.
          Independent of the <option>-fglasgow-exts</option>
          flag. </para>
	</listitem>
      </varlistentry>

      <varlistentry>
	<term><option>-fallow-overlapping-instances</option></term>
	<term><option>-fallow-undecidable-instances</option></term>
	<term><option>-fallow-incoherent-instances</option></term>
	<term><option>-fcontext-stack</option></term>
	<indexterm><primary><option>-fallow-overlapping-instances</option></primary></indexterm>
	<indexterm><primary><option>-fallow-undecidable-instances</option></primary></indexterm>
	<indexterm><primary><option>-fcontext-stack</option></primary></indexterm>
	<listitem>
	  <para> See <xref LinkEnd="instance-decls">.  Only relevant
          if you also use <option>-fglasgow-exts</option>.</para>
	</listitem>
      </varlistentry>

      <varlistentry>
	<term><option>-finline-phase</option></term>
	<indexterm><primary><option>-finline-phase</option></primary></indexterm>
	<listitem>
	  <para>See <xref LinkEnd="rewrite-rules">.  Only relevant if
          you also use <option>-fglasgow-exts</option>.</para>
	</listitem>
      </varlistentry>

      <varlistentry>
	<term><option>-fgenerics</option></term>
	<indexterm><primary><option>-fgenerics</option></primary></indexterm>
	<listitem>
	  <para>See <xref LinkEnd="generic-classes">.  Independent of
          <option>-fglasgow-exts</option>.</para>
	</listitem>
      </varlistentry>

	<varlistentry>
	  <term><option>-fno-implicit-prelude</option></term>
	  <listitem>
	    <para><indexterm><primary>-fno-implicit-prelude
            option</primary></indexterm> GHC normally imports
            <filename>Prelude.hi</filename> files for you.  If you'd
            rather it didn't, then give it a
            <option>-fno-implicit-prelude</option> option.  The idea
            is that you can then import a Prelude of your own.  (But
            don't call it <literal>Prelude</literal>; the Haskell
            module namespace is flat, and you must not conflict with
            any Prelude module.)</para>

	    <para>Even though you have not imported the Prelude, most of
            the built-in syntax still refers to the built-in Haskell
            Prelude types and values, as specified by the Haskell
            Report.  For example, the type <literal>[Int]</literal>
            still means <literal>Prelude.[] Int</literal>; tuples
            continue to refer to the standard Prelude tuples; the
            translation for list comprehensions continues to use
            <literal>Prelude.map</literal> etc.</para>

	    <para>However, <option>-fno-implicit-prelude</option> does
	    change the handling of certain built-in syntax: see
	    <xref LinkEnd="rebindable-syntax">.</para>

	  </listitem>
	</varlistentry>

    </variablelist>
  </sect1>

<!-- UNBOXED TYPES AND PRIMITIVE OPERATIONS -->
<!--    included from primitives.sgml  -->
&primitives;


<!-- TYPE SYSTEM EXTENSIONS -->
<sect1 id="type-extensions">
<title>Type system extensions</title>

<sect2 id="nullary-types">
<title>Data types with no constructors</title>

<para>With the <option>-fglasgow-exts</option> flag, GHC lets you declare
a data type with no constructors.  For example:</para>

<programlisting>
  data S      -- S :: *
  data T a    -- T :: * -> *
</programlisting>

<para>Syntactically, the declaration lacks the "= constrs" part.  The 
type can be parameterised over types of any kind, but if the kind is
not <literal>*</literal> then an explicit kind annotation must be used
(see <xref linkend="sec-kinding">).</para>

<para>Such data types have only one value, namely bottom.
Nevertheless, they can be useful when defining "phantom types".</para>
</sect2>

<sect2 id="infix-tycons">
<title>Infix type constructors</title>

<para>
GHC allows type constructors to be operators, and to be written infix, very much 
like expressions.  More specifically:
<itemizedlist>
<listitem><para>
  A type constructor can be an operator, beginning with a colon; e.g. <literal>:*:</literal>.
  The lexical syntax is the same as that for data constructors.
  </para></listitem>
<listitem><para>
  Types can be written infix.  For example <literal>Int :*: Bool</literal>.  
  </para></listitem>
<listitem><para>
  Back-quotes work
  as for expressions, both for type constructors and type variables;  e.g. <literal>Int `Either` Bool</literal>, or
  <literal>Int `a` Bool</literal>.  Similarly, parentheses work the same; e.g.  <literal>(:*:) Int Bool</literal>.
  </para></listitem>
<listitem><para>
  Fixities may be declared for type constructors just as for data constructors.  However,
  one cannot distinguish between the two in a fixity declaration; a fixity declaration
  sets the fixity for a data constructor and the corresponding type constructor.  For example:
<screen>
  infixl 7 T, :*:
</screen>
  sets the fixity for both type constructor <literal>T</literal> and data constructor <literal>T</literal>,
  and similarly for <literal>:*:</literal>.
  <literal>Int `a` Bool</literal>.
  </para></listitem>
<listitem><para>
  Function arrow is <literal>infixr</literal> with fixity 0.  (This might change; I'm not sure what it should be.)
  </para></listitem>
<listitem><para>
  Data type and type-synonym declarations can be written infix.  E.g.
<screen>
  data a :*: b = Foo a b
  type a :+: b = Either a b
</screen>
  </para></listitem>
<listitem><para>
  The only thing that differs between operators in types and operators in expressions is that
  ordinary non-constructor operators, such as <literal>+</literal> and <literal>*</literal>
  are not allowed in types. Reason: the uniform thing to do would be to make them type
  variables, but that's not very useful.  A less uniform but more useful thing would be to
  allow them to be type <emphasis>constructors</emphasis>.  But that gives trouble in export
  lists.  So for now we just exclude them.
  </para></listitem>

</itemizedlist>
</para>
</sect2>

<sect2 id="sec-kinding">
<title>Explicitly-kinded quantification</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:
<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>
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>
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>


<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:
<programlisting>
  class Seq s a where
    fromList :: [a] -> s a
    elem     :: Eq a => a -> s a -> Bool
</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>

</sect2>

<sect2 id="multi-param-type-classes">
<title>Multi-parameter type classes
</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>
I'd like to thank people who reported shorcomings in the GHC 3.02
implementation.  Our default decisions were all conservative ones, and
the experience of these heroic pioneers has given useful concrete
examples to support several generalisations.  (These appear below as
design choices not implemented in 3.02.)
</para>

<para>
I've discussed these notes with Mark Jones, and I believe that Hugs
will migrate towards the same design choices as I outline here.
Thanks to him, and to many others who have offered very useful
feedback.
</para>

<sect3>
<title>Types</title>

<para>
There are the following restrictions on the form of a qualified
type:
</para>

<para>

<programlisting>
  forall tv1..tvn (c1, ...,cn) => type
</programlisting>

</para>

<para>
(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">).
</para>

<para>

<OrderedList>
<listitem>

<para>
 <emphasis>Each universally quantified type variable
<literal>tvi</literal> must be mentioned (i.e. appear free) in <literal>type</literal></emphasis>.

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:


<programlisting>
  forall a. Eq a => Int
</programlisting>


When a value with this type was used, the constraint <literal>Eq tv</literal>
would be introduced where <literal>tv</literal> is a fresh type variable, and
(in the dictionary-translation implementation) the value would be
applied to a dictionary for <literal>Eq tv</literal>.  The difficulty is that we
can never know which instance of <literal>Eq</literal> to use because we never
get any more information about <literal>tv</literal>.

</para>
</listitem>
<listitem>

<para>
 <emphasis>Every constraint <literal>ci</literal> must mention at least one of the
universally quantified type variables <literal>tvi</literal></emphasis>.

For example, this type is OK because <literal>C a b</literal> mentions the
universally quantified type variable <literal>b</literal>:


<programlisting>
  forall a. C a b => burble
</programlisting>


The next type is illegal because the constraint <literal>Eq b</literal> does not
mention <literal>a</literal>:


<programlisting>
  forall a. Eq b => burble
</programlisting>


The reason for this restriction is milder than the other one.  The
excluded types are never useful or necessary (because the offending
context doesn't need to be witnessed at this point; it can be floated
out).  Furthermore, floating them out increases sharing. Lastly,
excluding them is a conservative choice; it leaves a patch of
territory free in case we need it later.

</para>
</listitem>

</OrderedList>

</para>

<para>
These restrictions apply to all types, whether declared in a type signature
or inferred.
</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
</para>

<para>

<programlisting>
  f :: Eq (m a) => [m a] -> [m a]
  g :: Eq [a] => ...
</programlisting>

</para>

<para>
This choice recovers principal types, a property that Haskell 1.4 does not have.
</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.
</programlisting>



</para>
</listitem>
<listitem>

<para>
 <emphasis>The class hierarchy must be acyclic</emphasis>.  However, the definition
of "acyclic" involves only the superclass relationships.  For example,
this is OK:


<programlisting>
  class C a where {
    op :: D b => a -> b -> b
  }

  class C a => D a where { ... }
</programlisting>


Here, <literal>C</literal> is a superclass of <literal>D</literal>, but it's OK for a
class operation <literal>op</literal> of <literal>C</literal> to mention <literal>D</literal>.  (It
would not be OK for <literal>D</literal> to be a superclass of <literal>C</literal>.)

</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
</programlisting>


</para>
</listitem>
<listitem>

<para>
 <emphasis>In the signature of a class operation, every constraint
must mention at least one type variable that is not a class type
variable</emphasis>.

Thus:


<programlisting>
  class Collection c a where
    mapC :: Collection c b => (a->b) -> c a -> c b
</programlisting>


is OK because the constraint <literal>(Collection a b)</literal> mentions
<literal>b</literal>, even though it also mentions the class variable
<literal>a</literal>.  On the other hand:


<programlisting>
  class C a where
    op :: Eq a => (a,b) -> (a,b)
</programlisting>


is not OK because the constraint <literal>(Eq a)</literal> mentions on the class
type variable <literal>a</literal>, but not <literal>b</literal>.  However, any such
example is easily fixed by moving the offending context up to the
superclass context:


<programlisting>
  class Eq a => C a where
    op ::(a,b) -> (a,b)
</programlisting>


A yet more relaxed rule would allow the context of a class-op signature
to mention only class type variables.  However, that conflicts with
Rule 1(b) for types above.

</para>
</listitem>
<listitem>

<para>
 <emphasis>The type of each class operation must mention <emphasis>all</emphasis> of
the class type variables</emphasis>.  For example:


<programlisting>
  class Coll s a where
    empty  :: s
    insert :: s -> a -> s
</programlisting>


is not OK, because the type of <literal>empty</literal> doesn't mention
<literal>a</literal>.  This rule is a consequence of Rule 1(a), above, for
types, and has the same motivation.

Sometimes, offending class declarations exhibit misunderstandings.  For
example, <literal>Coll</literal> might be rewritten


<programlisting>
  class Coll s a where
    empty  :: s a
    insert :: s a -> a -> s a
</programlisting>


which makes the connection between the type of a collection of
<literal>a</literal>'s (namely <literal>(s a)</literal>) and the element type <literal>a</literal>.
Occasionally this really doesn't work, in which case you can split the
class like this:


<programlisting>
  class CollE s where
    empty  :: s

  class CollE s => Coll s a where
    insert :: s -> a -> s
</programlisting>


</para>
</listitem>

</OrderedList>

</para>

</sect3>

<sect3 id="instance-decls">
<title>Instance declarations</title>

<para>

<OrderedList>
<listitem>

<para>
 <emphasis>Instance declarations may not overlap</emphasis>.  The two instance
declarations


<programlisting>
  instance context1 => C type1 where ...
  instance context2 => C type2 where ...
</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>
 EITHER <literal>type1</literal> and <literal>type2</literal> do not unify
</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.
</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)

</para>
</listitem>
<listitem>

<para>
 do not mention the contexts <literal>context1</literal>, <literal>context2</literal>
Reason: you can pick which instance decl
"matches" based on the type.
</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>
<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:


<programlisting>
  instance C Int a where ...

  instance D (Int, Int) where ...

  instance E [[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>


The "at least one not a type variable" restriction is to 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>
  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:


<programlisting>
  instance C a where
    op = ... -- Default
</programlisting>


Second, sometimes you might want to use the following to get the
effect of a "class synonym":


<programlisting>
  class (C1 a, C2 a, C3 a) => C a where { }

  instance (C1 a, C2 a, C3 a) => C a where { }
</programlisting>


This allows you to write shorter signatures:


<programlisting>
  f :: C a => ...
</programlisting>


instead of


<programlisting>
  f :: (C1 a, C2 a, C3 a) => ...
</programlisting>


I'm on the lookout for a simple rule that preserves decidability while
allowing these idioms.  The experimental flag
<option>-fallow-undecidable-instances</option><indexterm><primary>-fallow-undecidable-instances
option</primary></indexterm> lifts this restriction, allowing all the types in an
instance head to be type variables.

</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:


<programlisting>
  type Point = (Int,Int)
  instance C Point   where ...
  instance C [Point] where ...
</programlisting>


is legal.  However, if you added


<programlisting>
  instance C (Int,Int) where ...
</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>


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


<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.  Again, the intent here is to make sure that context
reduction terminates.

Voluminous correspondence on the Haskell mailing list has convinced me
that it's worth experimenting with a more liberal rule.  If you use
the flag <option>-fallow-undecidable-instances</option> can use arbitrary
types in an instance context.  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>
</listitem>

</OrderedList>

</para>

</sect3>

</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>
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>
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>
  sort :: (?cmp :: a -> a -> Bool) => [a] -> [a]
</programlisting>
The dynamic binding constraints are just a new form of predicate in the type class system.
</para>
<para>
An implicit parameter is introduced by the special form <literal>?x</literal>, 
where <literal>x</literal> is
any valid identifier. Use if this construct also introduces new
dynamic binding constraints. 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>
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>
  least   :: (?cmp :: a -> a -> Bool) => [a] -> a
  least xs = fst (sort xs)
</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.
</para>
<para>
An implicit parameter 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>
<para>
An implicit parameter is bound using the standard
<literal>let</literal> binding form, where the bindings 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. This form binds the implicit
parameters arising in the body, not the free variables as a
<literal>let</literal> or <literal>where</literal> would do. For
example, we define the <literal>min</literal> function by binding
<literal>cmp</literal>.</para>
<programlisting>
  min :: [a] -> a
  min  = let ?cmp = (<=) in least
</programlisting>
<para>
Note the following points:
<itemizedlist>
<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.
</para></listitem>

<listitem><para>
You may put multiple implicit-parameter bindings in a
single <literal>let</literal> expression; 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, each scoping over the bindings that
follow.  For example, consider:
<programlisting>
  f y = let { ?x = y; ?x = ?x+1 } in ?x
</programlisting>
This function adds one to its argument.
</para></listitem>

<listitem><para>
You may not have an implicit-parameter binding in a <literal>where</literal> clause,
only in a <literal>let</literal> binding.
</para></listitem>