Executive summary of our extensions:
</Para>
-<Para>
-<VariableList>
-
-<VarListEntry>
-<Term>Unboxed types and primitive operations:</Term>
-<ListItem>
-<Para>
-You can get right down to the raw machine types and operations;
-included in this are “primitive arrays” (direct access to Big Wads
-of Bytes). Please see <XRef LinkEnd="glasgow-unboxed"> and following.
-</Para>
-</ListItem>
-</VarListEntry>
+ <variablelist>
-<VarListEntry>
-<Term>Multi-parameter type classes:</Term>
-<ListItem>
-<Para>
-GHC's type system supports extended type classes with multiple
-parameters. Please see <XRef LinkEnd="multi-param-type-classes">.
-</Para>
-</ListItem>
-</VarListEntry>
-
-<VarListEntry>
-<Term>Local universal quantification:</Term>
-<ListItem>
-<Para>
-GHC's type system supports explicit universal quantification in
-constructor fields and function arguments. This is useful for things
-like defining <Literal>runST</Literal> from the state-thread world. See <XRef LinkEnd="universal-quantification">.
-</Para>
-</ListItem>
-</VarListEntry>
+ <varlistentry>
+ <term>Unboxed types and primitive operations:</Term>
+ <listitem>
+ <para>You can get right down to the raw machine types and
+ operations; included in this are “primitive
+ arrays” (direct access to Big Wads of Bytes). Please
+ see <XRef LinkEnd="glasgow-unboxed"> and following.</para>
+ </listitem>
+ </varlistentry>
-<VarListEntry>
-<Term>Extistentially quantification in data types:</Term>
-<ListItem>
-<Para>
-Some or all of the type variables in a datatype declaration may be
-<Emphasis>existentially quantified</Emphasis>. More details in <XRef LinkEnd="existential-quantification">.
-</Para>
-</ListItem>
-</VarListEntry>
+ <varlistentry>
+ <term>Type system extensions:</term>
+ <listitem>
+ <Para> GHC supports a large number of extensions to Haskell's
+ type system. Specifically:</para>
+
+ <variablelist>
+ <varlistentry>
+ <term>Multi-parameter type classes:</term>
+ <listitem>
+ <para><XRef LinkEnd="multi-param-type-classes"></para>
+ </listitem>
+ </varlistentry>
+
+ <varlistentry>
+ <term>Functional dependencies:</term>
+ <listitem>
+ <para><XRef LinkEnd="functional-dependencies"></para>
+ </listitem>
+ </varlistentry>
+
+ <varlistentry>
+ <term>Implicit parameters:</term>
+ <listitem>
+ <para><XRef LinkEnd="implicit-parameters"></para>
+ </listitem>
+ </varlistentry>
+
+ <varlistentry>
+ <term>Local universal quantification:</term>
+ <listitem>
+ <para><XRef LinkEnd="universal-quantification"></para>
+ </listitem>
+ </varlistentry>
+
+ <varlistentry>
+ <term>Extistentially quantification in data types:</term>
+ <listitem>
+ <para><XRef LinkEnd="existential-quantification"></para>
+ </listitem>
+ </varlistentry>
+
+ <varlistentry>
+ <term>Scoped type variables:</term>
+ <listitem>
+ <para>Scoped type variables enable the programmer to
+ supply type signatures for some nested declarations,
+ where this would not be legal in Haskell 98. Details in
+ <XRef LinkEnd="scoped-type-variables">.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </listitem>
+ </varlistentry>
-<VarListEntry>
-<Term>Scoped type variables:</Term>
-<ListItem>
-<Para>
-Scoped type variables enable the programmer to supply type signatures
-for some nested declarations, where this would not be legal in Haskell
-98. Details in <XRef LinkEnd="scoped-type-variables">.
-</Para>
-</ListItem>
-</VarListEntry>
+ <varlistentry>
+ <term>Pattern guards</term>
+ <listitem>
+ <para>Instead of being a boolean expression, a guard is a list
+ of qualifiers, exactly as in a list comprehension. See <XRef
+ LinkEnd="pattern-guards">.</para>
+ </listitem>
+ </varlistentry>
-<VarListEntry>
-<Term>Pattern guards</Term>
-<ListItem>
-<Para>
-Instead of being a boolean expression, a guard is a list of qualifiers, exactly as in a list comprehension. See <XRef LinkEnd="pattern-guards">.
-</Para>
-</ListItem>
-</VarListEntry>
+ <varlistentry>
+ <term>Foreign calling:</term>
+ <listitem>
+ <para>Just what it sounds like. We provide
+ <Emphasis>lots</Emphasis> of rope that you can dangle around
+ your neck. Please see <XRef LinkEnd="ffi">.</para>
+ </listitem>
+ </varlistentry>
-<VarListEntry>
-<Term>Foreign calling:</Term>
-<ListItem>
-<Para>
-Just what it sounds like. We provide <Emphasis>lots</Emphasis> of rope that you
-can dangle around your neck. Please see <XRef LinkEnd="ffi">.
-</Para>
-</ListItem>
-</VarListEntry>
+ <varlistentry>
+ <term>Pragmas</term>
+ <listitem>
+ <para>Pragmas are special instructions to the compiler placed
+ in the source file. The pragmas GHC supports are described in
+ <XRef LinkEnd="pragmas">.</para>
+ </listitem>
+ </varlistentry>
-<VarListEntry>
-<Term>Pragmas</Term>
-<ListItem>
-<Para>
-Pragmas are special instructions to the compiler placed in the source
-file. The pragmas GHC supports are described in <XRef LinkEnd="pragmas">.
-</Para>
-</ListItem>
-</VarListEntry>
+ <varlistentry>
+ <term>Rewrite rules:</term>
+ <listitem>
+ <para>The programmer can specify rewrite rules as part of the
+ source program (in a pragma). GHC applies these rewrite rules
+ wherever it can. Details in <XRef
+ LinkEnd="rewrite-rules">.</para>
+ </listitem>
+ </varlistentry>
-<VarListEntry>
-<Term>Rewrite rules:</Term>
-<ListItem>
-<Para>
-The programmer can specify rewrite rules as part of the source program
-(in a pragma). GHC applies these rewrite rules wherever it can.
-Details in <XRef LinkEnd="rewrite-rules">.
-</Para>
-</ListItem>
-</VarListEntry>
-</VariableList>
-</Para>
+ <varlistentry>
+ <term>Generic classes:</term>
+ <listitem>
+ <para>Generic class declarations allow you to define a class
+ whose methods say how to work over an arbitrary data type.
+ Then it's really easy to make any new type into an instance of
+ the class. This generalises the rather ad-hoc "deriving"
+ feature of Haskell 98. Details in <XRef
+ LinkEnd="generic-classes">.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
<Para>
Before you get too carried away working at the lowest level (e.g.,
<xref linkend="book-hslibs">.
</Para>
+ <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>-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>-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, all
+ 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> With one group of exceptions! You may want to
+ define your own numeric class hierarchy. It completely
+ defeats that purpose if the literal "1" means
+ "<literal>Prelude.fromInteger 1</literal>", which is what
+ the Haskell Report specifies. So the
+ <option>-fno-implicit-prelude</option> flag causes the
+ following pieces of built-in syntax to refer to whatever
+ is in scope, not the Prelude versions:</para>
+
+ <itemizedlist>
+ <listitem>
+ <para>Integer and fractional literals mean
+ "<literal>fromInteger 1</literal>" and
+ "<literal>fromRational 3.2</literal>", not the
+ Prelude-qualified versions; both in expressions and in
+ patterns.</para>
+ </listitem>
+
+ <listitem>
+ <para>Negation (e.g. "<literal>- (f x)</literal>")
+ means "<literal>negate (f x)</literal>" (not
+ <literal>Prelude.negate</literal>).</para>
+ </listitem>
+
+ <listitem>
+ <para>In an n+k pattern, the standard Prelude
+ <literal>Ord</literal> class is used for comparison,
+ but the necessary subtraction uses whatever
+ "<literal>(-)</literal>" is in scope (not
+ "<literal>Prelude.(-)</literal>").</para>
+ </listitem>
+ </itemizedlist>
+
+ </listitem>
+ </varlistentry>
+
+ </variablelist>
+ </sect1>
+
<Sect1 id="primitives">
<Title>Unboxed types and primitive operations
</Title>
</Para>
<Para>
-The <Literal>IO</Literal> and <Literal>ST</Literal> monads use unboxed tuples to avoid unnecessary
-allocation during sequences of operations.
+The <Literal>IO</Literal> and <Literal>ST</Literal> monads use unboxed
+tuples to avoid unnecessary allocation during sequences of operations.
</Para>
</Sect2>
<Sect2>
<Title>Character and numeric types</Title>
-<Para>
<IndexTerm><Primary>character types, primitive</Primary></IndexTerm>
<IndexTerm><Primary>numeric types, primitive</Primary></IndexTerm>
<IndexTerm><Primary>integer types, primitive</Primary></IndexTerm>
<IndexTerm><Primary>floating point types, primitive</Primary></IndexTerm>
+<Para>
There are the following obvious primitive types:
</Para>
-<Para>
-
<ProgramListing>
type Char#
type Int#
<IndexTerm><Primary><literal>Double#</literal></Primary></IndexTerm>
<IndexTerm><Primary><literal>Int64#</literal></Primary></IndexTerm>
<IndexTerm><Primary><literal>Word64#</literal></Primary></IndexTerm>
-</Para>
<Para>
If you really want to know their exact equivalents in C, see
1# an Int#
1.2# a Float#
1.34## a Double#
-'a'# a Char#; for weird characters, use '\o<octal>'#
-"a"# an Addr# (a `char *')
+'a'# a Char#; for weird characters, use e.g. '\o<octal>'#
+"a"# an Addr# (a `char *'); only characters '\0'..'\255' allowed
</ProgramListing>
<IndexTerm><Primary>literals, primitive</Primary></IndexTerm>
</Sect2>
-<Sect2>
+<Sect2 id="instance-decls">
<Title>Instance declarations</Title>
<Para>
</Sect1>
+<Sect1 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>
+There should be more documentation, but there isn't (yet). Yell if you need it.
+</Para>
+<ItemizedList>
+<ListItem>
+<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>
+</ListItem>
+
+</ItemizedList>
+
+</Sect1>
+
+
+<Sect1 id="functional-dependencies">
+<Title>Functional dependencies
+</Title>
+
+<Para> Functional dependencies are implemented as described by Mark Jones
+in "Type Classes with Functional Dependencies", Mark P. Jones,
+In Proceedings of the 9th European Symposium on Programming,
+ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782.
+</Para>
+
+<Para>
+There should be more documentation, but there isn't (yet). Yell if you need it.
+</Para>
+</Sect1>
+
+
<Sect1 id="universal-quantification">
<Title>Explicit universal quantification
</Title>
<Para>
-GHC now allows you to write explicitly quantified types. GHC's
-syntax for this now agrees with Hugs's, namely:
+GHC's type system supports explicit universal quantification in
+constructor fields and function arguments. This is useful for things
+like defining <Literal>runST</Literal> from the state-thread world.
+GHC's syntax for this now agrees with Hugs's, namely:
</Para>
<Para>
<ProgramListing>
kelvinToC :: Double -> Double
-kelvinToC k = assert (k &gt;= 0.0) (k+273.15)
+kelvinToC k = assert (k >= 0.0) (k+273.15)
</ProgramListing>
</Para>
"wrong2" forall f. f True = True
</ProgramListing>
-In <Literal>"wrong1"</Literal>, the LHS is not an application; in <Literal>"wrong1"</Literal>, the LHS has a pattern variable
+In <Literal>"wrong1"</Literal>, the LHS is not an application; in <Literal>"wrong2"</Literal>, the LHS has a pattern variable
in the head.
</Para>
</ListItem>
</Sect1>
+<Sect1 id="generic-classes">
+<Title>Generic classes</Title>
+
+<Para>
+The ideas behind this extension are described in detail in "Derivable type classes",
+Ralf Hinze and Simon Peyton Jones, Haskell Workshop, Montreal Sept 2000, pp94-105.
+An example will give the idea:
+</Para>
+
+<ProgramListing>
+ import Generics
+
+ class Bin a where
+ toBin :: a -> [Int]
+ fromBin :: [Int] -> (a, [Int])
+
+ toBin {| Unit |} Unit = []
+ toBin {| a :+: b |} (Inl x) = 0 : toBin x
+ toBin {| a :+: b |} (Inr y) = 1 : toBin y
+ toBin {| a :*: b |} (x :*: y) = toBin x ++ toBin y
+
+ fromBin {| Unit |} bs = (Unit, bs)
+ fromBin {| a :+: b |} (0:bs) = (Inl x, bs') where (x,bs') = fromBin bs
+ fromBin {| a :+: b |} (1:bs) = (Inr y, bs') where (y,bs') = fromBin bs
+ fromBin {| a :*: b |} bs = (x :*: y, bs'') where (x,bs' ) = fromBin bs
+ (y,bs'') = fromBin bs'
+</ProgramListing>
+<Para>
+This class declaration explains how <Literal>toBin</Literal> and <Literal>fromBin</Literal>
+work for arbitrary data types. They do so by giving cases for unit, product, and sum,
+which are defined thus in the library module <Literal>Generics</Literal>:
+</Para>
+<ProgramListing>
+ data Unit = Unit
+ data a :+: b = Inl a | Inr b
+ data a :*: b = a :*: b
+</ProgramListing>
+<Para>
+Now you can make a data type into an instance of Bin like this:
+<ProgramListing>
+ instance (Bin a, Bin b) => Bin (a,b)
+ instance Bin a => Bin [a]
+</ProgramListing>
+That is, just leave off the "where" clasuse. Of course, you can put in the
+where clause and over-ride whichever methods you please.
+</Para>
+
+ <Sect2>
+ <Title> Using generics </Title>
+ <Para>To use generics you need to</para>
+ <ItemizedList>
+ <ListItem>
+ <Para>Use the <Option>-fgenerics</Option> flag.</Para>
+ </ListItem>
+ <ListItem>
+ <Para>Import the module <Literal>Generics</Literal> from the
+ <Literal>lang</Literal> package. This import brings into
+ scope the data types <Literal>Unit</Literal>,
+ <Literal>:*:</Literal>, and <Literal>:+:</Literal>. (You
+ don't need this import if you don't mention these types
+ explicitly; for example, if you are simply giving instance
+ declarations.)</Para>
+ </ListItem>
+ </ItemizedList>
+ </Sect2>
+
+<Sect2> <Title> Changes wrt the paper </Title>
+<Para>
+Note that the type constructors <Literal>:+:</Literal> and <Literal>:*:</Literal>
+can be written infix (indeed, you can now use
+any operator starting in a colon as an infix type constructor). Also note that
+the type constructors are not exactly as in the paper (Unit instead of 1, etc).
+Finally, note that the syntax of the type patterns in the class declaration
+uses "<Literal>{|</Literal>" and "<Literal>{|</Literal>" brackets; curly braces
+alone would ambiguous when they appear on right hand sides (an extension we
+anticipate wanting).
+</Para>
+</Sect2>
+
+<Sect2> <Title>Terminology and restrictions</Title>
+<Para>
+Terminology. A "generic default method" in a class declaration
+is one that is defined using type patterns as above.
+A "polymorphic default method" is a default method defined as in Haskell 98.
+A "generic class declaration" is a class declaration with at least one
+generic default method.
+</Para>
+
+<Para>
+Restrictions:
+<ItemizedList>
+<ListItem>
+<Para>
+Alas, we do not yet implement the stuff about constructor names and
+field labels.
+</Para>
+</ListItem>
+
+<ListItem>
+<Para>
+A generic class can have only one parameter; you can't have a generic
+multi-parameter class.
+</Para>
+</ListItem>
+
+<ListItem>
+<Para>
+A default method must be defined entirely using type patterns, or entirely
+without. So this is illegal:
+<ProgramListing>
+ class Foo a where
+ op :: a -> (a, Bool)
+ op {| Unit |} Unit = (Unit, True)
+ op x = (x, False)
+</ProgramListing>
+However it is perfectly OK for some methods of a generic class to have
+generic default methods and others to have polymorphic default methods.
+</Para>
+</ListItem>
+
+<ListItem>
+<Para>
+The type variable(s) in the type pattern for a generic method declaration
+scope over the right hand side. So this is legal (note the use of the type variable ``p'' in a type signature on the right hand side:
+<ProgramListing>
+ class Foo a where
+ op :: a -> Bool
+ op {| p :*: q |} (x :*: y) = op (x :: p)
+ ...
+</ProgramListing>
+</Para>
+</ListItem>
+
+<ListItem>
+<Para>
+The type patterns in a generic default method must take one of the forms:
+<ProgramListing>
+ a :+: b
+ a :*: b
+ Unit
+</ProgramListing>
+where "a" and "b" are type variables. Furthermore, all the type patterns for
+a single type constructor (<Literal>:*:</Literal>, say) must be identical; they
+must use the same type variables. So this is illegal:
+<ProgramListing>
+ class Foo a where
+ op :: a -> Bool
+ op {| a :+: b |} (Inl x) = True
+ op {| p :+: q |} (Inr y) = False
+</ProgramListing>
+The type patterns must be identical, even in equations for different methods of the class.
+So this too is illegal:
+<ProgramListing>
+ class Foo a where
+ op1 :: a -> Bool
+ op {| a :*: b |} (Inl x) = True
+
+ op2 :: a -> Bool
+ op {| p :*: q |} (Inr y) = False
+</ProgramListing>
+(The reason for this restriction is that we gather all the equations for a particular type consructor
+into a single generic instance declaration.)
+</Para>
+</ListItem>
+
+<ListItem>
+<Para>
+A generic method declaration must give a case for each of the three type constructors.
+</Para>
+</ListItem>
+
+<ListItem>
+<Para>
+The type for a generic method can be built only from:
+ <ItemizedList>
+ <ListItem> <Para> Function arrows </Para> </ListItem>
+ <ListItem> <Para> Type variables </Para> </ListItem>
+ <ListItem> <Para> Tuples </Para> </ListItem>
+ <ListItem> <Para> Arbitrary types not involving type variables </Para> </ListItem>
+ </ItemizedList>
+Here are some example type signatures for generic methods:
+<ProgramListing>
+ op1 :: a -> Bool
+ op2 :: Bool -> (a,Bool)
+ op3 :: [Int] -> a -> a
+ op4 :: [a] -> Bool
+</ProgramListing>
+Here, op1, op2, op3 are OK, but op4 is rejected, because it has a type variable
+inside a list.
+</Para>
+<Para>
+This restriction is an implementation restriction: we just havn't got around to
+implementing the necessary bidirectional maps over arbitrary type constructors.
+It would be relatively easy to add specific type constructors, such as Maybe and list,
+to the ones that are allowed.</para>
+</ListItem>
+
+<ListItem>
+<Para>
+In an instance declaration for a generic class, the idea is that the compiler
+will fill in the methods for you, based on the generic templates. However it can only
+do so if
+ <ItemizedList>
+ <ListItem>
+ <Para>
+ The instance type is simple (a type constructor applied to type variables, as in Haskell 98).
+ </Para>
+ </ListItem>
+ <ListItem>
+ <Para>
+ No constructor of the instance type has unboxed fields.
+ </Para>
+ </ListItem>
+ </ItemizedList>
+(Of course, these things can only arise if you are already using GHC extensions.)
+However, you can still give an instance declarations for types which break these rules,
+provided you give explicit code to override any generic default methods.
+</Para>
+</ListItem>
+
+</ItemizedList>
+</Para>
+
+<Para>
+The option <Option>-ddump-deriv</Option> dumps incomprehensible stuff giving details of
+what the compiler does with generic declarations.
+</Para>
+
+</Sect2>
+
+<Sect2> <Title> Another example </Title>
+<Para>
+Just to finish with, here's another example I rather like:
+<ProgramListing>
+ class Tag a where
+ nCons :: a -> Int
+ nCons {| Unit |} _ = 1
+ nCons {| a :*: b |} _ = 1
+ nCons {| a :+: b |} _ = nCons (bot::a) + nCons (bot::b)
+
+ tag :: a -> Int
+ tag {| Unit |} _ = 1
+ tag {| a :*: b |} _ = 1
+ tag {| a :+: b |} (Inl x) = tag x
+ tag {| a :+: b |} (Inr y) = nCons (bot::a) + tag y
+</ProgramListing>
+</Para>
+</Sect2>
+</Sect1>
+
<!-- Emacs stuff:
;;; Local Variables: ***
;;; mode: sgml ***