%
-% $Id: glasgow_exts.vsgml,v 1.1 1998/01/30 17:02:18 simonm Exp $
+% $Id: glasgow_exts.vsgml,v 1.12 1999/07/14 11:33:10 simonmar Exp $
%
% GHC Language Extensions.
%
<tag>Local universal quantification:</tag>
-GHC's type system supports explicit unversal quantification in
+GHC's type system supports explicit universal quantification in
constructor fields and function arguments. This is useful for things
-like defining @runST@ from the state-thread world amongst other
-things. See Section <ref name="Local universal quantification"
-id="universal-quantification">.
+like defining @runST@ from the state-thread world. See Section <ref
+name="Local universal quantification" id="universal-quantification">.
+
+<tag>Extistentially quantification in data types:</tag>
+
+Some or all of the type variables in a datatype declaration may be
+<em>existentially quantified</em>. More details in Section <ref
+name="Existential Quantification" id="existential-quantification">.
+
+<tag>Scoped type variables:</tag>
+
+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 Section <ref name="Scoped Type Variables"
+id="scoped-type-variables">.
<tag>Calling out to C:</tag>
can dangle around your neck. Please see Section <ref name="Calling~C
directly from Haskell" id="glasgow-ccalls">.
+<tag>Pragmas</tag>
+
+Pragmas are special instructions to the compiler placed in the source
+file. The pragmas GHC supports are described in Section <ref
+name="Pragmas" id="pragmas">.
+
+<tag>Rewrite rules:</tag>
+
+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 Section <ref name="Rewrite Rules"
+id="rewrite-rules">.
+
</descrip>
Before you get too carried away working at the lowest level (e.g.,
might expect; e.g., @(+#)@ is addition on @Int#@s, and is the
machine-addition that we all know and love---usually one instruction.
-A numerically-intensive program using unboxed types can go a <em>lot</em>
-faster than its ``standard'' counterpart---we saw a threefold speedup
-on one example.
+There are some restrictions on the use of unboxed types, the main one
+being that you can't pass an unboxed value to a polymorphic function
+or store one in a polymorphic data type. This rules out things like
+@[Int#]@ (ie. lists of unboxed integers). The reason for this
+restriction is that polymorphic arguments and constructor fields are
+assumed to be pointers: if an unboxed integer is stored in one of
+these, the garbage collector would attempt to follow it, leading to
+unpredictable space leaks. Or a @seq@ operation on the polymorphic
+component may attempt to dereference the pointer, with disastrous
+results. Even worse, the unboxed value might be larger than a pointer
+(@Double#@ for instance).
+
+Nevertheless, A numerically-intensive program using unboxed types can
+go a <em>lot</em> faster than its ``standard'' counterpart---we saw a
+threefold speedup on one example.
Please see Section <ref name="The module PrelGHC: really primitive
stuff" id="ghc-libs-ghc"> for the details of unboxed types and the
<em>in-place</em>.
<tag>``Static'' (in C land):</tag>
-A C~routine may pass an @Addr#@ pointer back into Haskell land. There
+A C routine may pass an @Addr#@ pointer back into Haskell land. There
are then primitive operations with which you may merrily grab values
over in C land, by indexing off the ``static'' pointer.
<tag>``Stable'' pointers:</tag>
If, for some reason, you wish to hand a Haskell pointer (i.e.,
-<em>not</em> an unboxed value) to a C~routine, you first make the
+<em>not</em> an unboxed value) to a C routine, you first make the
pointer ``stable,'' so that the garbage collector won't forget that it
exists. That is, GHC provides a safe way to pass Haskell pointers to
C.
<tag>``Foreign objects'':</tag>
A ``foreign object'' is a safe way to pass an external object (a
-C~allocated pointer, say) to Haskell and have Haskell do the Right
+C-allocated pointer, say) to Haskell and have Haskell do the Right
Thing when it no longer references the object. So, for example, C
could pass a large bitmap over to Haskell and say ``please free this
memory when you're done with it.''
</descrip>
-The libraries section give more details on all these ``primitive
+The libraries section gives more details on all these ``primitive
array'' types and the operations on them, Section <ref name="The GHC
Prelude and Libraries" id="ghc-prelude">. Some of these extensions
are also supported by Hugs, and the supporting libraries are described
document.
%************************************************************************
-%* *
-<sect1>Using your own @mainIO@
-<label id="own-mainIO">
-<p>
-<nidx>mainIO, rolling your own</nidx>
-<nidx>GHCmain, module containing mainIO</nidx>
-%* *
-%************************************************************************
-
-Normally, the GHC runtime system begins things by called an internal
-function
-
-<tscreen><verb>
- mainIO :: IO ()
-</verb></tscreen>
-
- which, in turn, fires up your @Main.main@. The standard
-definition of @mainIO@ looks like this:
-
-<tscreen><verb>
- mainIO = catch Main.main
- (\err -> error ("I/O error: " ++ show err ++ "\n"))
-</verb></tscreen>
-
-That is, all it does is run @Main.main@, catching any I/O errors that
-occur and displaying them on standard error before exiting the
-program.
-
-To subvert the above process, you need only provide a @mainIO@ of your
-own (in a module named @PrelMain@).
-
-Here's a little example, stolen from Alastair Reid:
-
-<tscreen><verb>
-module GHCmain ( mainIO ) where
-
-import GlaExts
-
-mainIO :: IO ()
-mainIO = do
- _ccall_ sleep 5
- _ccall_ printf "%d\n" (14::Int)
-</verb></tscreen>
-
-%************************************************************************
%* *
<sect1>Calling~C directly from Haskell
<label id="glasgow-ccalls">
corraled in a few modules, rather than sprinkled all over your code.
It will then be quite easy to update later on.
-WARNING AS OF 2.03: Yes, the @_ccall_@ stuff probably <em>will
-change</em>, to something better, of course! One step in that
-direction is Green Card, a foreign function interface pre-processor
-for Haskell (``Glasgow'' Haskell in particular) --- check out
-
-<tscreen><verb>
-ftp://ftp.dcs.gla.ac.uk/pub/haskell/glasgow/green-card.ANNOUNCE
-ftp://ftp.dcs.gla.ac.uk/pub/haskell/glasgow/green-card-src.tar.gz
-</verb></tscreen>
-
%************************************************************************
%* *
<sect2>@_ccall_@ and @_casm_@: an introduction
through a native-code generator):
<tscreen><verb>
+import Addr
+import CString
+
oldGetEnv name
- = _casm_ ``%r = getenv((char *) %0);'' name >>= \ litstring@(A# str#) ->
+ = _casm_ ``%r = getenv((char *) %0);'' name >>= \ litstring ->
return (
- if (litstring == ``NULL'') then
+ if (litstring == nullAddr) then
Left ("Fail:oldGetEnv:"++name)
else
- Right (unpackCString# str#)
+ Right (unpackCString litstring)
)
</verb></tscreen>
easy way to do simple C~casting. Everything said about @_ccall_@ goes
for @_casm_@ as well.
+The use of @_casm_@ in your code does pose a problem to the compiler
+when it comes to generating an interface file for a freshly compiled
+module. Included in an interface file is the unfolding (if any) of a
+declaration. However, if a declaration's unfolding happens to contain
+a @_casm_@, its unfolding will <em/not/ be emitted into the interface
+file even if it qualifies by all the other criteria. The reason why
+the compiler prevents this from happening is that unfolding @_casm_@s
+into an interface file unduly constrains how code that import your
+module have to be compiled. If an imported declaration is unfolded and
+it contains a @_casm_@, you now have to be using a compiler backend
+capable of dealing with it (i.e., the C compiler backend). If you are
+using the C compiler backend, the unfolded @_casm_@ may still cause you
+problems since the C code snippet it contains may mention CPP symbols
+that were in scope when compiling the original module are not when
+compiling the importing module.
+
+If you're willing to put up with the drawbacks of doing cross-module
+inlining of C code (GHC - A Better C Compiler :-), the option
+@-funfold-casms-in-hi-file@ will turn off the default behaviour.
+<nidx>-funfold-casms-in-hi-file option</nidx>
+
+%************************************************************************
+%* *
+<sect2>Literal-literals
+<label id="glasgow-literal-literals">
+<p>
+<nidx>Literal-literals</nidx>
+%* *
+%************************************************************************
+
+The literal-literal argument to @_casm_@ can be made use of separately
+from the @_casm_@ construct itself. Indeed, we've already used it:
+
+<tscreen><verb>
+fooH :: Char -> Int -> Double -> Word -> IO Double
+fooH c i d w = _ccall_ fooC (``stdin''::Addr) c i d w
+</verb></tscreen>
+
+The first argument that's passed to @fooC@ is given as a literal-literal,
+that is, a literal chunk of C code that will be inserted into the generated
+@.hc@ code at the right place.
+
+A literal-literal is restricted to having a type that's an instance of
+the @CCallable@ class, see <ref name="CCallable" id="ccall-gotchas">
+for more information.
+
+Notice that literal-literals are by their very nature unfriendly to
+native code generators, so exercise judgement about whether or not to
+make use of them in your code.
+
%************************************************************************
%* *
<sect2>Using function headers
You can find appropriate definitions for @StgInt@, @StgForeignObj@,
etc using @gcc@ on your architecture by consulting
-@ghc/includes/StgTypes.lh@. The following table summarises the
+@ghc/includes/StgTypes.h@. The following table summarises the
relationship between Haskell types and C types.
<tabular ca="ll">
<nidx>enterInt</nidx>
<nidx>enterFloat</nidx>
-% ToDo ADR: test these functions!
-
Note Bene: @_ccall_GC_@<nidx>_ccall_GC_</nidx> must be used if any of
these functions are used.
%************************************************************************
%* *
-<sect2>Pointing outside the Haskell heap
+<sect2>Foreign objects: pointing outside the Haskell heap
<label id="glasgow-foreignObjs">
<p>
<nidx>foreign objects (Glasgow extension)</nidx>
within Haskell.
<tscreen><verb>
-void StgPerformGarbageCollection()
+void GarbageCollect()
performGC :: IO ()
</verb></tscreen>
More information on the programmers' interface to @ForeignObj@ can be
-found in Section <ref name="Foreign objects" id="sec:foreign-obj">.
+found in the library documentation.
%************************************************************************
%* *
<label id="ccall-gotchas">
<p>
<nidx>C call dangers</nidx>
+<nidx>CCallable</nidx>
+<nidx>CReturnable</nidx>
%* *
%************************************************************************
id="glasgow-foreign-headers"> says more about this...)
This scheme is the <em>only</em> way that you will get <em>any</em>
-typechecking of your @_ccall_@s. (It shouldn't be that way,
-but...)
+typechecking of your @_ccall_@s. (It shouldn't be that way, but...).
+GHC will pass the flag @-Wimplicit@ to gcc so that you'll get warnings
+if any @_ccall_@ed functions have no prototypes.
<item>
Try to avoid @_ccall_@s to C~functions that take @float@
@ForeignObjs@ | Yes | Yes | see later @@
</tabular>
+Actually, the @Word@ type is defined as being the same size as a
+pointer on the target architecture, which is <em>probably</em>
+@unsigned long int@.
+
The brave and careful programmer can add their own instances of these
classes for the following types:
your life.
<item> If you call out to C code which may trigger the Haskell garbage
-collector (examples of this later...), then you must use the
-@_ccall_GC_@<nidx>_ccall_GC_ primitive</nidx> or
+collector or create new threads (examples of this later...), then you
+must use the @_ccall_GC_@<nidx>_ccall_GC_ primitive</nidx> or
@_casm_GC_@<nidx>_casm_GC_ primitive</nidx> variant of C-calls. (This
does not work with the native code generator - use @\fvia-C@.) This
stuff is hairy with a capital H! </itemize>
<label id="multi-param-type-classes">
<p>
-(ToDo)
+This section documents GHC's implementation of multi-paramter type
+classes. There's lots of background in the paper <url name="Type
+classes: exploring the design space"
+url="http://www.dcs.gla.ac.uk/~simonpj/multi.ps.gz"> (Simon Peyton
+Jones, Mark Jones, Erik Meijer).
+
+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.)
+
+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.
+
+<sect2>Types
+<p>
+
+There are the following restrictions on the form of a qualified
+type:
+
+<tscreen><verb>
+ forall tv1..tvn (c1, ...,cn) => type
+</verb></tscreen>
+
+(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 Section <ref
+name="Explicit universal quantification"
+id="universal-quantification">).
+
+<enum>
+
+<item> <bf>Each universally quantified type variable
+@tvi@ must be mentioned (i.e. appear free) in @type@</bf>.
+
+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:
+
+<tscreen><verb>
+ forall a. Eq a => Int
+</verb></tscreen>
+
+When a value with this type was used, the constraint <tt>Eq tv</tt>
+would be introduced where <tt>tv</tt> is a fresh type variable, and
+(in the dictionary-translation implementation) the value would be
+applied to a dictionary for <tt>Eq tv</tt>. The difficulty is that we
+can never know which instance of <tt>Eq</tt> to use because we never
+get any more information about <tt>tv</tt>.
+
+<item> <bf>Every constraint @ci@ must mention at least one of the
+universally quantified type variables @tvi@</bf>.
+
+For example, this type is OK because <tt>C a b</tt> mentions the
+universally quantified type variable <tt>b</tt>:
+
+<tscreen><verb>
+ forall a. C a b => burble
+</verb></tscreen>
+
+The next type is illegal because the constraint <tt>Eq b</tt> does not
+mention <tt>a</tt>:
+
+<tscreen><verb>
+ forall a. Eq b => burble
+</verb></tscreen>
+
+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.
+
+</enum>
+
+These restrictions apply to all types, whether declared in a type signature
+or inferred.
+
+Unlike Haskell 1.4, constraints in types do <bf>not</bf> have to be of
+the form <em>(class type-variables)</em>. Thus, these type signatures
+are perfectly OK
+
+<tscreen><verb>
+ f :: Eq (m a) => [m a] -> [m a]
+ g :: Eq [a] => ...
+</verb></tscreen>
+
+This choice recovers principal types, a property that Haskell 1.4 does not have.
+
+<sect2>Class declarations
+<p>
+
+<enum>
+
+<item> <bf>Multi-parameter type classes are permitted</bf>. For example:
+
+<tscreen><verb>
+ class Collection c a where
+ union :: c a -> c a -> c a
+ ...etc..
+</verb></tscreen>
+
+
+<item> <bf>The class hierarchy must be acyclic</bf>. However, the definition
+of "acyclic" involves only the superclass relationships. For example,
+this is OK:
+
+<tscreen><verb>
+ class C a where {
+ op :: D b => a -> b -> b
+ }
+
+ class C a => D a where { ... }
+</verb></tscreen>
+
+Here, <tt>C</tt> is a superclass of <tt>D</tt>, but it's OK for a
+class operation <tt>op</tt> of <tt>C</tt> to mention <tt>D</tt>. (It
+would not be OK for <tt>D</tt> to be a superclass of <tt>C</tt>.)
+
+<item> <bf>There are no restrictions on the context in a class declaration
+(which introduces superclasses), except that the class hierarchy must
+be acyclic</bf>. So these class declarations are OK:
+
+<tscreen><verb>
+ class Functor (m k) => FiniteMap m k where
+ ...
+
+ class (Monad m, Monad (t m)) => Transform t m where
+ lift :: m a -> (t m) a
+</verb></tscreen>
+
+<item> <bf>In the signature of a class operation, every constraint
+must mention at least one type variable that is not a class type
+variable</bf>.
+
+Thus:
+
+<tscreen><verb>
+ class Collection c a where
+ mapC :: Collection c b => (a->b) -> c a -> c b
+</verb></tscreen>
+
+is OK because the constraint <tt>(Collection a b)</tt> mentions
+<tt>b</tt>, even though it also mentions the class variable
+<tt>a</tt>. On the other hand:
+
+<tscreen><verb>
+ class C a where
+ op :: Eq a => (a,b) -> (a,b)
+</verb></tscreen>
+
+is not OK because the constraint <tt>(Eq a)</tt> mentions on the class
+type variable <tt>a</tt>, but not <tt>b</tt>. However, any such
+example is easily fixed by moving the offending context up to the
+superclass context:
+
+<tscreen><verb>
+ class Eq a => C a where
+ op ::(a,b) -> (a,b)
+</verb></tscreen>
+
+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.
+
+<item> <bf>The type of each class operation must mention <em/all/ of
+the class type variables</bf>. For example:
+
+<tscreen><verb>
+ class Coll s a where
+ empty :: s
+ insert :: s -> a -> s
+</verb></tscreen>
+
+is not OK, because the type of <tt>empty</tt> doesn't mention
+<tt>a</tt>. 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, <tt>Coll</tt> might be rewritten
+
+<tscreen><verb>
+ class Coll s a where
+ empty :: s a
+ insert :: s a -> a -> s a
+</verb></tscreen>
+
+which makes the connection between the type of a collection of
+<tt>a</tt>'s (namely <tt>(s a)</tt>) and the element type <tt>a</tt>.
+Occasionally this really doesn't work, in which case you can split the
+class like this:
+
+<tscreen><verb>
+ class CollE s where
+ empty :: s
+
+ class CollE s => Coll s a where
+ insert :: s -> a -> s
+</verb></tscreen>
+
+</enum>
+
+<sect2>Instance declarations
+<p>
+
+<enum>
+
+<item> <bf>Instance declarations may not overlap</bf>. The two instance
+declarations
+
+<tscreen><verb>
+ instance context1 => C type1 where ...
+ instance context2 => C type2 where ...
+</verb></tscreen>
+
+"overlap" if @type1@ and @type2@ unify
+
+However, if you give the command line option
+@-fallow-overlapping-instances@<nidx>-fallow-overlapping-instances
+option</nidx> then two overlapping instance declarations are permitted
+iff
+
+<itemize>
+<item> EITHER @type1@ and @type2@ do not unify
+<item> OR @type2@ is a substitution instance of @type1@
+ (but not identical to @type1@)
+<item> OR vice versa
+</itemize>
+
+Notice that these rules
+
+<itemize>
+<item> make it clear which instance decl to use
+ (pick the most specific one that matches)
+
+<item> do not mention the contexts @context1@, @context2@
+ Reason: you can pick which instance decl
+ "matches" based on the type.
+</itemize>
+
+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 <tt>Main</tt>. 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 <tt>Main</tt>.)
+
+<item> <bf>There are no restrictions on the type in an instance
+<em/head/, except that at least one must not be a type variable</bf>.
+The instance "head" is the bit after the "=>" in an instance decl. For
+example, these are OK:
+
+<tscreen><verb>
+ instance C Int a where ...
+
+ instance D (Int, Int) where ...
+
+ instance E [[a]] where ...
+</verb></tscreen>
+
+Note that instance heads <bf>may</bf> contain repeated type variables.
+For example, this is OK:
+
+<tscreen><verb>
+ instance Stateful (ST s) (MutVar s) where ...
+</verb></tscreen>
+
+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:
+
+<tscreen><verb>
+ instance C a => C a where ...
+</verb></tscreen>
+
+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:
+
+<tscreen><verb>
+ instance C a where
+ op = ... -- Default
+</verb></tscreen>
+
+Second, sometimes you might want to use the following to get the
+effect of a "class synonym":
+
+<tscreen><verb>
+ class (C1 a, C2 a, C3 a) => C a where { }
+
+ instance (C1 a, C2 a, C3 a) => C a where { }
+</verb></tscreen>
+
+This allows you to write shorter signatures:
+
+<tscreen><verb>
+ f :: C a => ...
+</verb></tscreen>
+
+instead of
+
+<tscreen><verb>
+ f :: (C1 a, C2 a, C3 a) => ...
+</verb></tscreen>
+
+I'm on the lookout for a simple rule that preserves decidability while
+allowing these idioms. The experimental flag
+@-fallow-undecidable-instances@<nidx>-fallow-undecidable-instances
+option</nidx> lifts this restriction, allowing all the types in an
+instance head to be type variables.
+
+<item> <bf>Unlike Haskell 1.4, instance heads may use type
+synonyms</bf>. As always, using a type synonym is just shorthand for
+writing the RHS of the type synonym definition. For example:
+
+<tscreen><verb>
+ type Point = (Int,Int)
+ instance C Point where ...
+ instance C [Point] where ...
+</verb></tscreen>
+
+is legal. However, if you added
+
+<tscreen><verb>
+ instance C (Int,Int) where ...
+</verb></tscreen>
+
+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:
+
+<tscreen><verb>
+ type P a = [[a]]
+ instance Monad P where ...
+</verb></tscreen>
+
+This design decision is independent of all the others, and easily
+reversed, but it makes sense to me.
+
+<item><bf>The types in an instance-declaration <em/context/ must all
+be type variables</bf>. Thus
+
+<tscreen><verb>
+ instance C a b => Eq (a,b) where ...
+</verb></tscreen>
+
+is OK, but
-<sect1> Local universal quantification
+<tscreen><verb>
+ instance C Int b => Foo b where ...
+</verb></tscreen>
+
+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 <tt>-fallow-undecidable-instances</tt> you 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 <tt>-fcontext-stack</tt><em/N/.
+
+</enum>
+
+% -----------------------------------------------------------------------------
+<sect1>Explicit universal quantification
<label id="universal-quantification">
<p>
-(ToDo)
+GHC now allows you to write explicitly quantified types. GHC's
+syntax for this now agrees with Hugs's, namely:
+
+<tscreen><verb>
+ forall a b. (Ord a, Eq b) => a -> b -> a
+</verb></tscreen>
+
+The context is, of course, optional. You can't use <tt>forall</tt> as
+a type variable any more!
+
+Haskell type signatures are implicitly quantified. The <tt>forall</tt>
+allows us to say exactly what this means. For example:
+
+<tscreen><verb>
+ g :: b -> b
+</verb></tscreen>
+
+means this:
+
+<tscreen><verb>
+ g :: forall b. (b -> b)
+</verb></tscreen>
+
+The two are treated identically.
+
+<sect2>Universally-quantified data type fields
+<label id="univ">
+<p>
+
+In a <tt>data</tt> or <tt>newtype</tt> declaration one can quantify
+the types of the constructor arguments. Here are several examples:
+
+<tscreen><verb>
+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
+ }
+
+newtype Swizzle = MkSwizzle (Ord a => [a] -> [a])
+</verb></tscreen>
+
+The constructors now have so-called <em/rank 2/ polymorphic
+types, in which there is a for-all in the argument types.:
+
+<tscreen><verb>
+T1 :: forall a. (forall b. b -> b -> b) -> a -> T1 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
+</verb></tscreen>
+
+Notice that you don't need to use a <tt>forall</tt> if there's an
+explicit context. For example in the first argument of the
+constructor <tt>MkSwizzle</tt>, an implicit "<tt>forall a.</tt>" is
+prefixed to the argument type. The implicit <tt>forall</tt>
+quantifies all type variables that are not already in scope, and are
+mentioned in the type quantified over.
+
+As for type signatures, implicit quantification happens for non-overloaded
+types too. So if you write this:
+<tscreen><verb>
+ data T a = MkT (Either a b) (b -> b)
+</verb></tscreen>
+it's just as if you had written this:
+<tscreen><verb>
+ data T a = MkT (forall b. Either a b) (forall b. b -> b)
+</verb></tscreen>
+That is, since the type variable <tt>b</tt> isn't in scope, it's
+implicitly universally quantified. (Arguably, it would be better
+to <em>require</em> explicit quantification on constructor arguments
+where that is what is wanted. Feedback welcomed.)
+
+<sect2> Construction
+<p>
+
+You construct values of types <tt>T1, MonadT, Swizzle</tt> by applying
+the constructor to suitable values, just as usual. For example,
+
+<tscreen><verb>
+(T1 (\xy->x) 3) :: T Int
+
+(MkSwizzle sort) :: Swizzle
+(MkSwizzle reverse) :: Swizzle
+
+(let r x = Just x
+ b m k = case m of
+ Just y -> k y
+ Nothing -> Nothing
+ in
+ MkMonad r b) :: MonadT Maybe
+</verb></tscreen>
+
+The type of the argument can, as usual, be more general than the type
+required, as <tt>(MkSwizzle reverse)</tt> shows. (<tt>reverse</tt>
+does not need the <tt>Ord</tt> constraint.)
+
+<sect2>Pattern matching
+<p>
+
+When you use pattern matching, the bound variables may now have
+polymorphic types. For example:
+
+<tscreen><verb>
+ f :: T a -> a -> (a, Char)
+ f (T1 f k) x = (f k x, f 'c' 'd')
+
+ 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)
+</verb></tscreen>
+
+In the function <tt>h</tt> we use the record selectors <tt>return</tt>
+and <tt>bind</tt> to extract the polymorphic bind and return functions
+from the <tt>MonadT</tt> data structure, rather than using pattern
+matching.
+
+You cannot pattern-match against an argument that is polymorphic.
+For example:
+<tscreen><verb>
+ newtype TIM s a = TIM (ST s (Maybe a))
+
+ runTIM :: (forall s. TIM s a) -> Maybe a
+ runTIM (TIM m) = runST m
+</verb></tscreen>
+
+Here the pattern-match fails, because you can't pattern-match against
+an argument of type <tt>(forall s. TIM s a)</tt>. Instead you
+must bind the variable and pattern match in the right hand side:
+<tscreen><verb>
+ runTIM :: (forall s. TIM s a) -> Maybe a
+ runTIM tm = case tm of { TIM m -> runST m }
+</verb></tscreen>
+The <tt>tm</tt> on the right hand side is (invisibly) instantiated, like
+any polymorphic value at its occurrence site, and now you can pattern-match
+against it.
+
+<sect2>The partial-application restriction
+<p>
+
+There is really only one way in which data structures with polymorphic
+components might surprise you: you must not partially apply them.
+For example, this is illegal:
+
+<tscreen><verb>
+ map MkSwizzle [sort, reverse]
+</verb></tscreen>
+
+The restriction is this: <em>every subexpression of the program must
+have a type that has no for-alls, except that in a function
+application (f e1 ... en) the partial applications are not subject to
+this rule</em>. The restriction makes type inference feasible.
+
+In the illegal example, the sub-expression <tt>MkSwizzle</tt> has the
+polymorphic type <tt>(Ord b => [b] -> [b]) -> Swizzle</tt> and is not
+a sub-expression of an enclosing application. On the other hand, this
+expression is OK:
+
+<tscreen><verb>
+ map (T1 (\a b -> a)) [1,2,3]
+</verb></tscreen>
+
+even though it involves a partial application of <tt>T1</tt>, because
+the sub-expression <tt>T1 (\a b -> a)</tt> has type <tt>Int -> T
+Int</tt>.
+
+<sect2>Type signatures
+<label id="sigs">
+<p>
+
+Once you have data constructors with universally-quantified fields, or
+constants such as <tt>runST</tt> that have rank-2 types, it isn't long
+before you discover that you need more! Consider:
+
+<tscreen><verb>
+ mkTs f x y = [T1 f x, T1 f y]
+</verb></tscreen>
+
+<tt>mkTs</tt> is a fuction that constructs some values of type
+<tt>T</tt>, using some pieces passed to it. The trouble is that since
+<tt>f</tt> is a function argument, Haskell assumes that it is
+monomorphic, so we'll get a type error when applying <tt>T1</tt> to
+it. This is a rather silly example, but the problem really bites in
+practice. Lots of people trip over the fact that you can't make
+"wrappers functions" for <tt>runST</tt> for exactly the same reason.
+In short, it is impossible to build abstractions around functions with
+rank-2 types.
+
+The solution is fairly clear. We provide the ability to give a rank-2
+type signature for <em>ordinary</em> functions (not only data
+constructors), thus:
+
+<tscreen><verb>
+ mkTs :: (forall b. b -> b -> b) -> a -> [T a]
+ mkTs f x y = [T1 f x, T1 f y]
+</verb></tscreen>
+
+This type signature tells the compiler to attribute <tt>f</tt> with
+the polymorphic type <tt>(forall b. b -> b -> b)</tt> when type
+checking the body of <tt>mkTs</tt>, so now the application of
+<tt>T1</tt> is fine.
+
+There are two restrictions:
+
+<itemize>
+<item> You can only define a rank 2 type, specified by the following
+grammar:
+
+<tscreen><verb>
+ rank2type ::= [forall tyvars .] [context =>] funty
+ funty ::= ([forall tyvars .] [context =>] ty) -> funty
+ | ty
+ ty ::= ...current Haskell monotype syntax...
+</verb></tscreen>
+
+Informally, the universal quantification must all be right at the beginning,
+or at the top level of a function argument.
+
+<item> There is a restriction on the definition of a function whose
+type signature is a rank-2 type: the polymorphic arguments must be
+matched on the left hand side of the "<tt>=</tt>" sign. You can't
+define <tt>mkTs</tt> like this:
+
+<tscreen><verb>
+ mkTs :: (forall b. b -> b -> b) -> a -> [T a]
+ mkTs = \ f x y -> [T1 f x, T1 f y]
+</verb></tscreen>
+
+
+The same partial-application rule applies to ordinary functions with
+rank-2 types as applied to data constructors.
+
+</itemize>
+
+% -----------------------------------------------------------------------------
+<sect1>Existentially quantified data constructors
+<label id="existential-quantification">
+<p>
+
+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 <tt>hbc</tt> Haskell compiler for several years, and
+proved very useful. Here's the idea. Consider the declaration:
+
+<tscreen><verb>
+ data Foo = forall a. MkFoo a (a -> Bool)
+ | Nil
+</verb></tscreen>
+
+The data type <tt>Foo</tt> has two constructors with types:
+
+<tscreen><verb>
+ MkFoo :: forall a. a -> (a -> Bool) -> Foo
+ Nil :: Foo
+</verb></tscreen>
+
+Notice that the type variable <tt>a</tt> in the type of <tt>MkFoo</tt>
+does not appear in the data type itself, which is plain <tt>Foo</tt>.
+For example, the following expression is fine:
+
+<tscreen><verb>
+ [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo]
+</verb></tscreen>
+
+Here, <tt>(MkFoo 3 even)</tt> packages an integer with a function
+<tt>even</tt> that maps an integer to <tt>Bool</tt>; and <tt>MkFoo 'c'
+isUpper</tt> packages a character with a compatible function. These
+two things are each of type <tt>Foo</tt> and can be put in a list.
+
+What can we do with a value of type <tt>Foo</tt>?. In particular,
+what happens when we pattern-match on <tt>MkFoo</tt>?
+
+<tscreen><verb>
+ f (MkFoo val fn) = ???
+</verb></tscreen>
+
+Since all we know about <tt>val</tt> and <tt>fn</tt> is that they
+are compatible, the only (useful) thing we can do with them is to
+apply <tt>fn</tt> to <tt>val</tt> to get a boolean. For example:
+
+<tscreen><verb>
+ f :: Foo -> Bool
+ f (MkFoo val fn) = fn val
+</verb></tscreen>
+
+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.
+
+<sect2>Why existential?
+<label id="existential">
+<p>
+
+What has this to do with <em>existential</em> quantification?
+Simply that <tt>MkFoo</tt> has the (nearly) isomorphic type
+
+<tscreen><verb>
+ MkFoo :: (exists a . (a, a -> Bool)) -> Foo
+</verb></tscreen>
+
+But Haskell programmers can safely think of the ordinary
+<em>universally</em> quantified type given above, thereby avoiding
+adding a new existential quantification construct.
+
+<sect2>Type classes
+<p>
+
+An easy extension (implemented in <tt>hbc</tt>) is to allow
+arbitrary contexts before the constructor. For example:
+
+<tscreen><verb>
+ data Baz = forall a. Eq a => Baz1 a a
+ | forall b. Show b => Baz2 b (b -> b)
+</verb></tscreen>
+
+The two constructors have the types you'd expect:
+
+<tscreen><verb>
+ Baz1 :: forall a. Eq a => a -> a -> Baz
+ Baz2 :: forall b. Show b => b -> (b -> b) -> Baz
+</verb></tscreen>
+
+But when pattern matching on <tt>Baz1</tt> the matched values can be compared
+for equality, and when pattern matching on <tt>Baz2</tt> the first matched
+value can be converted to a string (as well as applying the function to it).
+So this program is legal:
+
+<tscreen><verb>
+ f :: Baz -> String
+ f (Baz1 p q) | p == q = "Yes"
+ | otherwise = "No"
+ f (Baz1 v fn) = show (fn v)
+</verb></tscreen>
+
+Operationally, in a dictionary-passing implementation, the
+constructors <tt>Baz1</tt> and <tt>Baz2</tt> must store the
+dictionaries for <tt>Eq</tt> and <tt>Show</tt> respectively, and
+extract it on pattern matching.
+
+Notice the way that the syntax fits smoothly with that used for
+universal quantification earlier.
+
+<sect2>Restrictions
+<p>
+
+There are several restrictions on the ways in which existentially-quantified
+constructors can be use.
+
+<itemize>
+
+<item> 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:
+
+<tscreen><verb>
+ f1 (MkFoo a f) = a
+</verb></tscreen>
+
+Here, the type bound by <tt>MkFoo</tt> "escapes", because <tt>a</tt>
+is the result of <tt>f1</tt>. One way to see why this is wrong is to
+ask what type <tt>f1</tt> has:
+
+<tscreen><verb>
+ f1 :: Foo -> a -- Weird!
+</verb></tscreen>
+
+What is this "<tt>a</tt>" in the result type? Clearly we don't mean
+this:
+
+<tscreen><verb>
+ f1 :: forall a. Foo -> a -- Wrong!
+</verb></tscreen>
+
+The original program is just plain wrong. Here's another sort of error
+
+<tscreen><verb>
+ f2 (Baz1 a b) (Baz1 p q) = a==q
+</verb></tscreen>
+
+It's ok to say <tt>a==b</tt> or <tt>p==q</tt>, but
+<tt>a==q</tt> is wrong because it equates the two distinct types arising
+from the two <tt>Baz1</tt> constructors.
+
+
+<item>You can't pattern-match on an existentially quantified
+constructor in a <tt>let</tt> or <tt>where</tt> group of
+bindings. So this is illegal:
+
+<tscreen><verb>
+ f3 x = a==b where { Baz1 a b = x }
+</verb></tscreen>
+
+You can only pattern-match
+on an existentially-quantified constructor in a <tt>case</tt> 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.
+
+<item>You can't use existential quantification for <tt>newtype</tt>
+declarations. So this is illegal:
+
+<tscreen><verb>
+ newtype T = forall a. Ord a => MkT a
+</verb></tscreen>
+
+Reason: a value of type <tt>T</tt> must be represented as a pair
+of a dictionary for <tt>Ord t</tt> and a value of type <tt>t</tt>.
+That contradicts the idea that <tt>newtype</tt> should have no
+concrete representation. You can get just the same efficiency and effect
+by using <tt>data</tt> instead of <tt>newtype</tt>. If there is no
+overloading involved, then there is more of a case for allowing
+an existentially-quantified <tt>newtype</tt>, because the <tt>data</tt>
+because the <tt>data</tt> version does carry an implementation cost,
+but single-field existentially quantified constructors aren't much
+use. So the simple restriction (no existential stuff on <tt>newtype</tt>)
+stands, unless there are convincing reasons to change it.
+</itemize>
+
+
+<sect1> <idx/Assertions/
+<label id="sec:assertions">
+<p>
+
+If you want to make use of assertions in your standard Haskell code, you
+could define a function like the following:
+
+<tscreen><verb>
+assert :: Bool -> a -> a
+assert False x = error "assertion failed!"
+assert _ x = x
+</verb></tscreen>
+
+which works, but gives you back a less than useful error message --
+an assertion failed, but which and where?
+
+One way out is to define an extended <tt/assert/ function which also
+takes a descriptive string to include in the error message and
+perhaps combine this with the use of a pre-processor which inserts
+the source location where <tt/assert/ was used.
+
+Ghc offers a helping hand here, doing all of this for you. For every
+use of <tt/assert/ in the user's source:
+
+<tscreen><verb>
+kelvinToC :: Double -> Double
+kelvinToC k = assert (k >= 0.0) (k+273.15)
+</verb></tscreen>
+
+Ghc will rewrite this to also include the source location where the
+assertion was made,
+
+<tscreen><verb>
+assert pred val ==> assertError "Main.hs|15" pred val
+</verb></tscreen>
+
+The rewrite is only performed by the compiler when it spots
+applications of <tt>Exception.assert</tt>, so you can still define and
+use your own versions of <tt/assert/, should you so wish. If not,
+import <tt/Exception/ to make use <tt/assert/ in your code.
+
+To have the compiler ignore uses of assert, use the compiler option
+@-fignore-asserts@. <nidx>-fignore-asserts option</nidx> That is,
+expressions of the form @assert pred e@ will be rewritten to @e@.
+
+Assertion failures can be caught, see the documentation for the
+Hugs/GHC Exception library for information of how.
+
+% -----------------------------------------------------------------------------
+<sect1>Scoped Type Variables
+<label id="scoped-type-variables">
+<p>
+
+A <em/pattern type signature/ can introduce a <em/scoped type
+variable/. For example
+
+<tscreen><verb>
+f (xs::[a]) = ys ++ ys
+ where
+ ys :: [a]
+ ys = reverse xs
+</verb></tscreen>
+
+The pattern @(xs::[a])@ includes a type signature for @xs@.
+This brings the type variable @a@ into scope; it scopes over
+all the patterns and right hand sides for this equation for @f@.
+In particular, it is in scope at the type signature for @y@.
+
+At ordinary type signatures, such as that for @ys@, any type variables
+mentioned in the type signature <em/that are not in scope/ are
+implicitly universally quantified. (If there are no type variables in
+scope, all type variables mentioned in the signature are universally
+quantified, which is just as in Haskell 98.) In this case, since @a@
+is in scope, it is not universally quantified, so the type of @ys@ is
+the same as that of @xs@. In Haskell 98 it is not possible to declare
+a type for @ys@; a major benefit of scoped type variables is that
+it becomes possible to do so.
+
+Scoped type variables are implemented in both GHC and Hugs. Where the
+implementations differ from the specification below, those differences
+are noted.
+
+So much for the basic idea. Here are the details.
+
+<sect2>Scope and implicit quantification
+<p>
+
+<itemize>
+<item> All the type variables mentioned in the patterns for a single
+function definition equation, that are not already in scope,
+are brought into scope by the patterns. We describe this set as
+the <em/type variables bound by the equation/.
+
+<item> The type variables thus brought into scope may be mentioned
+in ordinary type signatures or pattern type signatures anywhere within
+their scope.
+
+<item> In ordinary type signatures, any type variable mentioned in the
+signature that is in scope is <em/not/ universally quantified.
+
+<item> Ordinary type signatures do not bring any new type variables
+into scope (except in the type signature itself!). So this is illegal:
+
+<tscreen><verb>
+ f :: a -> a
+ f x = x::a
+</verb></tscreen>
+
+It's illegal because @a@ is not in scope in the body of @f@,
+so the ordinary signature @x::a@ is equivalent to @x::forall a.a@;
+and that is an incorrect typing.
+
+<item> There is no implicit universal quantification on pattern type
+signatures, nor may one write an explicit @forall@ type in a pattern
+type signature. The pattern type signature is a monotype.
+
+<item>
+The type variables in the head of a @class@ or @instance@ declaration
+scope over the methods defined in the @where@ part. For example:
+
+<tscreen><verb>
+ class C a where
+ op :: [a] -> a
+
+ op xs = let ys::[a]
+ ys = reverse xs
+ in
+ head ys
+</verb></tscreen>
+
+(Not implemented in Hugs yet, Dec 98).
+</itemize>
+
+<sect2>Polymorphism
+<p>
+
+<itemize>
+<item> Pattern type signatures are completely orthogonal to ordinary, separate
+type signatures. The two can be used independently or together. There is
+no scoping associated with the names of the type variables in a separate type signature.
+
+<tscreen><verb>
+ f :: [a] -> [a]
+ f (xs::[b]) = reverse xs
+</verb></tscreen>
+
+<item> The function must be polymorphic in the type variables
+bound by all its equations. Operationally, the type variables bound
+by one equation must not:
+
+<itemize>
+<item> Be unified with a type (such as @Int@, or @[a]@).
+<item> Be unified with a type variable free in the environment.
+<item> Be unified with each other. (They may unify with the type variables
+bound by another equation for the same function, of course.)
+</itemize>
+
+For example, the following all fail to type check:
+
+<tscreen><verb>
+ f (x::a) (y::b) = [x,y] -- a unifies with b
+
+ g (x::a) = x + 1::Int -- a unifies with Int
+
+ h x = let k (y::a) = [x,y] -- a is free in the
+ in k x -- environment
+
+ k (x::a) True = ... -- a unifies with Int
+ k (x::Int) False = ...
+
+ w :: [b] -> [b]
+ w (x::a) = x -- a unifies with [b]
+</verb></tscreen>
+
+<item> The pattern-bound type variable may, however, be constrained
+by the context of the principal type, thus:
+
+<tscreen><verb>
+ f (x::a) (y::a) = x+y*2
+</verb></tscreen>
+
+gets the inferred type: @forall a. Num a => a -> a -> a@.
+</itemize>
+
+<sect2>Result type signatures
+<p>
+
+<itemize>
+<item> The result type of a function can be given a signature,
+thus:
+
+<tscreen><verb>
+ f (x::a) :: [a] = [x,x,x]
+</verb></tscreen>
+
+The final @":: [a]"@ after all the patterns gives a signature to the
+result type. Sometimes this is the only way of naming the type variable
+you want:
+
+<tscreen><verb>
+ f :: Int -> [a] -> [a]
+ f n :: ([a] -> [a]) = let g (x::a, y::a) = (y,x)
+ in \xs -> map g (reverse xs `zip` xs)
+</verb></tscreen>
+
+</itemize>
+
+Result type signatures are not yet implemented in Hugs.
+
+<sect2>Pattern signatures on other constructs
+<p>
+
+<itemize>
+<item> A pattern type signature can be on an arbitrary sub-pattern, not
+just on a variable:
+
+<tscreen><verb>
+ f ((x,y)::(a,b)) = (y,x) :: (b,a)
+</verb></tscreen>
+
+<item> Pattern type signatures, including the result part, can be used
+in lambda abstractions:
+
+<tscreen><verb>
+ (\ (x::a, y) :: a -> x)
+</verb></tscreen>
+
+Type variables bound by these patterns must be polymorphic in
+the sense defined above.
+For example:
+
+<tscreen><verb>
+ f1 (x::c) = f1 x -- ok
+ f2 = \(x::c) -> f2 x -- not ok
+</verb></tscreen>
+
+Here, @f1@ is OK, but @f2@ is not, because @c@ gets unified
+with a type variable free in the environment, in this
+case, the type of @f2@, which is in the environment when
+the lambda abstraction is checked.
+
+<item> Pattern type signatures, including the result part, can be used
+in @case@ expressions:
+
+<tscreen><verb>
+ case e of { (x::a, y) :: a -> x }
+</verb></tscreen>
+
+The pattern-bound type variables must, as usual,
+be polymorphic in the following sense: each case alternative,
+considered as a lambda abstraction, must be polymorphic.
+Thus this is OK:
+
+<tscreen><verb>
+ case (True,False) of { (x::a, y) -> x }
+</verb></tscreen>
+
+Even though the context is that of a pair of booleans,
+the alternative itself is polymorphic. Of course, it is
+also OK to say:
+
+<tscreen><verb>
+ case (True,False) of { (x::Bool, y) -> x }
+</verb></tscreen>
+
+<item>
+To avoid ambiguity, the type after the ``@::@'' in a result
+pattern signature on a lambda or @case@ must be atomic (i.e. a single
+token or a parenthesised type of some sort). To see why,
+consider how one would parse this:
+
+<tscreen><verb>
+ \ x :: a -> b -> x
+</verb></tscreen>
+
+<item> Pattern type signatures that bind new type variables
+may not be used in pattern bindings at all.
+So this is illegal:
+
+<tscreen><verb>
+ f x = let (y, z::a) = x in ...
+</verb></tscreen>
+
+But these are OK, because they do not bind fresh type variables:
+
+<tscreen><verb>
+ f1 x = let (y, z::Int) = x in ...
+ f2 (x::(Int,a)) = let (y, z::a) = x in ...
+</verb></tscreen>
+
+However a single variable is considered a degenerate function binding,
+rather than a degerate pattern binding, so this is permitted, even
+though it binds a type variable:
+
+<tscreen><verb>
+ f :: (b->b) = \(x::b) -> x
+</verb></tscreen>
+
+</itemize>
+Such degnerate function bindings do not fall under the monomorphism
+restriction. Thus:
+
+<tscreen><verb>
+ g :: a -> a -> Bool = \x y. x==y
+</verb></tscreen>
+
+Here @g@ has type @forall a. Eq a => a -> a -> Bool@, just as if
+@g@ had a separate type signature. Lacking a type signature, @g@
+would get a monomorphic type.
+
+<sect2>Existentials
+<p>
+
+<itemize>
+<item> Pattern type signatures can bind existential type variables.
+For example:
+
+<tscreen><verb>
+ data T = forall a. MkT [a]
+
+ f :: T -> T
+ f (MkT [t::a]) = MkT t3
+ where
+ t3::[a] = [t,t,t]
+</verb></tscreen>
+
+</itemize>
+
+%-----------------------------------------------------------------------------
+<sect1>Pragmas
+<label id="pragmas">
+<p>
+
+GHC supports several pragmas, or instructions to the compiler placed
+in the source code. Pragmas don't affect the meaning of the program,
+but they might affect the efficiency of the generated code.
+
+<sect2>INLINE pragma
+<label id="inline-pragma">
+<nidx>INLINE pragma</nidx>
+<nidx>pragma, INLINE</nidx>
+<p>
+
+GHC (with @-O@, as always) tries to inline (or ``unfold'')
+functions/values that are ``small enough,'' thus avoiding the call
+overhead and possibly exposing other more-wonderful optimisations.
+
+You will probably see these unfoldings (in Core syntax) in your
+interface files.
+
+Normally, if GHC decides a function is ``too expensive'' to inline, it
+will not do so, nor will it export that unfolding for other modules to
+use.
+
+The sledgehammer you can bring to bear is the
+@INLINE@<nidx>INLINE pragma</nidx> pragma, used thusly:
+<tscreen><verb>
+key_function :: Int -> String -> (Bool, Double)
+
+#ifdef __GLASGOW_HASKELL__
+{-# INLINE key_function #-}
+#endif
+</verb></tscreen>
+(You don't need to do the C pre-processor carry-on unless you're going
+to stick the code through HBC---it doesn't like @INLINE@ pragmas.)
+
+The major effect of an @INLINE@ pragma is to declare a function's
+``cost'' to be very low. The normal unfolding machinery will then be
+very keen to inline it.
+
+An @INLINE@ pragma for a function can be put anywhere its type
+signature could be put.
+
+@INLINE@ pragmas are a particularly good idea for the
+@then@/@return@ (or @bind@/@unit@) functions in a monad.
+For example, in GHC's own @UniqueSupply@ monad code, we have:
+<tscreen><verb>
+#ifdef __GLASGOW_HASKELL__
+{-# INLINE thenUs #-}
+{-# INLINE returnUs #-}
+#endif
+</verb></tscreen>
+
+<sect2>NOINLINE pragma
+<label id="noinline-pragma">
+<p>
+<nidx>NOINLINE pragma</nidx>
+<nidx>pragma, NOINLINE</nidx>
+
+The @NOINLINE@ pragma does exactly what you'd expect: it stops the
+named function from being inlined by the compiler. You shouldn't ever
+need to do this, unless you're very cautious about code size.
+
+<sect2>SPECIALIZE pragma
+<label id="specialize-pragma">
+<p>
+<nidx>SPECIALIZE pragma</nidx>
+<nidx>pragma, SPECIALIZE</nidx>
+<nidx>overloading, death to</nidx>
+
+(UK spelling also accepted.) For key overloaded functions, you can
+create extra versions (NB: more code space) specialised to particular
+types. Thus, if you have an overloaded function:
+
+<tscreen><verb>
+hammeredLookup :: Ord key => [(key, value)] -> key -> value
+</verb></tscreen>
+
+If it is heavily used on lists with @Widget@ keys, you could
+specialise it as follows:
+<tscreen><verb>
+{-# SPECIALIZE hammeredLookup :: [(Widget, value)] -> Widget -> value #-}
+</verb></tscreen>
+
+To get very fancy, you can also specify a named function to use for
+the specialised value, by adding @= blah@, as in:
+<tscreen><verb>
+{-# SPECIALIZE hammeredLookup :: ...as before... = blah #-}
+</verb></tscreen>
+It's <em>Your Responsibility</em> to make sure that @blah@ really
+behaves as a specialised version of @hammeredLookup@!!!
+
+NOTE: the @=blah@ feature isn't implemented in GHC 4.xx.
+
+An example in which the @= blah@ form will Win Big:
+<tscreen><verb>
+toDouble :: Real a => a -> Double
+toDouble = fromRational . toRational
+
+{-# SPECIALIZE toDouble :: Int -> Double = i2d #-}
+i2d (I# i) = D# (int2Double# i) -- uses Glasgow prim-op directly
+</verb></tscreen>
+The @i2d@ function is virtually one machine instruction; the
+default conversion---via an intermediate @Rational@---is obscenely
+expensive by comparison.
+
+By using the US spelling, your @SPECIALIZE@ pragma will work with
+HBC, too. Note that HBC doesn't support the @= blah@ form.
+
+A @SPECIALIZE@ pragma for a function can be put anywhere its type
+signature could be put.
+
+<sect2>SPECIALIZE instance pragma
+<label id="specialize-instance-pragma">
+<p>
+<nidx>SPECIALIZE pragma</nidx>
+<nidx>overloading, death to</nidx>
+Same idea, except for instance declarations. For example:
+<tscreen><verb>
+instance (Eq a) => Eq (Foo a) where { ... usual stuff ... }
+
+{-# SPECIALIZE instance Eq (Foo [(Int, Bar)] #-}
+</verb></tscreen>
+Compatible with HBC, by the way.
+
+<sect2>LINE pragma
+<label id="line-pragma">
+<p>
+<nidx>LINE pragma</nidx>
+<nidx>pragma, LINE</nidx>
+
+This pragma is similar to C's @#line@ pragma, and is mainly for use in
+automatically generated Haskell code. It lets you specify the line
+number and filename of the original code; for example
+
+<tscreen><verb>
+{-# LINE 42 "Foo.vhs" #-}
+</verb></tscreen>
+
+if you'd generated the current file from something called @Foo.vhs@
+and this line corresponds to line 42 in the original. GHC will adjust
+its error messages to refer to the line/file named in the @LINE@
+pragma.
+
+<sect2>RULES pragma
+<p>
+The RULES pragma lets you specify rewrite rules. It is described in
+Section <ref name="Rewrite Rules"
+id="rewrite-rules">.
+
+%-----------------------------------------------------------------------------
+<sect1>Rewrite rules
+<label id="rewrite-rules">
+<nidx>RULES pagma</nidx>
+<nidx>pragma, RULES</nidx>
+<nidx>rewrite rules</nidx>
+<p>
+
+The programmer can specify rewrite rules as part of the source program
+(in a pragma). GHC applies these rewrite rules wherever it can.
+
+Here is an example:
+<tscreen><verb>
+ {-# RULES
+ "map/map" forall f,g,xs. map f (map g) xs = map (f.g) xs
+ #-}
+</verb></tscreen>
+
+<sect2>Syntax
+<p>
+
+From a syntactic point of view:
+<itemize>
+<item> Each rule has a name, enclosed in double quotes.
+<item> There may be zero or more rules in a @RULES@ pragma.
+<item> Layout applies in a @RULES@ pragma. Currently no new indentation level
+is set, so you must lay out your rules starting in the same column as the
+enclosing definitions.
+<item> Each variable mentioned in a rule must either be in scope (e.g. @map@),
+or bound by the @forall@ (e.g. @f@, @g@, @xs@). The variables bound by
+the @forall@ are called the <em>pattern</em> variables.
+<item> A pattern variable may optionally have a type signature.
+If its type is polymorphic, it <em>must</em> have a type signature.
+For example, here is the @foldr/build@ rule:
+<tscreen><verb>
+ "fold/build" forall k,z,g::forall b. (a->b->b) -> b -> b .
+ foldr k z (build g) = g k z
+</verb></tscreen>
+
+
+<item> The left hand side of a rule must consist of a top-level variable applied
+to arbitrary expressions. For example, this is <em>not</em> OK:
+<tscreen><verb>
+ "wrong1" forall e1,e2. case True of { True -> e1; False -> e2 } = e1
+ "wrong2" forall f. f True = True
+</verb></tscreen>
+In @"wrong1"@, the LHS is not an application; in @"wrong1"@, the LHS has a pattern variable
+in the head.
+<item> A rule does not need to be in the same module as (any of) the
+variables it mentions, though of course they need to be in scope.
+<item> Rules are automatically exported from a module, just as instance declarations are.
+</itemize>
+
+<sect2>Semantics
+<p>
+
+From a semantic point of view:
+<itemize>
+<item> Rules are only applied if you use the @-O@ flag.
+
+<item> Rules are regarded as left-to-right rewrite rules.
+When GHC finds an expression that is a substitution instance of the LHS
+of a rule, it replaces the expression by the (appropriately-substituted) RHS.
+By "a substitution instance" we mean that the LHS can be made equal to the
+expression by substituting for the pattern variables.
+
+<item> The LHS and RHS of a rule are typechecked, and must have the
+same type.
+
+<item> GHC makes absolutely no attempt to verify that the LHS and RHS
+of a rule have the same meaning. That is undecideable in general, and
+infeasible in most interesting cases. The responsibility is entirely the programmer's!
+
+<item> GHC makes no attempt to make sure that the rules are confluent or
+terminating. For example:
+<tscreen><verb>
+ "loop" forall x,y. f x y = f y x
+</verb></tscreen>
+This rule will cause the compiler to go into an infinite loop.
+
+<item> GHC currently uses a very simple, syntactic, matching algorithm
+for matching a rule LHS with an expression. It seeks a substitution
+which makes the LHS and expression syntactically equal modulo: alpha
+conversion, and (I think) eta conversion. But not beta conversion (that's
+called higher-order matching).
+
+<item> GHC keeps trying to apply the rules as it optimises the program.
+For example, consider:
+<tscreen><verb>
+ let s = map f
+ t = map g
+ in
+ s (t xs)
+</verb></tscreen>
+The expression @s (t xs)@ does not match the rule @"map/map"@, but GHC
+will substitute for @s@ and @t@, giving an expression which does match.
+If @s@ or @t@ was (a) used more than once, and (b) large or a redex, then it would
+not be substituted, and the rule would not fire.
+
+<item> In the earlier phases of compilation, GHC inlines <em>nothing
+that appears on the LHS of a rule</em>, because once you have substituted
+for something you can't match against it (given the simple minded
+matching). So if you write the rule
+<tscreen><verb>
+ "map/map" forall f,g. map f . map g = map (f.g)
+</verb></tscreen>
+this <em>won't</em> match the expression @map f (map g xs)@.
+It will only match something written with explicit use of ".".
+Well, not quite. It <em>will</em> match the expression
+<tscreen><verb>
+ wibble f g xs
+</verb></tscreen>
+where @wibble@ is defined:
+<tscreen><verb>
+ wibble f g = map f . map g
+</verb></tscreen>
+because @wibble@ will be inlined (it's small).
+
+Later on in compilation, GHC starts inlining even things on the
+LHS of rules, but still leaves the rules enabled. This inlining
+policy is controlled by the per-simplification-pass flag @-finline-phase@n.
+</itemize>
+
+
+<sect2>Controlling what's going on
+<p>
+
+<itemize>
+<item> Use @-fddump-rules@ to see what transformation rules GHC is using.
+<item> Use @-fddump-simpl-stats@ to see what rules are being fired.
+<item> The defintion of (say) @build@ in @PrelBase.lhs@ looks llike this:
+<tscreen><verb>
+ build :: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a]
+ {-# INLINE build #-}
+ build g = g (:) []
+</verb></tscreen>
+Notice the @INLINE@! That prevents @(:)@ from being inlined when compiling
+@PrelBase@, so that an importing module will ``see'' the @(:)@, and can
+match it on the LHS of a rule. @INLINE@ prevents any inlining happening
+in the RHS of the @INLINE@ thing. I regret the delicacy of this.
+
+<item> In @ghc/lib/std/PrelBase.lhs@ look at the rules for @map@ to
+see how to write rules that will do fusion and yet give an efficient
+program even if fusion doesn't happen. More rules in @PrelList.lhs@.
+</itemize>
projects / ghc-hetmet.git / blobdiff