X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fdocs%2Fusers_guide%2Fglasgow_exts.sgml;h=12e828495e9ffd697da642fbdf06564b4f41e029;hb=d28c5d2fb3510802c02f2650097e5dbac9353d0a;hp=0956fd162b5a17887bdc0385b92b4fe0e4fcf218;hpb=f3d376e190102c5e92f81a9f37c2f716f0c731d8;p=ghc-hetmet.git
diff --git a/ghc/docs/users_guide/glasgow_exts.sgml b/ghc/docs/users_guide/glasgow_exts.sgml
index 0956fd1..12e8284 100644
--- a/ghc/docs/users_guide/glasgow_exts.sgml
+++ b/ghc/docs/users_guide/glasgow_exts.sgml
@@ -2,17 +2,19 @@
language, GHCextensions, GHC
As with all known Haskell systems, GHC implements some extensions to
-the language. To use them, you'll need to give a
--fglasgow-exts option option.
+the language. They are all enabled by options; by default GHC
+understands only plain Haskell 98.
-Virtually all of the Glasgow extensions serve to give you access to
-the underlying facilities with which we implement Haskell. Thus, you
-can get at the Raw Iron, if you are willing to write some non-standard
-code at a more primitive level. You need not be “stuck” on
-performance because of the implementation costs of Haskell's
-“high-level” features—you can always code “under” them. In an extreme case, you can write all your time-critical code in C, and then just glue it together with Haskell!
+Some of the Glasgow extensions serve to give you access to the
+underlying facilities with which we implement Haskell. Thus, you can
+get at the Raw Iron, if you are willing to write some non-portable
+code at a more primitive level. You need not be “stuck”
+on performance because of the implementation costs of Haskell's
+“high-level” features—you can always code
+“under” them. In an extreme case, you can write all your
+time-critical code in C, and then just glue it together with Haskell!
@@ -20,8 +22,8 @@ Before you get too carried away working at the lowest level (e.g.,
sloshing MutableByteArray#s around your
program), you may wish to check if there are libraries that provide a
“Haskellised veneer” over the features you want. The
-separate libraries documentation describes all the libraries that come
-with GHC.
+separate libraries
+documentation describes all the libraries that come with GHC.
@@ -35,10 +37,38 @@ with GHC.
extensionsoptions controlling
- These flags control what variation of the language are
+ These flags control what variation of the language are
permitted. Leaving out all of them gives you standard Haskell
98.
+ NB. turning on an option that enables special syntax
+ might cause working Haskell 98 code to fail
+ to compile, perhaps because it uses a variable name which has
+ become a reserved word. So, together with each option below, we
+ list the special syntax which is enabled by this option. We use
+ notation and nonterminal names from the Haskell 98 lexical syntax
+ (see the Haskell 98 Report). There are two classes of special
+ syntax:
+
+
+
+ New reserved words and symbols: character sequences
+ which are no longer available for use as identifiers in the
+ program.
+
+
+ Other special syntax: sequences of characters that have
+ a different meaning when this particular option is turned
+ on.
+
+
+
+ We are only listing syntax changes here that might affect
+ existing working programs (i.e. "stolen" syntax). Many of these
+ extensions will also enable new context-free syntax, but in all
+ cases programs written to use the new syntax would not be
+ compilable without the option enabled.
+
@@ -49,6 +79,19 @@ with GHC.
Haskell 98 described in , except where otherwise
noted.
+
+ New reserved words: forall (only in
+ types), mdo.
+
+ Other syntax stolen:
+ varid{#},
+ char#,
+ string#,
+ integer#,
+ float#,
+ float##,
+ (#, #),
+ |), {|.
@@ -61,18 +104,8 @@ with GHC.
Haskell 98 Foreign Function Interface Addendum plus deprecated
syntax of previous versions of the FFI for backwards
compatibility.
-
-
-
- :
-
-
- This option enables the deprecated with
- keyword for implicit parameters; it is merely provided for backwards
- compatibility.
- It is independent of the
- flag.
+ New reserved words: foreign.
@@ -110,6 +143,23 @@ with GHC.
+
+
+
+ See . Independent of
+ .
+
+ New reserved words/symbols: rec,
+ proc, -<,
+ >-, -<<,
+ >>-.
+
+ Other syntax stolen: (|,
+ |).
+
+
+
+
@@ -118,34 +168,61 @@ with GHC.
-
-
-
- -fno-implicit-prelude
- option GHC normally imports
- Prelude.hi files for you. If you'd
- rather it didn't, then give it a
- option. The idea
- is that you can then import a Prelude of your own. (But
- don't call it Prelude; the Haskell
- module namespace is flat, and you must not conflict with
- any Prelude module.)
-
- Even though you have not imported the Prelude, most of
- the built-in syntax still refers to the built-in Haskell
- Prelude types and values, as specified by the Haskell
- Report. For example, the type [Int]
- still means Prelude.[] Int; tuples
- continue to refer to the standard Prelude tuples; the
- translation for list comprehensions continues to use
- Prelude.map etc.
-
- However, does
- change the handling of certain built-in syntax: see
- .
+
+
+
+ -fno-implicit-prelude
+ option GHC normally imports
+ Prelude.hi files for you. If you'd
+ rather it didn't, then give it a
+ option. The idea is
+ that you can then import a Prelude of your own. (But don't
+ call it Prelude; the Haskell module
+ namespace is flat, and you must not conflict with any
+ Prelude module.)
+
+ Even though you have not imported the Prelude, most of
+ the built-in syntax still refers to the built-in Haskell
+ Prelude types and values, as specified by the Haskell
+ Report. For example, the type [Int]
+ still means Prelude.[] Int; tuples
+ continue to refer to the standard Prelude tuples; the
+ translation for list comprehensions continues to use
+ Prelude.map etc.
+
+ However, does
+ change the handling of certain built-in syntax: see .
+
+
-
-
+
+
+
+ Enables Template Haskell (see ). Currently also implied by
+ .
+
+ Syntax stolen: [|,
+ [e|, [p|,
+ [d|, [t|,
+ $(,
+ $varid.
+
+
+
+
+
+
+ Enables implicit parameters (see ). Currently also implied by
+ .
+
+ Syntax stolen:
+ ?varid,
+ %varid.
+
+
@@ -406,9 +483,9 @@ tuples to avoid unnecessary allocation during sequences of operations.
import qualified Control.Monad.ST.Strict as ST
- Hierarchical modules have an impact on the way that GHC
- searches for files. For a description, see .
+ For details on how GHC searches for source and interface
+ files in the presence of hierarchical modules, see .GHC comes with a large collection of libraries arranged
hierarchically; see the accompanying library documentation.
@@ -635,32 +712,6 @@ This name is not supported by GHC.
- Infix type constructors
-
-GHC supports infix type constructors, much as it supports infix data constructors. For example:
-
- infixl 5 :+:
-
- data a :+: b = Inl a | Inr b
-
- f :: a `Either` b -> a :+: b
- f (Left x) = Inl x
-
-
-The lexical
-syntax of an infix type constructor is just like that of an infix data constructor: either
-it's an operator beginning with ":", or it is an ordinary (alphabetic) type constructor enclosed in
-back-quotes.
-
-
-When you give a fixity declaration, the fixity applies to both the data constructor and the
-type constructor with the specified name. You cannot give different fixities to the type constructor T
-and the data constructor T.
-
-
-
-
-
@@ -791,7 +842,11 @@ and the data constructor T.
Type system extensions
-
+
+
+Data types and type synonyms
+
+Data types with no constructorsWith the flag, GHC lets you declare
@@ -809,9 +864,9 @@ not * then an explicit kind annotation must be used
Such data types have only one value, namely bottom.
Nevertheless, they can be useful when defining "phantom types".
-
+
-
+Infix type constructors
@@ -862,590 +917,673 @@ like expressions. More specifically:
-
+
-
-Explicitly-kinded quantification
+
+Liberalised type synonyms
-Haskell infers the kind of each type variable. Sometimes it is nice to be able
-to give the kind explicitly as (machine-checked) documentation,
-just as it is nice to give a type signature for a function. On some occasions,
-it is essential to do so. For example, in his paper "Restricted Data Types in Haskell" (Haskell Workshop 1999)
-John Hughes had to define the data type:
-
- data Set cxt a = Set [a]
- | Unused (cxt a -> ())
-
-The only use for the Unused constructor was to force the correct
-kind for the type variable cxt.
-
-
-GHC now instead allows you to specify the kind of a type variable directly, wherever
-a type variable is explicitly bound. Namely:
+Type synonmys are like macros at the type level, and
+GHC does validity checking on types only after expanding type synonyms.
+That means that GHC can be very much more liberal about type synonyms than Haskell 98:
-data declarations:
-
- data Set (cxt :: * -> *) a = Set [a]
-
-type declarations:
-
- type T (f :: * -> *) = f Int
-
-class declarations:
-
- class (Eq a) => C (f :: * -> *) a where ...
-
-forall's in type signatures:
-
- f :: forall (cxt :: * -> *). Set cxt Int
-
-
-
+You can write a forall (including overloading)
+in a type synonym, thus:
+
+ type Discard a = forall b. Show b => a -> b -> (a, String)
-
-The parentheses are required. Some of the spaces are required too, to
-separate the lexemes. If you write (f::*->*) you
-will get a parse error, because "::*->*" is a
-single lexeme in Haskell.
-
+ f :: Discard a
+ f x y = (x, show y)
-
-As part of the same extension, you can put kind annotations in types
-as well. Thus:
-
- f :: (Int :: *) -> Int
- g :: forall a. a -> (a :: *)
-
-The syntax is
-
- atype ::= '(' ctype '::' kind ')
-
-The parentheses are required.
+ g :: Discard Int -> (Int,Bool) -- A rank-2 type
+ g f = f Int True
+
-
+
+
+You can write an unboxed tuple in a type synonym:
+
+ type Pr = (# Int, Int #)
-
-Class method types
-
-
-Haskell 98 prohibits class method types to mention constraints on the
-class type variable, thus:
+ h :: Int -> Pr
+ h x = (# x, x #)
+
+
+
+
+You can apply a type synonym to a forall type:
- class Seq s a where
- fromList :: [a] -> s a
- elem :: Eq a => a -> s a -> Bool
+ type Foo a = a -> a -> Bool
+
+ f :: Foo (forall b. b->b)
-The type of elem is illegal in Haskell 98, because it
-contains the constraint Eq a, constrains only the
-class type variable (in this case a).
+After expanding the synonym, f has the legal (in GHC) type:
+
+ f :: (forall b. b->b) -> (forall b. b->b) -> Bool
+
+
+
+
+You can apply a type synonym to a partially applied type synonym:
+
+ type Generic i o = forall x. i x -> o x
+ type Id x = x
+
+ foo :: Generic Id []
+
+After epxanding the synonym, foo has the legal (in GHC) type:
+
+ foo :: forall x. x -> [x]
+
+
+
+
+
-With the GHC lifts this restriction.
+GHC currently does kind checking before expanding synonyms (though even that
+could be changed.)
+
+After expanding type synonyms, GHC does validity checking on types, looking for
+the following mal-formedness which isn't detected simply by kind checking:
+
+
+Type constructor applied to a type involving for-alls.
+
+
+Unboxed tuple on left of an arrow.
+
+
+Partially-applied type synonym.
+
+
+So, for example,
+this will be rejected:
+
+ type Pr = (# Int, Int #)
-
+ h :: Pr -> Int
+ h x = ...
+
+because GHC does not allow unboxed tuples on the left of a function arrow.
+
+
-
-Multi-parameter type classes
+
+
+Existentially quantified data constructors
-This section documents GHC's implementation of multi-parameter type
-classes. There's lots of background in the paper Type
-classes: exploring the design space (Simon Peyton Jones, Mark
-Jones, Erik Meijer).
+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 hbc Haskell compiler for several years, and
+proved very useful. Here's the idea. Consider the declaration:
-
-
-Types
-
-GHC imposes the following restrictions on the form of a qualified
-type, whether declared in a type signature
-or inferred. Consider the type:
- forall tv1..tvn (c1, ...,cn) => type
+ data Foo = forall a. MkFoo a (a -> Bool)
+ | Nil
-(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 ).
-
-
-
+The data type Foo has two constructors with types:
+
- Each universally quantified type variable
-tvi must be reachable from type.
-
-A type variable is "reachable" if it it is functionally dependent
-(see )
-on the type variables free in type.
-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:
-
- forall a. Eq a => Int
+ MkFoo :: forall a. a -> (a -> Bool) -> Foo
+ Nil :: Foo
-
-When a value with this type was used, the constraint Eq tv
-would be introduced where tv is a fresh type variable, and
-(in the dictionary-translation implementation) the value would be
-applied to a dictionary for Eq tv. The difficulty is that we
-can never know which instance of Eq to use because we never
-get any more information about tv.
-
-
-
- Every constraint ci must mention at least one of the
-universally quantified type variables tvi.
-
-For example, this type is OK because C a b mentions the
-universally quantified type variable b:
+Notice that the type variable a in the type of MkFoo
+does not appear in the data type itself, which is plain Foo.
+For example, the following expression is fine:
+
+
- forall a. C a b => burble
+ [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo]
+
-The next type is illegal because the constraint Eq b does not
-mention a:
+
+Here, (MkFoo 3 even) packages an integer with a function
+even that maps an integer to Bool; and MkFoo 'c'
+isUpper packages a character with a compatible function. These
+two things are each of type Foo and can be put in a list.
+
+
+What can we do with a value of type Foo?. In particular,
+what happens when we pattern-match on MkFoo?
+
+
+
- forall a. Eq b => burble
+ f (MkFoo val fn) = ???
+
-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.
-
+
+Since all we know about val and fn is that they
+are compatible, the only (useful) thing we can do with them is to
+apply fn to val to get a boolean. For example:
-
-
+
+
+
+ f :: Foo -> Bool
+ f (MkFoo val fn) = fn val
+
+
+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.
+
+
+
+Why existential?
+
-Unlike Haskell 1.4, constraints in types do not have to be of
-the form (class type-variables). Thus, these type signatures
-are perfectly OK
+What has this to do with existential quantification?
+Simply that MkFoo has the (nearly) isomorphic type
- f :: Eq (m a) => [m a] -> [m a]
- g :: Eq [a] => ...
+ MkFoo :: (exists a . (a, a -> Bool)) -> Foo
-This choice recovers principal types, a property that Haskell 1.4 does not have.
+But Haskell programmers can safely think of the ordinary
+universally quantified type given above, thereby avoiding
+adding a new existential quantification construct.
-
+
-
-Class declarations
+
+Type classes
-
-
-
+An easy extension (implemented in hbc) is to allow
+arbitrary contexts before the constructor. For example:
+
- Multi-parameter type classes are permitted. For example:
-
- class Collection c a where
- union :: c a -> c a -> c a
- ...etc.
+data Baz = forall a. Eq a => Baz1 a a
+ | forall b. Show b => Baz2 b (b -> b)
-
-
-
-
- The class hierarchy must be acyclic. However, the definition
-of "acyclic" involves only the superclass relationships. For example,
-this is OK:
+The two constructors have the types you'd expect:
+
+
- class C a where {
- op :: D b => a -> b -> b
- }
-
- class C a => D a where { ... }
+Baz1 :: forall a. Eq a => a -> a -> Baz
+Baz2 :: forall b. Show b => b -> (b -> b) -> Baz
-
-Here, C is a superclass of D, but it's OK for a
-class operation op of C to mention D. (It
-would not be OK for D to be a superclass of C.)
-
-
-
- There are no restrictions on the context in a class declaration
-(which introduces superclasses), except that the class hierarchy must
-be acyclic. So these class declarations are OK:
+But when pattern matching on Baz1 the matched values can be compared
+for equality, and when pattern matching on Baz2 the first matched
+value can be converted to a string (as well as applying the function to it).
+So this program is legal:
+
+
- class Functor (m k) => FiniteMap m k where
- ...
-
- class (Monad m, Monad (t m)) => Transform t m where
- lift :: m a -> (t m) a
+ f :: Baz -> String
+ f (Baz1 p q) | p == q = "Yes"
+ | otherwise = "No"
+ f (Baz2 v fn) = show (fn v)
+
+
+
+Operationally, in a dictionary-passing implementation, the
+constructors Baz1 and Baz2 must store the
+dictionaries for Eq and Show respectively, and
+extract it on pattern matching.
+
+
+Notice the way that the syntax fits smoothly with that used for
+universal quantification earlier.
-
+
+
+
+Restrictions
+
+
+There are several restrictions on the ways in which existentially-quantified
+constructors can be use.
+
+
+
+
+
- All of the class type variables must be reachable (in the sense
-mentioned in )
-from the free varibles of each method type
-. For example:
+ 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:
- class Coll s a where
- empty :: s
- insert :: s -> a -> s
+f1 (MkFoo a f) = a
-is not OK, because the type of empty doesn't mention
-a. 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, Coll might be rewritten
+Here, the type bound by MkFoo "escapes", because a
+is the result of f1. One way to see why this is wrong is to
+ask what type f1 has:
- class Coll s a where
- empty :: s a
- insert :: s a -> a -> s a
+ f1 :: Foo -> a -- Weird!
-which makes the connection between the type of a collection of
-a's (namely (s a)) and the element type a.
-Occasionally this really doesn't work, in which case you can split the
-class like this:
+What is this "a" in the result type? Clearly we don't mean
+this:
- class CollE s where
- empty :: s
-
- class CollE s => Coll s a where
- insert :: s -> a -> s
+ f1 :: forall a. Foo -> a -- Wrong!
-
-
+The original program is just plain wrong. Here's another sort of error
-
-
+
+ f2 (Baz1 a b) (Baz1 p q) = a==q
+
-
-
-Instance declarations
+It's ok to say a==b or p==q, but
+a==q is wrong because it equates the two distinct types arising
+from the two Baz1 constructors.
-
-
+
+
- Instance declarations may not overlap. The two instance
-declarations
+You can't pattern-match on an existentially quantified
+constructor in a let or where group of
+bindings. So this is illegal:
- instance context1 => C type1 where ...
- instance context2 => C type2 where ...
+ f3 x = a==b where { Baz1 a b = x }
+Instead, use a case expression:
-"overlap" if type1 and type2 unify
+
+ f3 x = case x of Baz1 a b -> a==b
+
-However, if you give the command line option
--fallow-overlapping-instances
-option then overlapping instance declarations are permitted.
-However, GHC arranges never to commit to using an instance declaration
-if another instance declaration also applies, either now or later.
+In general, you can only pattern-match
+on an existentially-quantified constructor in a case 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.
-
- EITHER type1 and type2 do not unify
- OR type2 is a substitution instance of type1
-(but not identical to type1), or vice versa.
-
-
-
-Notice that these rules
-
-
+You can't use existential quantification for newtype
+declarations. So this is illegal:
+
+
+
+ newtype T = forall a. Ord a => MkT a
+
+
+
+Reason: a value of type T must be represented as a
+pair of a dictionary for Ord t and a value of type
+t. That contradicts the idea that
+newtype should have no concrete representation.
+You can get just the same efficiency and effect by using
+data instead of newtype. If
+there is no overloading involved, then there is more of a case for
+allowing an existentially-quantified newtype,
+because the data version does carry an
+implementation cost, but single-field existentially quantified
+constructors aren't much use. So the simple restriction (no
+existential stuff on newtype) stands, unless there
+are convincing reasons to change it.
-
- make it clear which instance decl to use
-(pick the most specific one that matches)
- do not mention the contexts context1, context2
-Reason: you can pick which instance decl
-"matches" based on the type.
-
-
+ You can't use deriving to define instances of a
+data type with existentially quantified data constructors.
+
+Reason: in most cases it would not make sense. For example:#
-
-However the rules are over-conservative. Two instance declarations can overlap,
-but it can still be clear in particular situations which to use. For example:
- instance C (Int,a) where ...
- instance C (a,Bool) where ...
+data T = forall a. MkT [a] deriving( Eq )
-These are rejected by GHC's rules, but it is clear what to do when trying
-to solve the constraint C (Int,Int) because the second instance
-cannot apply. Yell if this restriction bites you.
-
-
-GHC is also conservative about committing to an overlapping instance. For example:
+
+To derive Eq in the standard way we would need to have equality
+between the single component of two MkT constructors:
+
- class C a where { op :: a -> a }
- instance C [Int] where ...
- instance C a => C [a] where ...
-
- f :: C b => [b] -> [b]
- f x = op x
+instance Eq T where
+ (MkT a) == (MkT b) = ???
-From the RHS of f we get the constraint C [b]. But
-GHC does not commit to the second instance declaration, because in a paricular
-call of f, b might be instantiate to Int, so the first instance declaration
-would be appropriate. So GHC rejects the program. If you add
-GHC will instead silently pick the second instance, without complaining about
-the problem of subsequent instantiations.
-
-
-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 Main. 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 Main.)
+But a and b have distinct types, and so can't be compared.
+It's just about possible to imagine examples in which the derived instance
+would make sense, but it seems altogether simpler simply to prohibit such
+declarations. Define your own instances!
-
-
- There are no restrictions on the type in an instance
-head, except that at least one must not be a type variable.
-The instance "head" is the bit after the "=>" in an instance decl. For
-example, these are OK:
+
+
-
- instance C Int a where ...
+
+
- instance D (Int, Int) where ...
+
- instance E [[a]] where ...
-
-Note that instance heads may contain repeated type variables.
-For example, this is OK:
+
+Class declarations
+
+
+This section documents GHC's implementation of multi-parameter type
+classes. There's lots of background in the paper Type
+classes: exploring the design space (Simon Peyton Jones, Mark
+Jones, Erik Meijer).
+
+
+There are the following constraints on class declarations:
+
+
+
+
+ Multi-parameter type classes are permitted. For example:
- instance Stateful (ST s) (MutVar s) where ...
+ class Collection c a where
+ union :: c a -> c a -> c a
+ ...etc.
-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:
+
+
+
+
+
+
+ The class hierarchy must be acyclic. However, the definition
+of "acyclic" involves only the superclass relationships. For example,
+this is OK:
- instance C a => C a where ...
+ class C a where {
+ op :: D b => a -> b -> b
+ }
+
+ class C a => D a where { ... }
-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:
+Here, C is a superclass of D, but it's OK for a
+class operation op of C to mention D. (It
+would not be OK for D to be a superclass of C.)
+
+
+
+
+
+
+ There are no restrictions on the context in a class declaration
+(which introduces superclasses), except that the class hierarchy must
+be acyclic. So these class declarations are OK:
- instance C a where
- op = ... -- Default
+ class Functor (m k) => FiniteMap m k where
+ ...
+
+ class (Monad m, Monad (t m)) => Transform t m where
+ lift :: m a -> (t m) a
-Second, sometimes you might want to use the following to get the
-effect of a "class synonym":
+
+
+
-
- class (C1 a, C2 a, C3 a) => C a where { }
+
+ All of the class type variables must be reachable (in the sense
+mentioned in )
+from the free varibles of each method type
+. For example:
- instance (C1 a, C2 a, C3 a) => C a where { }
+
+
+ class Coll s a where
+ empty :: s
+ insert :: s -> a -> s
-This allows you to write shorter signatures:
+is not OK, because the type of empty doesn't mention
+a. 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, Coll might be rewritten
- f :: C a => ...
+ class Coll s a where
+ empty :: s a
+ insert :: s a -> a -> s a
-instead of
+which makes the connection between the type of a collection of
+a's (namely (s a)) and the element type a.
+Occasionally this really doesn't work, in which case you can split the
+class like this:
- f :: (C1 a, C2 a, C3 a) => ...
-
+ class CollE s where
+ empty :: s
+ class CollE s => Coll s a where
+ insert :: s -> a -> s
+
-I'm on the lookout for a simple rule that preserves decidability while
-allowing these idioms. The experimental flag
--fallow-undecidable-instances
-option lifts this restriction, allowing all the types in an
-instance head to be type variables.
-
-
-
- Unlike Haskell 1.4, instance heads may use type
-synonyms. As always, using a type synonym is just shorthand for
-writing the RHS of the type synonym definition. For example:
+
+
+
+Class method types
+
+Haskell 98 prohibits class method types to mention constraints on the
+class type variable, thus:
- type Point = (Int,Int)
- instance C Point where ...
- instance C [Point] where ...
+ class Seq s a where
+ fromList :: [a] -> s a
+ elem :: Eq a => a -> s a -> Bool
+The type of elem is illegal in Haskell 98, because it
+contains the constraint Eq a, constrains only the
+class type variable (in this case a).
+
+
+With the GHC lifts this restriction.
+
+
-is legal. However, if you added
+
+
+
+Type signatures
+The context of a type signature
+
+Unlike Haskell 98, constraints in types do not have to be of
+the form (class type-variable) or
+(class (type-variable type-variable ...)). Thus,
+these type signatures are perfectly OK
+
+ g :: Eq [a] => ...
+ g :: Ord (T a ()) => ...
+
+
+
+GHC imposes the following restrictions on the constraints in a type signature.
+Consider the type:
- instance C (Int,Int) where ...
+ forall tv1..tvn (c1, ...,cn) => type
+(Here, we write the "foralls" explicitly, although the Haskell source
+language omits them; in Haskell 98, 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 ).
+
-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:
+
+
+
+
+
+
+ Each universally quantified type variable
+tvi must be reachable from type.
+
+A type variable is "reachable" if it it is functionally dependent
+(see )
+on the type variables free in type.
+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:
- type P a = [[a]]
- instance Monad P where ...
+ forall a. Eq a => Int
-This design decision is independent of all the others, and easily
-reversed, but it makes sense to me.
+When a value with this type was used, the constraint Eq tv
+would be introduced where tv is a fresh type variable, and
+(in the dictionary-translation implementation) the value would be
+applied to a dictionary for Eq tv. The difficulty is that we
+can never know which instance of Eq to use because we never
+get any more information about tv.
-The types in an instance-declaration context must all
-be type variables. Thus
+ Every constraint ci must mention at least one of the
+universally quantified type variables tvi.
+
+For example, this type is OK because C a b mentions the
+universally quantified type variable b:
-instance C a b => Eq (a,b) where ...
+ forall a. C a b => burble
-is OK, but
+The next type is illegal because the constraint Eq b does not
+mention a:
-instance C Int b => Foo b where ...
+ forall a. Eq b => burble
-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 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 N.
+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.
@@ -1453,1135 +1591,1036 @@ with N.
-
-
-
-
-Implicit parameters
-
-
- 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.
-
-(Most of the following, stil rather incomplete, documentation is due to Jeff Lewis.)
+
+For-all hoisting
-A variable is called dynamically bound when it is bound by the calling
-context of a function and statically bound when bound by the callee's
-context. In Haskell, all variables are statically bound. Dynamic
-binding of variables is a notion that goes back to Lisp, but was later
-discarded in more modern incarnations, such as Scheme. Dynamic binding
-can be very confusing in an untyped language, and unfortunately, typed
-languages, in particular Hindley-Milner typed languages like Haskell,
-only support static scoping of variables.
-
-
-However, by a simple extension to the type class system of Haskell, we
-can support dynamic binding. Basically, we express the use of a
-dynamically bound variable as a constraint on the type. These
-constraints lead to types of the form (?x::t') => t, which says "this
-function uses a dynamically-bound variable ?x
-of type t'". For
-example, the following expresses the type of a sort function,
-implicitly parameterized by a comparison function named cmp.
+It is often convenient to use generalised type synonyms (see ) at the right hand
+end of an arrow, thus:
- sort :: (?cmp :: a -> a -> Bool) => [a] -> [a]
+ type Discard a = forall b. a -> b -> a
+
+ g :: Int -> Discard Int
+ g x y z = x+y
+
+Simply expanding the type synonym would give
+
+ g :: Int -> (forall b. Int -> b -> Int)
+
+but GHC "hoists" the forall to give the isomorphic type
+
+ g :: forall b. Int -> Int -> b -> Int
+
+In general, the rule is this: to determine the type specified by any explicit
+user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly
+performs the transformation:
+
+ type1 -> forall a1..an. context2 => type2
+==>
+ forall a1..an. context2 => type1 -> type2
+
+(In fact, GHC tries to retain as much synonym information as possible for use in
+error messages, but that is a usability issue.) This rule applies, of course, whether
+or not the forall comes from a synonym. For example, here is another
+valid way to write g's type signature:
+
+ g :: Int -> Int -> forall b. b -> Int
-The dynamic binding constraints are just a new form of predicate in the type class system.
-An implicit parameter occurs in an expression using the special form ?x,
-where x is
-any valid identifier (e.g. ord ?x is a valid expression).
-Use of this construct also introduces a new
-dynamic-binding constraint in the type of the expression.
-For example, the following definition
-shows how we can define an implicitly parameterized sort function in
-terms of an explicitly parameterized sortBy function:
+When doing this hoisting operation, GHC eliminates duplicate constraints. For
+example:
- sortBy :: (a -> a -> Bool) -> [a] -> [a]
-
- sort :: (?cmp :: a -> a -> Bool) => [a] -> [a]
- sort = sortBy ?cmp
+ type Foo a = (?x::Int) => Bool -> a
+ g :: Foo (Foo Int)
+
+means
+
+ g :: (?x::Int) => Bool -> Bool -> Int
+
+
+
+
+
+
+Instance declarations
-Implicit-parameter type constraints
+Overlapping instances
-Dynamic binding constraints behave just like other type class
-constraints in that they are automatically propagated. Thus, when a
-function is used, its implicit parameters are inherited by the
-function that called it. For example, our sort function might be used
-to pick out the least value in a list:
+In general, instance declarations may not overlap. The two instance
+declarations
+
+
- least :: (?cmp :: a -> a -> Bool) => [a] -> a
- least xs = fst (sort xs)
+ instance context1 => C type1 where ...
+ instance context2 => C type2 where ...
-Without lifting a finger, the ?cmp parameter is
-propagated to become a parameter of least as well. With explicit
-parameters, the default is that parameters must always be explicit
-propagated. With implicit parameters, the default is to always
-propagate them.
+
+"overlap" if type1 and type2 unify.
-An implicit-parameter type constraint differs from other type class constraints in the
-following way: All uses of a particular implicit parameter must have
-the same type. This means that the type of (?x, ?x)
-is (?x::a) => (a,a), and not
-(?x::a, ?x::b) => (a, b), as would be the case for type
-class constraints.
+However, if you give the command line option
+-fallow-overlapping-instances
+option then overlapping instance declarations are permitted.
+However, GHC arranges never to commit to using an instance declaration
+if another instance declaration also applies, either now or later.
+
+
+
+
+
+ EITHER type1 and type2 do not unify
+
+
- You can't have an implicit parameter in the context of a class or instance
-declaration. For example, both these declarations are illegal:
+
+ OR type2 is a substitution instance of type1
+(but not identical to type1), or vice versa.
+
+
+
+Notice that these rules
+
+
+
+
+ make it clear which instance decl to use
+(pick the most specific one that matches)
+
+
+
+
+
+
+ do not mention the contexts context1, context2
+Reason: you can pick which instance decl
+"matches" based on the type.
+
+
+
+
+However the rules are over-conservative. Two instance declarations can overlap,
+but it can still be clear in particular situations which to use. For example:
- class (?x::Int) => C a where ...
- instance (?x::a) => Foo [a] where ...
+ instance C (Int,a) where ...
+ instance C (a,Bool) where ...
-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.
+These are rejected by GHC's rules, but it is clear what to do when trying
+to solve the constraint C (Int,Int) because the second instance
+cannot apply. Yell if this restriction bites you.
+
-Implicit-parameter constraints do not cause ambiguity. For example, consider:
+GHC is also conservative about committing to an overlapping instance. For example:
- f :: (?x :: [a]) => Int -> Int
- f n = n + length ?x
-
- g :: (Read a, Show a) => String -> String
- g s = show (read s)
+ class C a where { op :: a -> a }
+ instance C [Int] where ...
+ instance C a => C [a] where ...
+
+ f :: C b => [b] -> [b]
+ f x = op x
-Here, g has an ambiguous type, and is rejected, but f
-is fine. The binding for ?x at f's call site is
-quite unambiguous, and fixes the type a.
+From the RHS of f we get the constraint C [b]. But
+GHC does not commit to the second instance declaration, because in a paricular
+call of f, b might be instantiate to Int, so the first instance declaration
+would be appropriate. So GHC rejects the program. If you add
+GHC will instead silently pick the second instance, without complaining about
+the problem of subsequent instantiations.
+
+
+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 Main. 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 Main.)
-Implicit-parameter bindings
+Type synonyms in the instance head
-An implicit parameter is bound using the standard
-let or where binding forms.
-For example, we define the min function by binding
-cmp.
+Unlike Haskell 98, instance heads may use type
+synonyms. (The instance "head" is the bit after the "=>" in an instance decl.)
+As always, using a type synonym is just shorthand for
+writing the RHS of the type synonym definition. For example:
+
+
- min :: [a] -> a
- min = let ?cmp = (<=) in least
+ type Point = (Int,Int)
+ instance C Point where ...
+ instance C [Point] where ...
-
-
-A group of implicit-parameter bindings may occur anywhere a normal group of Haskell
-bindings can occur, except at top level. That is, they can occur in a let
-(including in a list comprehension, or do-notation, or pattern guards),
-or a where clause.
-Note the following points:
-
-
-An implicit-parameter binding group must be a
-collection of simple bindings to implicit-style variables (no
-function-style bindings, and no type signatures); these bindings are
-neither polymorphic or recursive.
-
-
-You may not mix implicit-parameter bindings with ordinary bindings in a
-single let
-expression; use two nested lets instead.
-(In the case of where you are stuck, since you can't nest where clauses.)
-
-
-You may put multiple implicit-parameter bindings in a
-single binding group; but they are not treated
-as a mutually recursive group (as ordinary let bindings are).
-Instead they are treated as a non-recursive group, simultaneously binding all the implicit
-parameter. The bindings are not nested, and may be re-ordered without changing
-the meaning of the program.
-For example, consider:
+
+is legal. However, if you added
+
+
- f t = let { ?x = t; ?y = ?x+(1::Int) } in ?x + ?y
+ instance C (Int,Int) where ...
-The use of ?x in the binding for ?y does not "see"
-the binding for ?x, so the type of f is
+
+
+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:
+
+
- f :: (?x::Int) => Int -> Int
+ type P a = [[a]]
+ instance Monad P where ...
-
-
-
-
-
-
-Linear implicit parameters
-
-
-Linear implicit parameters are an idea developed by Koen Claessen,
-Mark Shields, and Simon PJ. They address the long-standing
-problem that monads seem over-kill for certain sorts of problem, notably:
-
-
- distributing a supply of unique names
- distributing a suppply of random numbers
- distributing an oracle (as in QuickCheck)
-
+This design decision is independent of all the others, and easily
+reversed, but it makes sense to me.
-
-Linear implicit parameters are just like ordinary implicit parameters,
-except that they are "linear" -- that is, they cannot be copied, and
-must be explicitly "split" instead. Linear implicit parameters are
-written '%x' instead of '?x'.
-(The '/' in the '%' suggests the split!)
-
-For example:
-
- import GHC.Exts( Splittable )
+
- data NameSupply = ...
-
- splitNS :: NameSupply -> (NameSupply, NameSupply)
- newName :: NameSupply -> Name
+
+Undecidable instances
- instance Splittable NameSupply where
- split = splitNS
+An instance declaration must normally obey the following rules:
+
+At least one of the types in the head of
+an instance declaration must not be a type variable.
+For example, these are OK:
+
+ instance C Int a where ...
- f :: (%ns :: NameSupply) => Env -> Expr -> Expr
- f env (Lam x e) = Lam x' (f env e)
- where
- x' = newName %ns
- env' = extend env x x'
- ...more equations for f...
+ instance D (Int, Int) where ...
+
+ instance E [[a]] where ...
-Notice that the implicit parameter %ns is consumed
-
- once by the call to newName
- once by the recursive call to f
-
-
-
-So the translation done by the type checker makes
-the parameter explicit:
+but this is not:
- f :: NameSupply -> Env -> Expr -> Expr
- f ns env (Lam x e) = Lam x' (f ns1 env e)
- where
- (ns1,ns2) = splitNS ns
- x' = newName ns2
- env = extend env x x'
+ instance F a where ...
-Notice the call to 'split' introduced by the type checker.
-How did it know to use 'splitNS'? Because what it really did
-was to introduce a call to the overloaded function 'split',
-defined by the class Splittable:
+Note that instance heads may contain repeated type variables.
+For example, this is OK:
- class Splittable a where
- split :: a -> (a,a)
+ instance Stateful (ST s) (MutVar s) where ...
-The instance for Splittable NameSupply tells GHC how to implement
-split for name supplies. But we can simply write
+
+
+
+
+
+All of the types in the context of
+an instance declaration must be type variables.
+Thus
- g x = (x, %ns, %ns)
+instance C a b => Eq (a,b) where ...
-and GHC will infer
+is OK, but
- g :: (Splittable a, %ns :: a) => b -> (b,a,a)
+instance C Int b => Foo b where ...
-The Splittable class is built into GHC. It's exported by module
-GHC.Exts.
+is not OK.
-
-Other points:
-
- '?x' and '%x'
-are entirely distinct implicit parameters: you
- can use them together and they won't intefere with each other.
-
- You can bind linear implicit parameters in 'with' clauses.
-
-You cannot have implicit parameters (whether linear or not)
- in the context of a class or instance declaration.
-
-
-
-Warnings
-
-
-The monomorphism restriction is even more important than usual.
-Consider the example above:
+
+These restrictions ensure that
+context reduction terminates: each reduction step removes one type
+constructor. For example, the following would make the type checker
+loop if it wasn't excluded:
- f :: (%ns :: NameSupply) => Env -> Expr -> Expr
- f env (Lam x e) = Lam x' (f env e)
- where
- x' = newName %ns
- env' = extend env x x'
+ instance C a => C a where ...
-If we replaced the two occurrences of x' by (newName %ns), which is
-usually a harmless thing to do, we get:
+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:
+
+
- f :: (%ns :: NameSupply) => Env -> Expr -> Expr
- f env (Lam x e) = Lam (newName %ns) (f env e)
- where
- env' = extend env x (newName %ns)
+ instance C a where
+ op = ... -- Default
-But now the name supply is consumed in three places
-(the two calls to newName,and the recursive call to f), so
-the result is utterly different. Urk! We don't even have
-the beta rule.
-
-
-Well, this is an experimental change. With implicit
-parameters we have already lost beta reduction anyway, and
-(as John Launchbury puts it) we can't sensibly reason about
-Haskell programs without knowing their typing.
-
-
-Recursive functions
-Linear implicit parameters can be particularly tricky when you have a recursive function
-Consider
+Second, sometimes you might want to use the following to get the
+effect of a "class synonym":
+
+
- foo :: %x::T => Int -> [Int]
- foo 0 = []
- foo n = %x : foo (n-1)
+ class (C1 a, C2 a, C3 a) => C a where { }
+
+ instance (C1 a, C2 a, C3 a) => C a where { }
-where T is some type in class Splittable.
-
-Do you get a list of all the same T's or all different T's
-(assuming that split gives two distinct T's back)?
-
-If you supply the type signature, taking advantage of polymorphic
-recursion, you get what you'd probably expect. Here's the
-translated term, where the implicit param is made explicit:
+
+
+This allows you to write shorter signatures:
+
+
- foo x 0 = []
- foo x n = let (x1,x2) = split x
- in x1 : foo x2 (n-1)
+ f :: C a => ...
-But if you don't supply a type signature, GHC uses the Hindley
-Milner trick of using a single monomorphic instance of the function
-for the recursive calls. That is what makes Hindley Milner type inference
-work. So the translation becomes
+
+
+instead of
+
+
- foo x = let
- foom 0 = []
- foom n = x : foom (n-1)
- in
- foom
+ f :: (C1 a, C2 a, C3 a) => ...
-Result: 'x' is not split, and you get a list of identical T's. So the
-semantics of the program depends on whether or not foo has a type signature.
-Yikes!
-
-You may say that this is a good reason to dislike linear implicit parameters
-and you'd be right. That is why they are an experimental feature.
+
+
+Voluminous correspondence on the Haskell mailing list has convinced me
+that it's worth experimenting with more liberal rules. If you use
+the experimental flag
+-fallow-undecidable-instances
+option, you can use arbitrary
+types in both an instance context and instance head. Termination is ensured by having a
+fixed-depth recursion stack. If you exceed the stack depth you get a
+sort of backtrace, and the opportunity to increase the stack depth
+with N.
+
+
+I'm on the lookout for a less brutal solution: a simple rule that preserves decidability while
+allowing these idioms interesting idioms.
-
-
-Functional dependencies
-
+
- 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,
-.
-
+
+Implicit parameters
-
-There should be more documentation, but there isn't (yet). Yell if you need it.
+ 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.
-
+(Most of the following, stil rather incomplete, documentation is
+due to Jeff Lewis.)
-
-Arbitrary-rank polymorphism
-
+Implicit parameter support is enabled with the option
+.
-Haskell type signatures are implicitly quantified. The new keyword forall
-allows us to say exactly what this means. For example:
+A variable is called dynamically bound when it is bound by the calling
+context of a function and statically bound when bound by the callee's
+context. In Haskell, all variables are statically bound. Dynamic
+binding of variables is a notion that goes back to Lisp, but was later
+discarded in more modern incarnations, such as Scheme. Dynamic binding
+can be very confusing in an untyped language, and unfortunately, typed
+languages, in particular Hindley-Milner typed languages like Haskell,
+only support static scoping of variables.
+However, by a simple extension to the type class system of Haskell, we
+can support dynamic binding. Basically, we express the use of a
+dynamically bound variable as a constraint on the type. These
+constraints lead to types of the form (?x::t') => t, which says "this
+function uses a dynamically-bound variable ?x
+of type t'". For
+example, the following expresses the type of a sort function,
+implicitly parameterized by a comparison function named cmp.
- g :: b -> b
-
-means this:
-
- g :: forall b. (b -> b)
+ sort :: (?cmp :: a -> a -> Bool) => [a] -> [a]
-The two are treated identically.
+The dynamic binding constraints are just a new form of predicate in the type class system.
-
-However, GHC's type system supports arbitrary-rank
-explicit universal quantification in
-types.
-For example, all the following types are legal:
+An implicit parameter occurs in an expression using the special form ?x,
+where x is
+any valid identifier (e.g. ord ?x is a valid expression).
+Use of this construct also introduces a new
+dynamic-binding constraint in the type of the expression.
+For example, the following definition
+shows how we can define an implicitly parameterized sort function in
+terms of an explicitly parameterized sortBy function:
- f1 :: forall a b. a -> b -> a
- g1 :: forall a b. (Ord a, Eq b) => a -> b -> a
-
- f2 :: (forall a. a->a) -> Int -> Int
- g2 :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int
+ sortBy :: (a -> a -> Bool) -> [a] -> [a]
- f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool
+ sort :: (?cmp :: a -> a -> Bool) => [a] -> [a]
+ sort = sortBy ?cmp
-Here, f1 and g1 are rank-1 types, and
-can be written in standard Haskell (e.g. f1 :: a->b->a).
-The forall makes explicit the universal quantification that
-is implicitly added by Haskell.
-
-
-The functions f2 and g2 have rank-2 types;
-the forall is on the left of a function arrrow. As g2
-shows, the polymorphic type on the left of the function arrow can be overloaded.
-
-
-The functions f3 and g3 have rank-3 types;
-they have rank-2 types on the left of a function arrow.
+
+
+Implicit-parameter type constraints
-GHC allows types of arbitrary rank; you can nest foralls
-arbitrarily deep in function arrows. (GHC used to be restricted to rank 2, but
-that restriction has now been lifted.)
-In particular, a forall-type (also called a "type scheme"),
-including an operational type class context, is legal:
-
- On the left of a function arrow
- On the right of a function arrow (see )
- As the argument of a constructor, or type of a field, in a data type declaration. For
-example, any of the f1,f2,f3,g1,g2,g3 above would be valid
-field type signatures.
- As the type of an implicit parameter
- In a pattern type signature (see )
-
-There is one place you cannot put a forall:
-you cannot instantiate a type variable with a forall-type. So you cannot
-make a forall-type the argument of a type constructor. So these types are illegal:
+Dynamic binding constraints behave just like other type class
+constraints in that they are automatically propagated. Thus, when a
+function is used, its implicit parameters are inherited by the
+function that called it. For example, our sort function might be used
+to pick out the least value in a list:
- x1 :: [forall a. a->a]
- x2 :: (forall a. a->a, Int)
- x3 :: Maybe (forall a. a->a)
+ least :: (?cmp :: a -> a -> Bool) => [a] -> a
+ least xs = fst (sort xs)
-Of course forall becomes a keyword; you can't use forall as
-a type variable any more!
+Without lifting a finger, the ?cmp parameter is
+propagated to become a parameter of least as well. With explicit
+parameters, the default is that parameters must always be explicit
+propagated. With implicit parameters, the default is to always
+propagate them.
-
-
-
-Examples
-
-
-In a data or newtype declaration one can quantify
-the types of the constructor arguments. Here are several examples:
+An implicit-parameter type constraint differs from other type class constraints in the
+following way: All uses of a particular implicit parameter must have
+the same type. This means that the type of (?x, ?x)
+is (?x::a) => (a,a), and not
+(?x::a, ?x::b) => (a, b), as would be the case for type
+class constraints.
+ You can't have an implicit parameter in the context of a class or instance
+declaration. For example, both these declarations are illegal:
+
+ class (?x::Int) => C a where ...
+ instance (?x::a) => Foo [a] where ...
+
+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.
-
+Implicit-parameter constraints do not cause ambiguity. For example, consider:
-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
- }
+ f :: (?x :: [a]) => Int -> Int
+ f n = n + length ?x
-newtype Swizzle = MkSwizzle (Ord a => [a] -> [a])
+ g :: (Read a, Show a) => String -> String
+ g s = show (read s)
-
+Here, g has an ambiguous type, and is rejected, but f
+is fine. The binding for ?x at f's call site is
+quite unambiguous, and fixes the type a.
+
-
-The constructors have rank-2 types:
-
+
+Implicit-parameter bindings
-
+An implicit parameter is bound using the standard
+let or where binding forms.
+For example, we define the min function by binding
+cmp.
-T1 :: forall a. (forall b. b -> b -> b) -> a -> T a
-MkMonad :: forall m. (forall a. a -> m a)
- -> (forall a b. m a -> (a -> m b) -> m b)
- -> MonadT m
-MkSwizzle :: (Ord a => [a] -> [a]) -> Swizzle
+ min :: [a] -> a
+ min = let ?cmp = (<=) in least
-
-
-
-
-Notice that you don't need to use a forall if there's an
-explicit context. For example in the first argument of the
-constructor MkSwizzle, an implicit "forall a." is
-prefixed to the argument type. The implicit forall
-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:
+A group of implicit-parameter bindings may occur anywhere a normal group of Haskell
+bindings can occur, except at top level. That is, they can occur in a let
+(including in a list comprehension, or do-notation, or pattern guards),
+or a where clause.
+Note the following points:
+
+
+An implicit-parameter binding group must be a
+collection of simple bindings to implicit-style variables (no
+function-style bindings, and no type signatures); these bindings are
+neither polymorphic or recursive.
+
+
+You may not mix implicit-parameter bindings with ordinary bindings in a
+single let
+expression; use two nested lets instead.
+(In the case of where you are stuck, since you can't nest where clauses.)
+
+
+You may put multiple implicit-parameter bindings in a
+single binding group; but they are not treated
+as a mutually recursive group (as ordinary let bindings are).
+Instead they are treated as a non-recursive group, simultaneously binding all the implicit
+parameter. The bindings are not nested, and may be re-ordered without changing
+the meaning of the program.
+For example, consider:
- data T a = MkT (Either a b) (b -> b)
+ f t = let { ?x = t; ?y = ?x+(1::Int) } in ?x + ?y
-
-it's just as if you had written this:
-
+The use of ?x in the binding for ?y does not "see"
+the binding for ?x, so the type of f is
- data T a = MkT (forall b. Either a b) (forall b. b -> b)
+ f :: (?x::Int) => Int -> Int
-
-That is, since the type variable b isn't in scope, it's
-implicitly universally quantified. (Arguably, it would be better
-to require explicit quantification on constructor arguments
-where that is what is wanted. Feedback welcomed.)
-
-
-
-You construct values of types T1, MonadT, Swizzle by applying
-the constructor to suitable values, just as usual. For example,
+
+
-
-
-
- a1 :: T Int
- a1 = T1 (\xy->x) 3
-
- a2, a3 :: Swizzle
- a2 = MkSwizzle sort
- a3 = MkSwizzle reverse
-
- a4 :: MonadT Maybe
- a4 = let r x = Just x
- b m k = case m of
- Just y -> k y
- Nothing -> Nothing
- in
- MkMonad r b
-
- mkTs :: (forall b. b -> b -> b) -> a -> [T a]
- mkTs f x y = [T1 f x, T1 f y]
-
-
-
+
+
+
+Linear implicit parameters
-The type of the argument can, as usual, be more general than the type
-required, as (MkSwizzle reverse) shows. (reverse
-does not need the Ord constraint.)
+Linear implicit parameters are an idea developed by Koen Claessen,
+Mark Shields, and Simon PJ. They address the long-standing
+problem that monads seem over-kill for certain sorts of problem, notably:
+
+ distributing a supply of unique names
+ distributing a suppply of random numbers
+ distributing an oracle (as in QuickCheck)
+
-When you use pattern matching, the bound variables may now have
-polymorphic types. For example:
+Linear implicit parameters are just like ordinary implicit parameters,
+except that they are "linear" -- that is, they cannot be copied, and
+must be explicitly "split" instead. Linear implicit parameters are
+written '%x' instead of '?x'.
+(The '/' in the '%' suggests the split!)
-
-
+For example:
- f :: T a -> a -> (a, Char)
- f (T1 w k) x = (w k x, w '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)
-
+ import GHC.Exts( Splittable )
-
+ data NameSupply = ...
+
+ splitNS :: NameSupply -> (NameSupply, NameSupply)
+ newName :: NameSupply -> Name
-
-In the function h we use the record selectors return
-and bind to extract the polymorphic bind and return functions
-from the MonadT data structure, rather than using pattern
-matching.
-
-
+ instance Splittable NameSupply where
+ split = splitNS
-
-Type inference
-
-In general, type inference for arbitrary-rank types is undecideable.
-GHC uses an algorithm proposed by Odersky and Laufer ("Putting type annotations to work", POPL'96)
-to get a decidable algorithm by requiring some help from the programmer.
-We do not yet have a formal specification of "some help" but the rule is this:
-
-
-For a lambda-bound or case-bound variable, x, either the programmer
-provides an explicit polymorphic type for x, or GHC's type inference will assume
-that x's type has no foralls in it.
+ f :: (%ns :: NameSupply) => Env -> Expr -> Expr
+ f env (Lam x e) = Lam x' (f env e)
+ where
+ x' = newName %ns
+ env' = extend env x x'
+ ...more equations for f...
+
+Notice that the implicit parameter %ns is consumed
+
+ once by the call to newName
+ once by the recursive call to f
+
-What does it mean to "provide" an explicit type for x? You can do that by
-giving a type signature for x directly, using a pattern type signature
-(), thus:
+So the translation done by the type checker makes
+the parameter explicit:
- \ f :: (forall a. a->a) -> (f True, f 'c')
+ f :: NameSupply -> Env -> Expr -> Expr
+ f ns env (Lam x e) = Lam x' (f ns1 env e)
+ where
+ (ns1,ns2) = splitNS ns
+ x' = newName ns2
+ env = extend env x x'
-Alternatively, you can give a type signature to the enclosing
-context, which GHC can "push down" to find the type for the variable:
+Notice the call to 'split' introduced by the type checker.
+How did it know to use 'splitNS'? Because what it really did
+was to introduce a call to the overloaded function 'split',
+defined by the class Splittable:
- (\ f -> (f True, f 'c')) :: (forall a. a->a) -> (Bool,Char)
+ class Splittable a where
+ split :: a -> (a,a)
-Here the type signature on the expression can be pushed inwards
-to give a type signature for f. Similarly, and more commonly,
-one can give a type signature for the function itself:
+The instance for Splittable NameSupply tells GHC how to implement
+split for name supplies. But we can simply write
- h :: (forall a. a->a) -> (Bool,Char)
- h f = (f True, f 'c')
+ g x = (x, %ns, %ns)
-You don't need to give a type signature if the lambda bound variable
-is a constructor argument. Here is an example we saw earlier:
+and GHC will infer
- f :: T a -> a -> (a, Char)
- f (T1 w k) x = (w k x, w 'c' 'd')
+ g :: (Splittable a, %ns :: a) => b -> (b,a,a)
-Here we do not need to give a type signature to w, because
-it is an argument of constructor T1 and that tells GHC all
-it needs to know.
+The Splittable class is built into GHC. It's exported by module
+GHC.Exts.
+
+Other points:
+
+ '?x' and '%x'
+are entirely distinct implicit parameters: you
+ can use them together and they won't intefere with each other.
+
-
+ You can bind linear implicit parameters in 'with' clauses.
+You cannot have implicit parameters (whether linear or not)
+ in the context of a class or instance declaration.
+
+
-
-Implicit quantification
+Warnings
-GHC performs implicit quantification as follows. At the top level (only) of
-user-written types, if and only if there is no explicit forall,
-GHC finds all the type variables mentioned in the type that are not already
-in scope, and universally quantifies them. For example, the following pairs are
-equivalent:
+The monomorphism restriction is even more important than usual.
+Consider the example above:
- f :: a -> a
- f :: forall a. a -> a
-
- g (x::a) = let
- h :: a -> b -> b
- h x y = y
- in ...
- g (x::a) = let
- h :: forall b. a -> b -> b
- h x y = y
- in ...
+ f :: (%ns :: NameSupply) => Env -> Expr -> Expr
+ f env (Lam x e) = Lam x' (f env e)
+ where
+ x' = newName %ns
+ env' = extend env x x'
+
+If we replaced the two occurrences of x' by (newName %ns), which is
+usually a harmless thing to do, we get:
+
+ f :: (%ns :: NameSupply) => Env -> Expr -> Expr
+ f env (Lam x e) = Lam (newName %ns) (f env e)
+ where
+ env' = extend env x (newName %ns)
+But now the name supply is consumed in three places
+(the two calls to newName,and the recursive call to f), so
+the result is utterly different. Urk! We don't even have
+the beta rule.
-Notice that GHC does not find the innermost possible quantification
-point. For example:
-
- f :: (a -> a) -> Int
- -- MEANS
- f :: forall a. (a -> a) -> Int
- -- NOT
- f :: (forall a. a -> a) -> Int
+Well, this is an experimental change. With implicit
+parameters we have already lost beta reduction anyway, and
+(as John Launchbury puts it) we can't sensibly reason about
+Haskell programs without knowing their typing.
+
+
- g :: (Ord a => a -> a) -> Int
- -- MEANS the illegal type
- g :: forall a. (Ord a => a -> a) -> Int
- -- NOT
- g :: (forall a. Ord a => a -> a) -> Int
+Recursive functions
+Linear implicit parameters can be particularly tricky when you have a recursive function
+Consider
+
+ foo :: %x::T => Int -> [Int]
+ foo 0 = []
+ foo n = %x : foo (n-1)
+
+where T is some type in class Splittable.
+
+Do you get a list of all the same T's or all different T's
+(assuming that split gives two distinct T's back)?
+
+If you supply the type signature, taking advantage of polymorphic
+recursion, you get what you'd probably expect. Here's the
+translated term, where the implicit param is made explicit:
+
+ foo x 0 = []
+ foo x n = let (x1,x2) = split x
+ in x1 : foo x2 (n-1)
-The latter produces an illegal type, which you might think is silly,
-but at least the rule is simple. If you want the latter type, you
-can write your for-alls explicitly. Indeed, doing so is strongly advised
-for rank-2 types.
+But if you don't supply a type signature, GHC uses the Hindley
+Milner trick of using a single monomorphic instance of the function
+for the recursive calls. That is what makes Hindley Milner type inference
+work. So the translation becomes
+
+ foo x = let
+ foom 0 = []
+ foom n = x : foom (n-1)
+ in
+ foom
+
+Result: 'x' is not split, and you get a list of identical T's. So the
+semantics of the program depends on whether or not foo has a type signature.
+Yikes!
+
+You may say that this is a good reason to dislike linear implicit parameters
+and you'd be right. That is why they are an experimental feature.
+
-
-Liberalised type synonyms
+
+Functional dependencies
+ 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,
+.
+
-Type synonmys are like macros at the type level, and
-GHC does validity checking on types only after expanding type synonyms.
-That means that GHC can be very much more liberal about type synonyms than Haskell 98:
-
-You can write a forall (including overloading)
-in a type synonym, thus:
+Functional dependencies are introduced by a vertical bar in the syntax of a
+class declaration; e.g.
- type Discard a = forall b. Show b => a -> b -> (a, String)
-
- f :: Discard a
- f x y = (x, show y)
+ class (Monad m) => MonadState s m | m -> s where ...
- g :: Discard Int -> (Int,Bool) -- A rank-2 type
- g f = f Int True
+ class Foo a b c | a b -> c where ...
+There should be more documentation, but there isn't (yet). Yell if you need it.
-
-
-
-You can write an unboxed tuple in a type synonym:
-
- type Pr = (# Int, Int #)
-
- h :: Int -> Pr
- h x = (# x, x #)
-
-
+
-
-You can apply a type synonym to a forall type:
-
- type Foo a = a -> a -> Bool
-
- f :: Foo (forall b. b->b)
-
-After expanding the synonym, f has the legal (in GHC) type:
-
- f :: (forall b. b->b) -> (forall b. b->b) -> Bool
-
-
-
-You can apply a type synonym to a partially applied type synonym:
-
- type Generic i o = forall x. i x -> o x
- type Id x = x
-
- foo :: Generic Id []
-
-After epxanding the synonym, foo has the legal (in GHC) type:
-
- foo :: forall x. x -> [x]
-
-
-
-
+
+Explicitly-kinded quantification
-GHC currently does kind checking before expanding synonyms (though even that
-could be changed.)
+Haskell infers the kind of each type variable. Sometimes it is nice to be able
+to give the kind explicitly as (machine-checked) documentation,
+just as it is nice to give a type signature for a function. On some occasions,
+it is essential to do so. For example, in his paper "Restricted Data Types in Haskell" (Haskell Workshop 1999)
+John Hughes had to define the data type:
+
+ data Set cxt a = Set [a]
+ | Unused (cxt a -> ())
+
+The only use for the Unused constructor was to force the correct
+kind for the type variable cxt.
-After expanding type synonyms, GHC does validity checking on types, looking for
-the following mal-formedness which isn't detected simply by kind checking:
+GHC now instead allows you to specify the kind of a type variable directly, wherever
+a type variable is explicitly bound. Namely:
-
-Type constructor applied to a type involving for-alls.
-
-
-Unboxed tuple on left of an arrow.
-
-
-Partially-applied type synonym.
-
+data declarations:
+
+ data Set (cxt :: * -> *) a = Set [a]
+
+type declarations:
+
+ type T (f :: * -> *) = f Int
+
+class declarations:
+
+ class (Eq a) => C (f :: * -> *) a where ...
+
+forall's in type signatures:
+
+ f :: forall (cxt :: * -> *). Set cxt Int
+
-So, for example,
-this will be rejected:
-
- type Pr = (# Int, Int #)
+
- h :: Pr -> Int
- h x = ...
-
-because GHC does not allow unboxed tuples on the left of a function arrow.
+
+The parentheses are required. Some of the spaces are required too, to
+separate the lexemes. If you write (f::*->*) you
+will get a parse error, because "::*->*" is a
+single lexeme in Haskell.
-
-
-For-all hoisting
-It is often convenient to use generalised type synonyms at the right hand
-end of an arrow, thus:
-
- type Discard a = forall b. a -> b -> a
+As part of the same extension, you can put kind annotations in types
+as well. Thus:
+
+ f :: (Int :: *) -> Int
+ g :: forall a. a -> (a :: *)
+
+The syntax is
+
+ atype ::= '(' ctype '::' kind ')
+
+The parentheses are required.
+
+
- g :: Int -> Discard Int
- g x y z = x+y
-
-Simply expanding the type synonym would give
-
- g :: Int -> (forall b. Int -> b -> Int)
-
-but GHC "hoists" the forall to give the isomorphic type
-
- g :: forall b. Int -> Int -> b -> Int
-
-In general, the rule is this: to determine the type specified by any explicit
-user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly
-performs the transformation:
-
- type1 -> forall a1..an. context2 => type2
-==>
- forall a1..an. context2 => type1 -> type2
-
-(In fact, GHC tries to retain as much synonym information as possible for use in
-error messages, but that is a usability issue.) This rule applies, of course, whether
-or not the forall comes from a synonym. For example, here is another
-valid way to write g's type signature:
-
- g :: Int -> Int -> forall b. b -> Int
-
+
+
+Arbitrary-rank polymorphism
+
+
+
+Haskell type signatures are implicitly quantified. The new keyword forall
+allows us to say exactly what this means. For example:
-When doing this hoisting operation, GHC eliminates duplicate constraints. For
-example:
- type Foo a = (?x::Int) => Bool -> a
- g :: Foo (Foo Int)
+ g :: b -> b
-means
+means this:
- g :: (?x::Int) => Bool -> Bool -> Int
+ g :: forall b. (b -> b)
+The two are treated identically.
-
+
+However, GHC's type system supports arbitrary-rank
+explicit universal quantification in
+types.
+For example, all the following types are legal:
+
+ f1 :: forall a b. a -> b -> a
+ g1 :: forall a b. (Ord a, Eq b) => a -> b -> a
-
-Existentially quantified data constructors
-
+ f2 :: (forall a. a->a) -> Int -> Int
+ g2 :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int
+ f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool
+
+Here, f1 and g1 are rank-1 types, and
+can be written in standard Haskell (e.g. f1 :: a->b->a).
+The forall makes explicit the universal quantification that
+is implicitly added by Haskell.
+
-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 hbc Haskell compiler for several years, and
-proved very useful. Here's the idea. Consider the declaration:
+The functions f2 and g2 have rank-2 types;
+the forall is on the left of a function arrrow. As g2
+shows, the polymorphic type on the left of the function arrow can be overloaded.
-
-
+The function f3 has a rank-3 type;
+it has rank-2 types on the left of a function arrow.
+
+
+GHC allows types of arbitrary rank; you can nest foralls
+arbitrarily deep in function arrows. (GHC used to be restricted to rank 2, but
+that restriction has now been lifted.)
+In particular, a forall-type (also called a "type scheme"),
+including an operational type class context, is legal:
+
+ On the left of a function arrow
+ On the right of a function arrow (see )
+ As the argument of a constructor, or type of a field, in a data type declaration. For
+example, any of the f1,f2,f3,g1,g2 above would be valid
+field type signatures.
+ As the type of an implicit parameter
+ In a pattern type signature (see )
+
+There is one place you cannot put a forall:
+you cannot instantiate a type variable with a forall-type. So you cannot
+make a forall-type the argument of a type constructor. So these types are illegal:
- data Foo = forall a. MkFoo a (a -> Bool)
- | Nil
+ x1 :: [forall a. a->a]
+ x2 :: (forall a. a->a, Int)
+ x3 :: Maybe (forall a. a->a)
-
-
-
-
-The data type Foo has two constructors with types:
+Of course forall becomes a keyword; you can't use forall as
+a type variable any more!
-
-
-
- MkFoo :: forall a. a -> (a -> Bool) -> Foo
- Nil :: Foo
-
-
+
+Examples
+
-Notice that the type variable a in the type of MkFoo
-does not appear in the data type itself, which is plain Foo.
-For example, the following expression is fine:
+In a data or newtype declaration one can quantify
+the types of the constructor arguments. Here are several examples:
- [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo]
-
+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])
+
-
-Here, (MkFoo 3 even) packages an integer with a function
-even that maps an integer to Bool; and MkFoo 'c'
-isUpper packages a character with a compatible function. These
-two things are each of type Foo and can be put in a list.
-What can we do with a value of type Foo?. In particular,
-what happens when we pattern-match on MkFoo?
+The constructors have rank-2 types:
- f (MkFoo val fn) = ???
+T1 :: forall a. (forall b. b -> b -> b) -> a -> T a
+MkMonad :: forall m. (forall a. a -> m a)
+ -> (forall a b. m a -> (a -> m b) -> m b)
+ -> MonadT m
+MkSwizzle :: (Ord a => [a] -> [a]) -> Swizzle
-Since all we know about val and fn is that they
-are compatible, the only (useful) thing we can do with them is to
-apply fn to val to get a boolean. For example:
+Notice that you don't need to use a forall if there's an
+explicit context. For example in the first argument of the
+constructor MkSwizzle, an implicit "forall a." is
+prefixed to the argument type. The implicit forall
+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:
- f :: Foo -> Bool
- f (MkFoo val fn) = fn val
+ data T a = MkT (Either a b) (b -> b)
-
-
-
-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.
-
-
-
-Why existential?
-
-
-
-What has this to do with existential quantification?
-Simply that MkFoo has the (nearly) isomorphic type
-
-
-
+it's just as if you had written this:
- MkFoo :: (exists a . (a, a -> Bool)) -> Foo
+ data T a = MkT (forall b. Either a b) (forall b. b -> b)
+That is, since the type variable b isn't in scope, it's
+implicitly universally quantified. (Arguably, it would be better
+to require explicit quantification on constructor arguments
+where that is what is wanted. Feedback welcomed.)
-But Haskell programmers can safely think of the ordinary
-universally quantified type given above, thereby avoiding
-adding a new existential quantification construct.
-
-
-
-
-
-Type classes
-
-
-An easy extension (implemented in hbc) is to allow
-arbitrary contexts before the constructor. For example:
+You construct values of types T1, MonadT, Swizzle by applying
+the constructor to suitable values, just as usual. For example,
-data Baz = forall a. Eq a => Baz1 a a
- | forall b. Show b => Baz2 b (b -> b)
-
+ a1 :: T Int
+ a1 = T1 (\xy->x) 3
+
+ a2, a3 :: Swizzle
+ a2 = MkSwizzle sort
+ a3 = MkSwizzle reverse
+
+ a4 :: MonadT Maybe
+ a4 = let r x = Just x
+ b m k = case m of
+ Just y -> k y
+ Nothing -> Nothing
+ in
+ MkMonad r b
-
+ mkTs :: (forall b. b -> b -> b) -> a -> [T a]
+ mkTs f x y = [T1 f x, T1 f y]
+
-
-The two constructors have the types you'd expect:
-
-
-Baz1 :: forall a. Eq a => a -> a -> Baz
-Baz2 :: forall b. Show b => b -> (b -> b) -> Baz
-
-
+The type of the argument can, as usual, be more general than the type
+required, as (MkSwizzle reverse) shows. (reverse
+does not need the Ord constraint.)
-But when pattern matching on Baz1 the matched values can be compared
-for equality, and when pattern matching on Baz2 the first matched
-value can be converted to a string (as well as applying the function to it).
-So this program is legal:
+When you use pattern matching, the bound variables may now have
+polymorphic types. For example:
- f :: Baz -> String
- f (Baz1 p q) | p == q = "Yes"
- | otherwise = "No"
- f (Baz2 v fn) = show (fn v)
-
+ f :: T a -> a -> (a, Char)
+ f (T1 w k) x = (w k x, w '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)
+
-
-Operationally, in a dictionary-passing implementation, the
-constructors Baz1 and Baz2 must store the
-dictionaries for Eq and Show respectively, and
-extract it on pattern matching.
-Notice the way that the syntax fits smoothly with that used for
-universal quantification earlier.
+In the function h we use the record selectors return
+and bind to extract the polymorphic bind and return functions
+from the MonadT data structure, rather than using pattern
+matching.
-
-Restrictions
+Type inference
-There are several restrictions on the ways in which existentially-quantified
-constructors can be use.
+In general, type inference for arbitrary-rank types is undecideable.
+GHC uses an algorithm proposed by Odersky and Laufer ("Putting type annotations to work", POPL'96)
+to get a decidable algorithm by requiring some help from the programmer.
+We do not yet have a formal specification of "some help" but the rule is this:
-
-
-
-
-
+For a lambda-bound or case-bound variable, x, either the programmer
+provides an explicit polymorphic type for x, or GHC's type inference will assume
+that x's type has no foralls in it.
+
- 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:
-
-
-
-f1 (MkFoo a f) = a
-
-
-
-Here, the type bound by MkFoo "escapes", because a
-is the result of f1. One way to see why this is wrong is to
-ask what type f1 has:
-
-
-
- f1 :: Foo -> a -- Weird!
-
-
-
-What is this "a" in the result type? Clearly we don't mean
-this:
-
-
+What does it mean to "provide" an explicit type for x? You can do that by
+giving a type signature for x directly, using a pattern type signature
+(), thus:
- f1 :: forall a. Foo -> a -- Wrong!
+ \ f :: (forall a. a->a) -> (f True, f 'c')
-
-
-The original program is just plain wrong. Here's another sort of error
-
-
+Alternatively, you can give a type signature to the enclosing
+context, which GHC can "push down" to find the type for the variable:
- f2 (Baz1 a b) (Baz1 p q) = a==q
+ (\ f -> (f True, f 'c')) :: (forall a. a->a) -> (Bool,Char)
-
-
-It's ok to say a==b or p==q, but
-a==q is wrong because it equates the two distinct types arising
-from the two Baz1 constructors.
-
-
-
-
-
-
-
-You can't pattern-match on an existentially quantified
-constructor in a let or where group of
-bindings. So this is illegal:
-
-
+Here the type signature on the expression can be pushed inwards
+to give a type signature for f. Similarly, and more commonly,
+one can give a type signature for the function itself:
- f3 x = a==b where { Baz1 a b = x }
+ h :: (forall a. a->a) -> (Bool,Char)
+ h f = (f True, f 'c')
-
-Instead, use a case expression:
-
+You don't need to give a type signature if the lambda bound variable
+is a constructor argument. Here is an example we saw earlier:
- f3 x = case x of Baz1 a b -> a==b
+ f :: T a -> a -> (a, Char)
+ f (T1 w k) x = (w k x, w 'c' 'd')
+Here we do not need to give a type signature to w, because
+it is an argument of constructor T1 and that tells GHC all
+it needs to know.
+
-In general, you can only pattern-match
-on an existentially-quantified constructor in a case 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.
-
-
-
+
+Implicit quantification
-You can't use existential quantification for newtype
-declarations. So this is illegal:
-
-
+GHC performs implicit quantification as follows. At the top level (only) of
+user-written types, if and only if there is no explicit forall,
+GHC finds all the type variables mentioned in the type that are not already
+in scope, and universally quantifies them. For example, the following pairs are
+equivalent:
- newtype T = forall a. Ord a => MkT a
-
-
-
-Reason: a value of type T must be represented as a pair
-of a dictionary for Ord t and a value of type t.
-That contradicts the idea that newtype should have no
-concrete representation. You can get just the same efficiency and effect
-by using data instead of newtype. If there is no
-overloading involved, then there is more of a case for allowing
-an existentially-quantified newtype, because the data
-because the data version does carry an implementation cost,
-but single-field existentially quantified constructors aren't much
-use. So the simple restriction (no existential stuff on newtype)
-stands, unless there are convincing reasons to change it.
-
+ f :: a -> a
+ f :: forall a. a -> a
+ g (x::a) = let
+ h :: a -> b -> b
+ h x y = y
+ in ...
+ g (x::a) = let
+ h :: forall b. a -> b -> b
+ h x y = y
+ in ...
+
-
-
-
- You can't use deriving to define instances of a
-data type with existentially quantified data constructors.
-
-Reason: in most cases it would not make sense. For example:#
-
+Notice that GHC does not find the innermost possible quantification
+point. For example:
-data T = forall a. MkT [a] deriving( Eq )
-
+ f :: (a -> a) -> Int
+ -- MEANS
+ f :: forall a. (a -> a) -> Int
+ -- NOT
+ f :: (forall a. a -> a) -> Int
-To derive Eq in the standard way we would need to have equality
-between the single component of two MkT constructors:
-
-instance Eq T where
- (MkT a) == (MkT b) = ???
+ g :: (Ord a => a -> a) -> Int
+ -- MEANS the illegal type
+ g :: forall a. (Ord a => a -> a) -> Int
+ -- NOT
+ g :: (forall a. Ord a => a -> a) -> Int
-
-But a and b have distinct types, and so can't be compared.
-It's just about possible to imagine examples in which the derived instance
-would make sense, but it seems altogether simpler simply to prohibit such
-declarations. Define your own instances!
+The latter produces an illegal type, which you might think is silly,
+but at least the rule is simple. If you want the latter type, you
+can write your for-alls explicitly. Indeed, doing so is strongly advised
+for rank-2 types.
-
-
-
+
+
-
-
-
Scoped type variables
@@ -2978,6 +3017,25 @@ Result type signatures are not yet implemented in Hugs.
+
+Deriving clause for classes Typeable and Data
+
+
+Haskell 98 allows the programmer to add "deriving( Eq, Ord )" to a data type
+declaration, to generate a standard instance declaration for classes specified in the deriving clause.
+In Haskell 98, the only classes that may appear in the deriving clause are the standard
+classes Eq, Ord,
+Enum, Ix, Bounded, Read, and Show.
+
+
+GHC extends this list with two more classes that may be automatically derived
+(provided the flag is specified):
+Typeable, and Data. These classes are defined in the library
+modules Data.Dynamic and Data.Generics respectively, and the
+appropriate class must be in scope before it can be mentioned in the deriving clause.
+
+
+
Generalised derived instances for newtypes
@@ -3110,17 +3168,24 @@ where
S is a type constructor,
- t1...tk are types,
+ The t1...tk are types,
- vk+1...vn are type variables which do not occur in any of
+ The vk+1...vn are type variables which do not occur in any of
the ti, and
- the ci are partial applications of
+ The ci are partial applications of
classes of the form C t1'...tj', where the arity of C
is exactly j+1. That is, C lacks exactly one type argument.
+
+ None of the ci is Read, Show,
+ Typeable, or Data. These classes
+ should not "look through" the type or its constructor. You can still
+ derive these classes for a newtype, but it happens in the usual way, not
+ via this new mechanism.
+
Then, for each ci, the derived instance
declaration is:
@@ -3175,11 +3240,19 @@ instances is most interesting.
Template Haskell
-Template Haskell allows you to do compile-time meta-programming in Haskell. The background
-the main technical innovations are discussed in "Template Haskell allows you to do compile-time meta-programming in Haskell. There is a "home page" for
+Template Haskell at
+http://www.haskell.org/th/, while
+the background to
+the main technical innovations is discussed in "
-Template Meta-programming for Haskell", in
-Proc Haskell Workshop 2002.
+Template Meta-programming for Haskell" (Proc Haskell Workshop 2002).
+The details of the Template Haskell design are still in flux. Make sure you
+consult the online library reference material
+(search for the type ExpQ).
+[Temporary: many changes to the original design are described in
+ "http://research.microsoft.com/~simonpj/tmp/notes2.ps".
+Not all of these changes are in GHC 6.2.]
The first example from that paper is set out below as a worked example to help get you started.
@@ -3190,10 +3263,16 @@ The documentation here describes the realisation in GHC. (It's rather sketchy j
Tim Sheard is going to expand it.)
- Syntax
-
- Template Haskell has the following new syntactic constructions. You need to use the flag
- -fglasgow-exts to switch these syntactic extensions on.
+
+ Syntax
+
+ Template Haskell has the following new syntactic
+ constructions. You need to use the flag
+
+ to switch these syntactic extensions on
+ ( is currently implied by
+ , but you are encouraged to
+ specify it explicitly).
@@ -3240,7 +3319,6 @@ Tim Sheard is going to expand it.)
- Using Template Haskell
@@ -3251,97 +3329,569 @@ Tim Sheard is going to expand it.)
Language.Haskell.THSyntax.
-
- You can only run a function at compile time if it is imported from another module. That is,
- you can't define a function in a module, and call it from within a splice in the same module.
- (It would make sense to do so, but it's hard to implement.)
-
+
+ You can only run a function at compile time if it is imported from another module. That is,
+ you can't define a function in a module, and call it from within a splice in the same module.
+ (It would make sense to do so, but it's hard to implement.)
+
+
+
+ The flag -ddump-splices shows the expansion of all top-level splices as they happen.
+
+
+ If you are building GHC from source, you need at least a stage-2 bootstrap compiler to
+ run Template Haskell. A stage-1 compiler will reject the TH constructs. Reason: TH
+ compiles and runs a program, and then looks at the result. So it's important that
+ the program it compiles produces results whose representations are identical to
+ those of the compiler itself.
+
+
+
+ Template Haskell works in any mode (--make, --interactive,
+ or file-at-a-time). There used to be a restriction to the former two, but that restriction
+ has been lifted.
+
+
+
+ A Template Haskell Worked Example
+To help you get over the confidence barrier, try out this skeletal worked example.
+ First cut and paste the two modules below into "Main.hs" and "Printf.hs":
+
+
+
+{- Main.hs -}
+module Main where
+
+-- Import our template "pr"
+import Printf ( pr )
+
+-- The splice operator $ takes the Haskell source code
+-- generated at compile time by "pr" and splices it into
+-- the argument of "putStrLn".
+main = putStrLn ( $(pr "Hello") )
+
+
+{- Printf.hs -}
+module Printf where
+
+-- Skeletal printf from the paper.
+-- It needs to be in a separate module to the one where
+-- you intend to use it.
+
+-- Import some Template Haskell syntax
+import Language.Haskell.THSyntax
+
+-- Describe a format string
+data Format = D | S | L String
+
+-- Parse a format string. This is left largely to you
+-- as we are here interested in building our first ever
+-- Template Haskell program and not in building printf.
+parse :: String -> [Format]
+parse s = [ L s ]
+
+-- Generate Haskell source code from a parsed representation
+-- of the format string. This code will be spliced into
+-- the module which calls "pr", at compile time.
+gen :: [Format] -> ExpQ
+gen [D] = [| \n -> show n |]
+gen [S] = [| \s -> s |]
+gen [L s] = stringE s
+
+-- Here we generate the Haskell code for the splice
+-- from an input format string.
+pr :: String -> ExpQ
+pr s = gen (parse s)
+
+
+Now run the compiler (here we are a Cygwin prompt on Windows):
+
+
+$ ghc --make -fth main.hs -o main.exe
+
+
+Run "main.exe" and here is your output:
+
+
+$ ./main
+Hello
+
+
+
+
+
+
+
+
+
+Arrow notation
+
+
+Arrows are a generalization of monads introduced by John Hughes.
+For more details, see
+
+
+
+
+“Generalising Monads to Arrows”,
+John Hughes, in Science of Computer Programming 37,
+pp67–111, May 2000.
+
+
+
+
+
+“A New Notation for Arrows”,
+Ross Paterson, in ICFP, Sep 2001.
+
+
+
+
+
+“Arrows and Computation”,
+Ross Paterson, in The Fun of Programming,
+Palgrave, 2003.
+
+
+
+
+and the arrows web page at
+http://www.haskell.org/arrows/.
+With the flag, GHC supports the arrow
+notation described in the second of these papers.
+What follows is a brief introduction to the notation;
+it won't make much sense unless you've read Hughes's paper.
+This notation is translated to ordinary Haskell,
+using combinators from the
+Control.Arrow
+module.
+
+
+The extension adds a new kind of expression for defining arrows,
+of the form proc pat -> cmd,
+where proc is a new keyword.
+The variables of the pattern are bound in the body of the
+proc-expression,
+which is a new sort of thing called a command.
+The syntax of commands is as follows:
+
+cmd ::= exp1 -< exp2
+ | exp1 -<< exp2
+ | do { cstmt1 .. cstmtn ; cmd }
+ | let decls in cmd
+ | if exp then cmd1 else cmd2
+ | case exp of { calts }
+ | cmd1 qop cmd2
+ | (| aexp cmd1 .. cmdn |)
+ | \ pat1 .. patn -> cmd
+ | cmd aexp
+ | ( cmd )
+
+cstmt ::= let decls
+ | pat <- cmd
+ | rec { cstmt1 .. cstmtn }
+ | cmd
+
+Commands produce values, but (like monadic computations)
+may yield more than one value,
+or none, and may do other things as well.
+For the most part, familiarity with monadic notation is a good guide to
+using commands.
+However the values of expressions, even monadic ones,
+are determined by the values of the variables they contain;
+this is not necessarily the case for commands.
+
+
+
+A simple example of the new notation is the expression
+
+proc x -> f -< x+1
+
+We call this a procedure or
+arrow abstraction.
+As with a lambda expression, the variable x
+is a new variable bound within the proc-expression.
+It refers to the input to the arrow.
+In the above example, -< is not an identifier but an
+new reserved symbol used for building commands from an expression of arrow
+type and an expression to be fed as input to that arrow.
+(The weird look will make more sense later.)
+It may be read as analogue of application for arrows.
+The above example is equivalent to the Haskell expression
+
+arr (\ x -> x+1) >>> f
+
+That would make no sense if the expression to the left of
+-< involves the bound variable x.
+More generally, the expression to the left of -<
+may not involve any local variable,
+i.e. a variable bound in the current arrow abstraction.
+For such a situation there is a variant -<<, as in
+
+proc x -> f x -<< x+1
+
+which is equivalent to
+
+arr (\ x -> (f, x+1)) >>> app
+
+so in this case the arrow must belong to the ArrowApply
+class.
+Such an arrow is equivalent to a monad, so if you're using this form
+you may find a monadic formulation more convenient.
+
+
+
+do-notation for commands
+
+
+Another form of command is a form of do-notation.
+For example, you can write
+
+proc x -> do
+ y <- f -< x+1
+ g -< 2*y
+ let z = x+y
+ t <- h -< x*z
+ returnA -< t+z
+
+You can read this much like ordinary do-notation,
+but with commands in place of monadic expressions.
+The first line sends the value of x+1 as an input to
+the arrow f, and matches its output against
+y.
+In the next line, the output is discarded.
+The arrow returnA is defined in the
+Control.Arrow
+module as arr id.
+The above example is treated as an abbreviation for
+
+arr (\ x -> (x, x)) >>>
+ first (arr (\ x -> x+1) >>> f) >>>
+ arr (\ (y, x) -> (y, (x, y))) >>>
+ first (arr (\ y -> 2*y) >>> g) >>>
+ arr snd >>>
+ arr (\ (x, y) -> let z = x+y in ((x, z), z)) >>>
+ first (arr (\ (x, z) -> x*z) >>> h) >>>
+ arr (\ (t, z) -> t+z) >>>
+ returnA
+
+Note that variables not used later in the composition are projected out.
+After simplification using rewrite rules (see )
+defined in the
+Control.Arrow
+module, this reduces to
+
+arr (\ x -> (x+1, x)) >>>
+ first f >>>
+ arr (\ (y, x) -> (2*y, (x, y))) >>>
+ first g >>>
+ arr (\ (_, (x, y)) -> let z = x+y in (x*z, z)) >>>
+ first h >>>
+ arr (\ (t, z) -> t+z)
+
+which is what you might have written by hand.
+With arrow notation, GHC keeps track of all those tuples of variables for you.
+
+
+
+Note that although the above translation suggests that
+let-bound variables like z must be
+monomorphic, the actual translation produces Core,
+so polymorphic variables are allowed.
+
+
+
+It's also possible to have mutually recursive bindings,
+using the new rec keyword, as in the following example:
+
+counter :: ArrowCircuit a => a Bool Int
+counter = proc reset -> do
+ rec output <- returnA -< if reset then 0 else next
+ next <- delay 0 -< output+1
+ returnA -< output
+
+The translation of such forms uses the loop combinator,
+so the arrow concerned must belong to the ArrowLoop class.
+
+
+
+
+
+Conditional commands
+
+
+In the previous example, we used a conditional expression to construct the
+input for an arrow.
+Sometimes we want to conditionally execute different commands, as in
+
+proc (x,y) ->
+ if f x y
+ then g -< x+1
+ else h -< y+2
+
+which is translated to
+
+arr (\ (x,y) -> if f x y then Left x else Right y) >>>
+ (arr (\x -> x+1) >>> f) ||| (arr (\y -> y+2) >>> g)
+
+Since the translation uses |||,
+the arrow concerned must belong to the ArrowChoice class.
+
+
+
+There are also case commands, like
+
+case input of
+ [] -> f -< ()
+ [x] -> g -< x+1
+ x1:x2:xs -> do
+ y <- h -< (x1, x2)
+ ys <- k -< xs
+ returnA -< y:ys
+
+The syntax is the same as for case expressions,
+except that the bodies of the alternatives are commands rather than expressions.
+The translation is similar to that of if commands.
+
+
+
-
- The flag -ddump-splices shows the expansion of all top-level splices as they happen.
-
-
- If you are building GHC from source, you need at least a stage-2 bootstrap compiler to
- run Template Haskell. A stage-1 compiler will reject the TH constructs. Reason: TH
- compiles and runs a program, and then looks at the result. So it's important that
- the program it compiles produces results whose representations are identical to
- those of the compiler itself.
-
-
+
+Defining your own control structures
+
+
+As we're seen, arrow notation provides constructs,
+modelled on those for expressions,
+for sequencing, value recursion and conditionals.
+But suitable combinators,
+which you can define in ordinary Haskell,
+may also be used to build new commands out of existing ones.
+The basic idea is that a command defines an arrow from environments to values.
+These environments assign values to the free local variables of the command.
+Thus combinators that produce arrows from arrows
+may also be used to build commands from commands.
+For example, the ArrowChoice class includes a combinator
+
+ArrowChoice a => (<+>) :: a e c -> a e c -> a e c
+
+so we can use it to build commands:
+
+expr' = proc x ->
+ returnA -< x
+ <+> do
+ symbol Plus -< ()
+ y <- term -< ()
+ expr' -< x + y
+ <+> do
+ symbol Minus -< ()
+ y <- term -< ()
+ expr' -< x - y
+
+This is equivalent to
+
+expr' = (proc x -> returnA -< x)
+ <+> (proc x -> do
+ symbol Plus -< ()
+ y <- term -< ()
+ expr' -< x + y)
+ <+> (proc x -> do
+ symbol Minus -< ()
+ y <- term -< ()
+ expr' -< x - y)
+
+It is essential that this operator be polymorphic in e
+(representing the environment input to the command
+and thence to its subcommands)
+and satisfy the corresponding naturality property
+
+arr k >>> (f <+> g) = (arr k >>> f) <+> (arr k >>> g)
+
+at least for strict k.
+(This should be automatic if you're not using seq.)
+This ensures that environments seen by the subcommands are environments
+of the whole command,
+and also allows the translation to safely trim these environments.
+The operator must also not use any variable defined within the current
+arrow abstraction.
- Template Haskell works in any mode (--make, --interactive,
- or file-at-a-time). There used to be a restriction to the former two, but that restriction
- has been lifted.
+
+
+We could define our own operator
+
+untilA :: ArrowChoice a => a e () -> a e Bool -> a e ()
+untilA body cond = proc x ->
+ if cond x then returnA -< ()
+ else do
+ body -< x
+ untilA body cond -< x
+
+and use it in the same way.
+Of course this infix syntax only makes sense for binary operators;
+there is also a more general syntax involving special brackets:
+
+proc x -> do
+ y <- f -< x+1
+ (|untilA (increment -< x+y) (within 0.5 -< x)|)
+
+
-
- A Template Haskell Worked Example
-To help you get over the confidence barrier, try out this skeletal worked example.
- First cut and paste the two modules below into "Main.hs" and "Printf.hs":
-
-{- Main.hs -}
-module Main where
+
+Primitive constructs
--- Import our template "pr"
-import Printf ( pr )
+
+Some operators will need to pass additional inputs to their subcommands.
+For example, in an arrow type supporting exceptions,
+the operator that attaches an exception handler will wish to pass the
+exception that occurred to the handler.
+Such an operator might have a type
+
+handleA :: ... => a e c -> a (e,Ex) c -> a e c
+
+where Ex is the type of exceptions handled.
+You could then use this with arrow notation by writing a command
+
+body `handleA` \ ex -> handler
+
+so that if an exception is raised in the command body,
+the variable ex is bound to the value of the exception
+and the command handler,
+which typically refers to ex, is entered.
+Though the syntax here looks like a functional lambda,
+we are talking about commands, and something different is going on.
+The input to the arrow represented by a command consists of values for
+the free local variables in the command, plus a stack of anonymous values.
+In all the prior examples, this stack was empty.
+In the second argument to handleA,
+this stack consists of one value, the value of the exception.
+The command form of lambda merely gives this value a name.
+
+
+
+More concretely,
+the values on the stack are paired to the right of the environment.
+So when designing operators like handleA that pass
+extra inputs to their subcommands,
+More precisely, the type of each argument of the operator (and its result)
+should have the form
+
+a (...(e,t1), ... tn) t
+
+where e is a polymorphic variable
+(representing the environment)
+and ti are the types of the values on the stack,
+with t1 being the top.
+The polymorphic variable e must not occur in
+a, ti or
+t.
+However the arrows involved need not be the same.
+Here are some more examples of suitable operators:
+
+bracketA :: ... => a e b -> a (e,b) c -> a (e,c) d -> a e d
+runReader :: ... => a e c -> a' (e,State) c
+runState :: ... => a e c -> a' (e,State) (c,State)
+
+We can supply the extra input required by commands built with the last two
+by applying them to ordinary expressions, as in
+
+proc x -> do
+ s <- ...
+ (|runReader (do { ... })|) s
+
+which adds s to the stack of inputs to the command
+built using runReader.
+
--- The splice operator $ takes the Haskell source code
--- generated at compile time by "pr" and splices it into
--- the argument of "putStrLn".
-main = putStrLn ( $(pr "Hello") )
-
+
+The command versions of lambda abstraction and application are analogous to
+the expression versions.
+In particular, the beta and eta rules describe equivalences of commands.
+These three features (operators, lambda abstraction and application)
+are the core of the notation; everything else can be built using them,
+though the results would be somewhat clumsy.
+For example, we could simulate do-notation by defining
+
+bind :: Arrow a => a e b -> a (e,b) c -> a e c
+u `bind` f = returnA &&& u >>> f
+bind_ :: Arrow a => a e b -> a e c -> a e c
+u `bind_` f = u `bind` (arr fst >>> f)
+
+We could simulate do by defining
-{- Printf.hs -}
-module Printf where
+cond :: ArrowChoice a => a e b -> a e b -> a (e,Bool) b
+cond f g = arr (\ (e,b) -> if b then Left e else Right e) >>> f ||| g
+
+
--- Skeletal printf from the paper.
--- It needs to be in a separate module to the one where
--- you intend to use it.
+
--- Import some Template Haskell syntax
-import Language.Haskell.THSyntax
+
+Differences with the paper
--- Describe a format string
-data Format = D | S | L String
+
--- Parse a format string. This is left largely to you
--- as we are here interested in building our first ever
--- Template Haskell program and not in building printf.
-parse :: String -> [Format]
-parse s = [ L s ]
+
+Instead of a single form of arrow application (arrow tail) with two
+translations, the implementation provides two forms
+-< (first-order)
+and -<< (higher-order).
+
+
--- Generate Haskell source code from a parsed representation
--- of the format string. This code will be spliced into
--- the module which calls "pr", at compile time.
-gen :: [Format] -> Expr
-gen [D] = [| \n -> show n |]
-gen [S] = [| \s -> s |]
-gen [L s] = string s
+
+User-defined operators are flagged with banana brackets instead of
+a new form keyword.
+
+
--- Here we generate the Haskell code for the splice
--- from an input format string.
-pr :: String -> Expr
-pr s = gen (parse s)
-
+
-Now run the compiler (here we are using a "stage three" build of GHC, at a Cygwin prompt on Windows):
+
+
+
+Portability
+
+
+Although only GHC implements arrow notation directly,
+there is also a preprocessor
+(available from the
+arrows web page)
+that translates arrow notation into Haskell 98
+for use with other Haskell systems.
+You would still want to check arrow programs with GHC;
+tracing type errors in the preprocessor output is not easy.
+Modules intended for both GHC and the preprocessor must observe some
+additional restrictions:
+
+
+
+
+The module must import
+Control.Arrow.
-
-ghc/compiler/stage3/ghc-inplace --make -fglasgow-exts -package haskell-src main.hs -o main.exe
-
+
-Run "main.exe" and here is your output:
+
+
+The preprocessor cannot cope with other Haskell extensions.
+These would have to go in separate modules.
+
-
-$ ./main
-Hello
-
+
+
+Because the preprocessor targets Haskell (rather than Core),
+let-bound variables are monomorphic.
+
+
+
+
+
-
+
@@ -3455,24 +4005,72 @@ Assertion failures can be caught, see the documentation for the
unrecognised word is (silently)
ignored.
-
-INLINE pragma
+
+ DEPRECATED pragma
+ DEPRECATED
+
-INLINE and NOINLINE pragmas
-pragma, INLINE
+ The DEPRECATED pragma lets you specify that a particular
+ function, class, or type, is deprecated. There are two
+ forms.
-
-GHC (with , 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.
-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.
-
+
+
+ You can deprecate an entire module thus:
+
+ module Wibble {-# DEPRECATED "Use Wobble instead" #-} where
+ ...
+
+ When you compile any module that import
+ Wibble, GHC will print the specified
+ message.
+
-
-The sledgehammer you can bring to bear is the
-INLINEINLINE pragma pragma, used thusly:
+
+ You can deprecate a function, class, or type, with the
+ following top-level declaration:
+
+ {-# DEPRECATED f, C, T "Don't use these" #-}
+
+ When you compile any module that imports and uses any
+ of the specifed entities, GHC will print the specified
+ message.
+
+
+ Any use of the deprecated item, or of anything from a deprecated
+ module, will be flagged with an appropriate message. However,
+ deprecations are not reported for
+ (a) uses of a deprecated function within its defining module, and
+ (b) uses of a deprecated function in an export list.
+ The latter reduces spurious complaints within a library
+ in which one module gathers together and re-exports
+ the exports of several others.
+
+ You can suppress the warnings with the flag
+ .
+
+
+
+ INLINE and NOINLINE pragmas
+
+ These pragmas control the inlining of function
+ definitions.
+
+
+ INLINE pragma
+ INLINE
+
+ GHC (with , 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.
+ 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
+ INLINEINLINE
+ pragma pragma, used thusly:
key_function :: Int -> String -> (Bool, Double)
@@ -3481,25 +4079,26 @@ key_function :: Int -> String -> (Bool, Double)
{-# INLINE key_function #-}
#endif
-(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.
-
+ (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.)
-
-Syntactially, an INLINE pragma for a function can be put anywhere its type
-signature could be put.
-
+ 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.
-
-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:
+ Syntactially, 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:
#ifdef __GLASGOW_HASKELL__
@@ -3508,95 +4107,140 @@ For example, in GHC's own UniqueSupply monad code, we have:
#endif
-
-
-
-The NOINLINE pragma
-
-NOINLINE pragma
-pragmaNOINLINE
-NOTINLINE pragma
-pragmaNOTINLINE
-
-
-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.
-
-
-NOTINLINE is a synonym for
-NOINLINE (NOTINLINE is specified
-by Haskell 98 as the standard way to disable inlining, so it should be
-used if you want your code to be portable).
-
-
+ See also the NOINLINE pragma ().
+
+
+
+ NOINLINE pragma
+
+ NOINLINE
+ NOTINLINE
+
+ 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.
+
+ NOTINLINE is a synonym for
+ NOINLINE (NOTINLINE is
+ specified by Haskell 98 as the standard way to disable
+ inlining, so it should be used if you want your code to be
+ portable).
+
+
+
+ Phase control
+
+ Sometimes you want to control exactly when in GHC's
+ pipeline the INLINE pragma is switched on. Inlining happens
+ only during runs of the simplifier. Each
+ run of the simplifier has a different phase
+ number; the phase number decreases towards zero.
+ If you use you'll see the
+ sequence of phase numbers for successive runs of the
+ simpifier. In an INLINE pragma you can optionally specify a
+ phase number, thus:
-
-Phase control
-
- Sometimes you want to control exactly when in GHC's pipeline
-the INLINE pragma is switched on. Inlining happens only during runs of
-the simplifier. Each run of the simplifier has a different
-phase number; the phase number decreases towards zero.
-If you use
-you'll see the sequence of phase numbers for successive runs of the simpifier.
-In an INLINE pragma you can optionally specify a phase number, thus:
-
-You can say "inline f in Phase 2 and all subsequent
-phases":
+
+
+ You can say "inline f in Phase 2
+ and all subsequent phases":
{-# INLINE [2] f #-}
-
+
+
-You can say "inline g in all phases up to, but
-not including, Phase 3":
+
+ You can say "inline g in all
+ phases up to, but not including, Phase 3":
{-# INLINE [~3] g #-}
-
+
+
-If you omit the phase indicator, you mean "inline in all phases".
-
-
-You can use a phase number on a NOINLINE pragma too:
-
-You can say "do not inline f until Phase 2; in
-Phase 2 and subsequently behave as if there was no pragma at all":
+
+ If you omit the phase indicator, you mean "inline in
+ all phases".
+
+
+
+ You can use a phase number on a NOINLINE pragma too:
+
+
+
+ You can say "do not inline f
+ until Phase 2; in Phase 2 and subsequently behave as if
+ there was no pragma at all":
{-# NOINLINE [2] f #-}
-
+
+
-You can say "do not inline g in Phase 3 or any subsequent phase;
-before that, behave as if there was no pragma":
+
+ You can say "do not inline g in
+ Phase 3 or any subsequent phase; before that, behave as if
+ there was no pragma":
{-# NOINLINE [~3] g #-}
-
+
+
-If you omit the phase indicator, you mean "never inline this function".
-
-
-
-The same phase-numbering control is available for RULES ().
-
+
+ If you omit the phase indicator, you mean "never
+ inline this function".
+
+
+
+ The same phase-numbering control is available for RULES
+ ().
+
+
+
+ LINE pragma
+ LINEpragma
+ pragmaLINE
+ 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
-
+
+{-# LINE 42 "Foo.vhs" #-}
+
-
-RULES pragma
+ 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.
+
-
-The RULES pragma lets you specify rewrite rules. It is described in
-.
-
+
+ OPTIONS pragma
+ OPTIONS
+
+ pragmaOPTIONS
+
+
+ The OPTIONS pragma is used to specify
+ additional options that are given to the compiler when compiling
+ this source file. See for
+ details.
+
-
+
+ RULES pragma
+ The RULES pragma lets you specify rewrite rules. It is
+ described in .
+ SPECIALIZE pragma
@@ -3625,35 +4269,34 @@ hammeredLookup :: Ord key => [(key, value)] -> key -> value
A SPECIALIZE pragma for a function can
be put anywhere its type signature could be put.
- To get very fancy, you can also specify a named function
- to use for the specialised value, as in:
-
+A SPECIALIZE has the effect of generating (a) a specialised
+version of the function and (b) a rewrite rule (see ) that
+rewrites a call to the un-specialised function into a call to the specialised
+one. You can, instead, provide your own specialised function and your own rewrite rule.
+For example, suppose that:
-{-# RULES "hammeredLookup" hammeredLookup = blah #-}
+ genericLookup :: Ord a => Table a b -> a -> b
+ intLookup :: Table Int b -> Int -> b
-
- where blah is an implementation of
- hammerdLookup written specialy for
- Widget lookups. It's Your
+where intLookup is an implementation of genericLookup
+that works very fast for keys of type Int. Then you can write the rule
+
+ {-# RULES "intLookup" genericLookup = intLookup #-}
+
+(see ). It is Your
Responsibility to make sure that
- blah really behaves as a specialised
- version of hammeredLookup!!!
-
- Note we use the RULE pragma here to
- indicate that hammeredLookup applied at a
- certain type should be replaced by blah. See
- for more information on
- RULES.
+ intLookup really behaves as a specialised
+ version of genericLookup!!!An example in which using RULES for
specialisation will Win Big:
-toDouble :: Real a => a -> Double
-toDouble = fromRational . toRational
+ toDouble :: Real a => a -> Double
+ toDouble = fromRational . toRational
-{-# RULES "toDouble/Int" toDouble = i2d #-}
-i2d (I# i) = D# (int2Double# i) -- uses Glasgow prim-op directly
+ {-# RULES "toDouble/Int" toDouble = i2d #-}
+ i2d (I# i) = D# (int2Double# i) -- uses Glasgow prim-op directly
The i2d function is virtually one machine
@@ -3688,73 +4331,71 @@ of the pragma.
-
-LINE pragma
-
-
-
-LINE pragma
-pragma, LINE
-
-
-
-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
-
-
-
-
-
-{-# LINE 42 "Foo.vhs" #-}
-
-
-
-
-
-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.
-
-
-
-
-
-DEPRECATED pragma
-
-
-The DEPRECATED pragma lets you specify that a particular function, class, or type, is deprecated.
-There are two forms.
-
-
-
-You can deprecate an entire module thus:
-
- module Wibble {-# DEPRECATED "Use Wobble instead" #-} where
- ...
-
-
-When you compile any module that import Wibble, GHC will print
-the specified message.
-
-
-
-
-You can deprecate a function, class, or type, with the following top-level declaration:
-
-
- {-# DEPRECATED f, C, T "Don't use these" #-}
-
-
-When you compile any module that imports and uses any of the specifed entities,
-GHC will print the specified message.
-
-
-
-You can suppress the warnings with the flag .
-
-
+
+ UNPACK pragma
+
+ UNPACK
+
+ The UNPACK indicates to the compiler
+ that it should unpack the contents of a constructor field into
+ the constructor itself, removing a level of indirection. For
+ example:
+
+
+data T = T {-# UNPACK #-} !Float
+ {-# UNPACK #-} !Float
+
+
+ will create a constructor T containing
+ two unboxed floats. This may not always be an optimisation: if
+ the T constructor is scrutinised and the
+ floats passed to a non-strict function for example, they will
+ have to be reboxed (this is done automatically by the
+ compiler).
+
+ Unpacking constructor fields should only be used in
+ conjunction with , in order to expose
+ unfoldings to the compiler so the reboxing can be removed as
+ often as possible. For example:
+
+
+f :: T -> Float
+f (T f1 f2) = f1 + f2
+
+
+ The compiler will avoid reboxing f1
+ and f2 by inlining +
+ on floats, but only when is on.
+
+ Any single-constructor data is eligible for unpacking; for
+ example
+
+
+data T = T {-# UNPACK #-} !(Int,Int)
+
+
+ will store the two Ints directly in the
+ T constructor, by flattening the pair.
+ Multi-level unpacking is also supported:
+
+
+data T = T {-# UNPACK #-} !S
+data S = S {-# UNPACK #-} !Int {-# UNPACK #-} !Int
+
+
+ will store two unboxed Int#s
+ directly in the T constructor. The
+ unpacker can see through newtypes, too.
+
+ If a field cannot be unpacked, you will not get a warning,
+ so it might be an idea to check the generated code with
+ .
+
+ See also the flag,
+ which essentially has the effect of adding
+ {-# UNPACK #-} to every strict
+ constructor field.
+
@@ -3769,7 +4410,10 @@ GHC will print the specified message.
The programmer can specify rewrite rules as part of the source program
-(in a pragma). GHC applies these rewrite rules wherever it can.
+(in a pragma). GHC applies these rewrite rules wherever it can, provided (a)
+the flag () is on,
+and (b) the flag
+() is not specified.
@@ -4217,7 +4861,7 @@ will fuse with one but not the other)
-
+
So, for example, the following should generate no intermediate lists:
@@ -4305,7 +4949,7 @@ If you add you get a more detailed listing.
- The defintion of (say) build in PrelBase.lhs looks llike this:
+ The defintion of (say) build in GHC/Base.lhs looks llike this:
build :: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a]
@@ -4323,9 +4967,9 @@ in the RHS of the INLINE thing. I regret the delicacy of thi
- In ghc/lib/std/PrelBase.lhs look at the rules for map to
+ In libraries/base/GHC/Base.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.
+program even if fusion doesn't happen. More rules in GHC/List.lhs.
@@ -4446,7 +5090,7 @@ Now you can make a data type into an instance of Bin like this:
instance (Bin a, Bin b) => Bin (a,b)
instance Bin a => Bin [a]
-That is, just leave off the "where" clasuse. Of course, you can put in the
+That is, just leave off the "where" clause. Of course, you can put in the
where clause and over-ride whichever methods you please.
@@ -4664,3 +5308,4 @@ Just to finish with, here's another example I rather like:
;;; sgml-parent-document: ("users_guide.sgml" "book" "chapter" "sect1") ***
;;; End: ***
-->
+