%
-% $Id: glasgow_exts.vsgml,v 1.2 1998/07/20 16:16:34 sof Exp $
+% $Id: glasgow_exts.vsgml,v 1.3 1998/12/02 13:20:38 simonm Exp $
%
% GHC Language Extensions.
%
GHC's type system supports explicit unversal 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>Calling out to C:</tag>
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
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>
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.
+
+<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>
projects / ghc-hetmet.git / blobdiff