# GHC 7.10 Prelude: we need your opinion

This post asks for your help in deciding how to proceed with some Prelude changes in GHC 7.10. Please read on, but all the info is also at the survey link, here: http://goo.gl/forms/XP1W2JdfpX. Deadline is 21 Feb 2015.

The Core Libraries Committee (CLC) is responsible for developing the core libraries that ship with GHC. This is an important but painstaking task, and we owe the CLC a big vote of thanks for taking it on.

For over a year the CLC has been working on integrating the Foldable and Traversable classes (shipped in base in GHC 7.8) into the core libraries, and into the Prelude in particular. Detailed planning for GHC 7.10 started in the autumn of 2014, and the CLC went ahead with this integration.

Then we had a failure of communication. As these changes affect the Prelude, which is in scope for all users of Haskell, these changes should be held to a higher bar than the regular libraries@ review process. However, the Foldable/Traversable changes were not particularly well signposted. Many people have only recently woken up to them, and some have objected (both in principle and detail).

This is an extremely unfortunate situation. On the one hand we are at RC2 for GHC 7.10, so library authors have invested effort in updating their libraries to the new Prelude. On the other, altering the Prelude is in effect altering the language, something we take pretty seriously. We should have had this debate back in 2014, but here we are, and it is unproductive to argue about whose fault it is. We all share responsibility. We need to decide what to do now. A small group of us met by Skype and we've decided to do this:

- Push back GHC 7.10's release by at least a month, to late March. This delay also gives us breathing space to address an unrelated show-stopping bug, Trac #9858.

- Invite input from the Haskell community on which of two approaches to adopt (this survey). The main questions revolve around impact on the Haskell ecosystem (commercial applications, teaching, libraries, etc etc), so we want to ask your opinion rather than guess it.

- Ask Simon Marlow and Simon Peyton Jones to decide which approach to follow for GHC 7.10.

Wiki pages have been created summarizing these two primary alternatives, including many more points and counter-points and technical details:

This survey invites your input on which plan we should follow. Would you please

- Read the details of the alternative plans on the three wiki pages above
- Add your response to the survey

Please do read the background. Well-informed responses will help. Thank you!

DEADLINE: 21 February 2015

Simon PJ

# Static pointers and serialisation

This longish post gives Simon's reflections on the implementation of Cloud-Haskell-style static pointers and serialiation. See also

Much of what is suggested here is implemented, in some form, in two existing projects

**Cloud Haskell libraries**distributed-static and rank1dynamic. Background in the paper Towards Haskell in the Cloud.

**HdpH libraries**hdph and hdph-closure. Background in the paper Implementing a high-level distributed-memory parallel Haskell in Haskell

My goal here is to identify the smallest possible extension to GHC, with the smallest possible trusted code base, that would enable these libraries to be written in an entirely type-safe way.

# Background

## Background: the trusted code base

The implementation `Typeable` class, and its associated functions, in
GHC offers a **type-safe** abstraction, in the classic sense that
"well typed programs won't go wrong". For example, we in `Data.Typeable` we have

cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b

We expect `cast` to be type-safe: if `cast` returns a value `Just x` then we really do know
that `x :: b`. Let's remind ourselves of class `Typeable`:

class Typeable a where typeRep :: proxy a -> TypeRep

(It's not *quite* this, but close.) The `proxy a` argument is
just a proxy for *type* argument; its value is never inspected
and you can always pass bottom.

Under the hood, `cast` uses `typeRep` to get the runtime `TypeRep` for
`a` and `b`, and compares them, thus:

cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b cast x = if typeRep (Proxy :: Proxy a) == typeRep (Proxy :: Proxy b) then Just (unsafeCoerce x) else Nothing

Although `cast` is written in Haskell, it uses `unsafeCoerce`. For it
to truly be type-safe, it must trust the `Typeable` instances. If the
user could write a `Typeable` instance, they could write a bogus one, and
defeat type safety. So only GHC is allowed write `Typeable` instances.

In short, `cast` and the `Typeable` instances are part of the **trusted code base**, or **TCB**:

- The TCB should be as small as possible
- The TCB should have a small, well-defined, statically-typed API used by client code
- Client code is un-trusted; if the client code is well-typed, and the TCB is implemented correctly, nothing can go wrong

## Background `Typeable a` and `TypeRep`

I'll use the `Typeable a` type class and values of type `TypeRep` more or less interchangeably. As you can see from the definition of class `Typeable` above, its payload is simply a constant function returning a `TypeRep`. So you can think of a `Typeable a` as simply a type-tagged version of `TypeRep`.

Of course, a `Typeable a` is a type class thing, which is hard to pass around explicitly like a value, but that is easily fixed using the "Dict Trick",
well known in Haskell folk lore:

data Dict (c :: Constraint) where Dict :: forall c. c => Dict c

Now a value of type `Dict (Typeable a)` is an ordinary value that embodies a `Typeable a` dictionary. For example:

f :: Dict (Typeable a) -> Dict (Typeable b) -> a -> Maybe b f Dict Dict val = cast val

The pattern-matches against the `Dict` constructor brings the `Typeable` dictionaries
into scope, so they can be used to discharge the constraint arising from the call to `cast`.

## Background: serialisation

I'm going to assume a a type class `Serialisable`, something like this:

class Serialisable a where encode :: a -> ByteString decode :: ByteString -> Maybe (a, ByteString)

'll use "encode" and "decode" as synonyms for "serialise" and "deserialise", because the former are easier to pronounce.

Here's an interesting question: are instances of `Serialisable` part of the TCB? No, they are not.
Here is a tricky case:

decode (encode [True,False]) :: Maybe (Int, ByteString)

Here I have encode a `[Bool]` into a `ByteString`, and then decoded an `Int` from that `ByteString`. This may
be naughty or undesirable, but it cannot seg-fault: it is type-safe in the sense above. You can
think of it like this: a decoder is simply a parser for the bits in the `ByteString`, so a decoder
for (say) `Int` can fail to parse a full `Int` (returning `Nothing`), but it can't return a non-`Int`.

For the naughtiness, one could imagine that a Cloud Haskell library
might send fingerprints or `TypeReps` or whatnot to eliminate
potential naughtiness. But even then it is very valuable if the
type-safety of the system does not rely on the CH library. Type
safety depends only on the correctness of the (small) TCB;
naughtiness-safety might additionally depend on the correctness of the
CH library.

## Background: static pointers

I'm taking for granted the basic design of the Cloud Haskell paper. That is,

- A type constructor
`StaticPtr :: * -> *`. Intuitively, a value of type`StaticPtr t`is represented by a static code pointer to a value of type`t`. Note "code pointer" not "heap pointer". That's the point!

- A language construct
`static <expr>`, whose type is`StaticPtr t`if`<expr>`has type`t`.

- In
`static <expr>`, the free variables of`<expr>`must all be bound at top level. The implementation almost certainly works by giving`<expr>`a top-level definition with a new name,`static34 = <expr>`.

- A function
`unStatic :: StaticPtr a -> a`, to unwrap a static pointer.

`Static`values are serialisable. Something like`instance Serialisable (StaticPtr a)`. (This will turn out to be not quite right.) Operationally this works by serialising the code pointer, or top-level name (e.g`"Foo.static34"`).

All of this is built-in. It is OK for the implementation of `StaticPtr` to be part of the TCB.
But our goal is that *no other code need be in the TCB*.

**A red herring**. I'm not going to address the question of how to serialise a static pointer. One method would be to serialise a machine address, but that only works if the encoding and decoding ends are running identical binaries. But that's easily fixed: encode a static as the *name* of the static value e.g. "function `foo` from module `M` in package `p`". Indeed, I'll informally assume an implementation of this latter kind.

In general, I will say that what we ultimately serialise is a `StaticName`. You can think of a `StaticName` as package/module/function triple, or something like that. The implementation of `StaticName` is certainly not part of the client-visible API for `StaticPtr`; indeed, the type `StaticName` is not part of the API either. But it gives us useful vocabulary.

# Serialising static pointers

We can see immediately that we cannot expect to have `instance Serialisable (Static a)`,
which is what the Cloud Haskell paper proposed. If we had such an instance we would have

encodeStatic :: forall a. StaticPtr a -> ByteString decodeStatic :: forall a. ByteString -> Maybe (StaticPtr a, ByteString)

And it's immediately apparent that `decodeStatic` *cannot* be right.
I could get a `ByteString` from anywhere, apply `decodeStatic` to it,
and thereby get a `StaticPtr a`. Then use
`unStatic` and you have a value of type `a`, for, *for any type a*!!

Plainly, what we need is (just in the case of `cast`) to do a dynamic typecheck, thus:

decodeStatic :: forall a. Typeable a => ByteString -> Maybe (StaticPtr a, ByteString)

Let's think operationally for a moment:

- GHC collects all the
`StaticPtr`values in a table, the**static pointer table**or**SPT**. Each row contains- The
`StaticName`of the value - A pointer to closure for the value itself
- A pointer to its
`TypeRep`

- The

`decodeStatic`now proceeds like this:- Parse a
`StaticName`from the`ByteString`(failure =>`Nothing`) - Look it up in table (not found =>
`Nothing`) - Compare the
`TypeRep`passed to`decodeStatic`(via the`Typeable a`dictionary) with the one ine the table (not equal =>`Nothing`) - Return the value

- Parse a

**Side note.** Another possibility is for `decodeStatic` not to take a `Typeable a` context but instead for `unStatic` to do so:: `unStatic :: Typeable a => StaticPtr a -> Maybe a`. But that seems a mess. Apart from anything else, it would mean that a value of type `StaticPtr a` might or might not point to a value of type `a`, so there's no point in having the type parameter in the first place. **End of side note.**

This design has some useful consequences that are worth calling out:

- A
`StaticPtr`is serialised simply to the`StaticName`;*the serialised form does not need to contain a*. Indeed it would not even be type-safe to serialise a`TypeRep``StaticPtr`to a pair of a`StaticName`and a`TypeRep`, trusting that the`TypeRep`described the type of the named function. Why not? Think back to "Background: serialisation" above, and imagine we saiddecode (encode ["wibble", "wobble"]) :: Typeable a => Maybe (StaticPtr a, ByteString)

Here we create an essentially-garbage`ByteString`by encoding a`[String]`, and try to decode it. If, by chance, we successfully parse a valid`StaticName`and`TypeRep`, there is absolutely no reason to suppose that the`TypeRep`will describe the type of the function.

Instead, the`TypeRep`of the static pointer lives in the SPT, securely put there when the SPT was created. Not only is this type-safe, but it also saves bandwidth by not transmitting`TypeReps`.

- Since clients can effectively fabricate a
`StaticName`(by supplying`decodeStatic`with a bogus`ByteString`, a`StaticName`is untrusted. That gives the implementation a good deal of wiggle room for how it chooses to implement static names. Even a simple index in the range 0..N would be type-safe!

The motivation for choosing a richer representation for`StaticName`(eg package/module/name) is not type-safety but rather resilience to change. For example, the Haskell programs at the two ends could be quite different, provided only that they agreed about what to call the static pointers that they want to exchange.

## Statics and existentials

Here is something very reasonable:

data StaticApp b where SA :: StaticPtr (a->b) -> StaticPtr a -> StaticApp b unStaticApp :: StaticApp a -> a unStaticApp (SA f a) = unStatic f (unStatic a)

(We might want to add more constructors, but I'm going to focus only on `SA`.)
A `SA` is just a pair of `StaticPtr`s, one for a function and one for an argument. We can securely unwrap it with `unStaticApp`.

Now, here is the question: can we serialise `StaticApp`s? Operationally, of course yes: to serialise a `SA`, just serialise the two `StaticPtrs` it contains, and dually for deserialisation. But, as before, deserialisation is the hard bit. We seek:

decodeSA :: Typeable b => ByteString -> Maybe (StaticApp b, ByteString)

But how can we write `decodeSA`? Here is the beginning of an attempt:

decodeSA :: Typeable b => ByteString -> Maybe (StaticApp b, ByteString) decodeSA bs = case decodeStatic bs :: Maybe (StaticPtr (a->b)) of Nothing -> Nothing Just (fun, bs1) -> ...

and you can immediately see that we are stuck. Type variable `b` is not in scope.
More concretely, we need a `Typeable (a->b)` to pass in to `decodeStatic`,
but we only have a `Typeable b` to hand.

What can we do? Tantalisingly, we know that if `decodeStatic` succeeds in parsing a static `StaticName` from `bs` then, when we look up that `StaticName` in the Static Pointer Table, we'll find a `TypeRep` for the value. So rather than passing a `Typeable` dictionary into `decodeStatic`, we'd like to get one out!

With that in mind, here is a new type signature for `decodeStatic` that returns
both pieces:

data DynStaticPtr where DSP :: Typeable a => StaticPtr a -> DynStaticPtr decodeStatic :: ByteString -> Maybe (DynStaticPtr, ByteString)

(The name `DynStaticPtr` comes from the fact that this data type is extremely similar to the library definition of `Dynamic`.)

Operationally, `decodeStaticK bs fail cont` works like this;

- Parse a
`StaticName`from`bs`(failure => return Nothing) - Look it up in the SPT (not found => return Nothing)
- Return the
`TypeRep`and the value found in the SPT, paired up with`DSP`. (Indeed the SPT could contain the`DynStaticPtr`values directly.)

For the construction of `DynStaticPtr` to be type-safe, we need to know that the
`TypeRep` passed really is a `TypeRep` for the value; so the construction
of the SPT is (unsurprisingly) part of the TCB.

Now we can write `decodeSA` (the monad is just the `Maybe` monad, nothing fancy):

decodeSA :: forall b. Typeable b => ByteString -> Maybe (StaticApp b, ByteString) decodeSA bs = do { (DSP (fun :: StaticPtr tfun), bs1) <- decodeStatic bs ; (DSP (arg :: StaticPtr targ), bs2) <- decodeStatic bs1 -- At this point we have -- Typeable b (from caller) -- Typeable tfun (from first DSP) -- Typeable targ (from second DSP) ; fun' :: StaticPtr (targ->b) <- cast fun ; return (SA fun' arg, bs2) }

The call to `cast` needs `Typeable tfun`, and `Typeable (targ->b)`. The
former is bound by the first `DSP` pattern match. The latter is
constructed automatically from `Typeable targ` and `Typeable b`, both
of which we have. Bingo!

Notice that * decodeSA is not part of the TCB*. Clients can freely write code like

`decodeSA`and be sure that it is type-safe.

# From static pointers to closures

The original Cloud Haskell paper defines closures like this:

data Closure a where Clo :: StaticPtr (ByteString -> a) -> ByteString -> Closure a

It is easy to define

unClo :: Closure a -> a unClo (Clo s e) = unStatic s e

## Side note on HdpH

HdpH refines the Cloud Haskell `Closure` in (at least) two ways. I think (but I am not certain) that this declaration captures the essence:

data Closure a where Clo :: StaticPtr (ByteString -> a) -> Put () -> a -> Closure a

The refinements are:

- The extra argument of type 'a' to avoid costs when we build a closure and then unwrap it with
`unClo`locally, or repeatedly.

- The use of
`Put ()`rather than a`ByteString`for the serialised environment, to avoid repeated copying when doing nested serialisation.

Both are importnat, but they are orthogonal to the discussion about static types, so I'll use the CH definition from here on.

## Serialising closures

Just as in the case of `StaticPtr`, it is immediately clear that we
cannot expect to have

decodeClo :: ByteString -> Maybe (Closure a, ByteString)

Instead we must play the same trick, and attempt to define

data DynClosure where DC :: Typeable a => Closure a -> DynClosure decodeClo :: ByteString -> Maybe (DynClosure, ByteString)

But there's an immediate problem in writing `decodeClo`:

decodeClo bs = do { (DSP (fun :: StaticPtr tfun), bs1) <- decodeStatic bs ; (env, bs2) <- decodeByteString bs1 ; return (DC (Clo fun env), bs2) } -- WRONG

This won't typecheck because `DC` needs `Typeable `a`, but we only have `Typeable (ByteString -> a)`.

This is Jolly Annoying. I can see three ways to make progress:

**Plan A**: Provide some (type-safe) way to decompose`TypeReps`, to get from`Typeable (a->b)`to`Typeable b`(and presumably`Typeable a`as well).**Plan C**: Serialise a`TypeRep a`with every`Closure a`.**Plan C**: Generalise`StaticPtr`

I like Plan C best. They are each discussed next.

### Plan A: Decomposing `TypeRep`

At the moment, GHC provides statically-typed ways to *construct* and *compare* a `TypeRep` (via `cast`), but no way to *decompose* one, at least not in a type-safe way.
It is tempting to seek this function as part of the TCB:

class Typeable a where typeRep :: proxy a -> TypeRep decomposeTypeRep :: DecompTR a data DecompTR a where TRApp :: (Typeable p, Typeable q) => DecompTR (p q) TRCon :: TyCon -> DecompTR a

This isn't a bad idea, but it does mean that `Typeable a` *must* be implemented (and presumably serialised) using a tree, whereas the current API would allow an implementation consisting only of a fingerprint.

(Oct 2014) I now think that Plan A is the right path. See Typeable for a design of `Typeable` that properly supports it.

(Thought experiment: maybe a `Typeable a`, and `Dict (Typeable a)` can be represented as a tree, but a `TypeRep` could be just a fingerprint?)

### Plan B: serialise `TypeRep` with `Closure`

Since we need a `Typeable a` at the far end, we could just serialise it directly
with the `Closure`, like this:

encodeClo :: forall a. Typeable a => Closure a -> ByteString encodeClo (Clo fun env) = encodeTypeable (proxy :: a) ++ encodeStatic fun ++ encodeByteString env

Here I am assuming (as part of the TBC)

encodeTypeable :: Typeable a => proxy a -> ByteString decodeTypeable :: ByteString -> Maybe (DynTypeable, ByteString) data DynTypeable where DT :: Typeable a => proxy a -> DynTypeable

which serialises a `TypeRep`. (Or, operationally, perhaps just its fingerprint.)
Now I think we can write `decodeClo`:

decodeClo :: ByteString -> Maybe (DynClosure, ByteString) decodeClo bs = do { (DT (_ :: Proxy a), bs1) <- decodeTypeable ; (DSP (fun :: StaticPtr tfun), bs2) <- decodeStatic bs1 ; (env, bs3) <- decodeByteString bs2 ; fun' :: StaticPtr (ByteString -> a) <- cast fun ; return (DC (Clo fun' env), bs2) } -- WRONG

But this too is annoying: we have to send these extra `TypeRep`s when morally they are already sitting there in the SPT.

### Plan C: Generalising `StaticPtr`

Our difficulty is that we are deserialising `StaticPtr (ByteString -> a)` but we want to be given `Typeable a` not `Typeable (ByteString -> a)`. So perhaps we can decompose the type into a type constructor and type argument, like this:

data StaticPtr (f :: *->*) (a :: *) unStatic :: StaticPtr f a -> f a decodeStatic :: ByteString -> Maybe (DynStaticPtr, ByteString) data DynStaticPtr where DS :: (Typeable f, Typeable a) => StaticPtr (f a) -> DynStaticPtr

Each row of the SPT contains:

- The
`StaticName` - The value of type
`f a` - The
`Typeable f`dictionary - The
`Typeable a`dictionary

Now we can define closures thus:

data Closure a where Clo :: StaticPtr (ByteString ->) a -> ByteString -> Closure a

and these are easy to deserialise:

decodeClo :: ByteString -> Maybe (DynClosure, ByteString) decodeClo bs = do { (DSP (fun :: StaticPtr f a), bs1) <- decodeStatic bs ; (env, bs2) <- decodeByteString bs1 -- Here we have Typeable f, Typeable a ; fun' :: StaticPtr (ByteString ->) a <- cast fun -- This cast checks that f ~ (ByteString ->) -- Needs Typeable f, Typealbe (ByteString ->) ; return (DC (Clo fun env), bs2) } -- DC needs Typeable a

I like this a lot better, but it has knock on effects.

- The old
`StaticPtr a`is now`StaticPtr Id a`.

- What becomes of our data type for
`StaticApply`? Perhpasdata StaticApp f b where SA :: StaticPtr f (a->b) -> StaticPtr f b -> StaticApp f b unStaticApp :: Applicative => StaticApp f b -> f b

**Bottom line: I have not yet followed through all the details, and I think Plan A is better**

## Applying closures

Can we write `closureApply`? I'm hoping for a structure like this:

closureApply :: Closure (a->b) -> Closure a -> Closure b closureApply fun arg = Clo (static caStatic) (fun, arg) caStatic :: ByteString -> b -- WRONG caStatic bs = do { ((fun,arg), bs1) <- decode bs ; return (unClo fun (unClo arg), bs1) }

This is obviously wrong. `caStatic` clearly cannot have that type. It would
at least need to be

caStatic :: Typeable b => ByteString -> b

and now there is the thorny question of where the `Typeable b` dictionary comes from.

**ToDo: ...I have stopped here for now**

# Polymorphism and serialisation

For this section I'll revert to the un-generalised single-parameter `StaticPtr`.

## Parametric polymorphism

Consider these definitions:

rs1 :: Static ([Int] -> [Int]) rs1 = static reverse rs2 :: Static ([Bool] -> [Bool]) rs2 = static reverse rs3 :: forall a. Typeable a => Static ([a] -> [a]) rs3 = static reverse

The first two are clearly fine. The SPT will get one row for each of the two monomorphic calls to reverse, one with a `TypeRep` of `[Int] -> [Int]` and one with a `TypeRep` of `[Bool] -> [Bool]`.

But *both will have the same code pointer*, namely the code for the polymorpic `reverse` function. Could we share just one `StaticName` for all instantiations of `reverse`, perhaps including `rs3` as well?

I think we can. The story would be this:

- The SPT has a row for
`reverse`, containing- The
`StaticName`for`reverse` - A pointer to the code for
`reverse`(or, more precisely, its static closure). - A function of type
`TypeRep -> TypeRep`that, given the`TypeRep`for`a`returns a`TypeRep`for`[a] -> [a]`.

- The

- When we serialise a
`StaticPtr`we send- The
`StaticName`of the (polymorphic) function - A list of the
`TypeRep`s of the type arguments of the function

- The

- The rule for
`static <expr>`becomes this: the free*term*variables`<expr>`must all be top level, but it may have free*type*variables, provided they are all`Typeable`.

All of this is part of the TCB, of course.

## Type-class polymorphism

Consider `static sort` where `sort :: Ord a => [a] -> [a]`. Can we make such a `StaticPtr`. After all, `sort` gets an implicit value argument, namely an `Ord a` dictionary. If that dictionary can be defined at top level, well and good, so this should be OK:

ss1 :: StaticPtr ([Int] -> [Int]) ss1 = static sort

But things go wrong as soon as you have polymorphism:

ss2 :: forall a. Ord a => StaticPtr ([a] -> [a]) ss2 = static sort -- WRONG

Now, clearly, the dictionary is a non-top-level free variable of the call to `sort`.

We might consider letting you write this:

ss3 :: forall a. StaticPtr (Ord a => [a] -> [a]) ss3 = static sort -- ???

so now the `static` wraps a function expeting a dictionary. But that edges us uncomforatbly close to impredicative types, which is known to contain many dragons.

A simpler alternative is to use the Dict Trick (see Background above):

ss4 :: forall a. StaticPtr (Dict (Ord a) -> [a] -> [a]) ss4 = static sortD sortD :: forall a. Dict (Ord a) -> [a] -> [a] sortD Dict xs = sort xs

Now, at the call side, when we unwrap the `StaticPtr`, we need to supply an explicit `Ord` dictionary, like this:

...(unStatic ss4 Dict)....

For now, I propose to deal with type classes via the Dict Trick, which is entirely end-user programmable, leaving only parametric polymorphism for built-in support.

# New directions for Template Haskell

**Nota bene**: *TemplateHaskell/BlogPostChanges is a copy of this blog post, but with subsequent edits and improvements. Don't pay too much attention to the text below; I'm keeping it only so that you can see the context for comments*.

This post explores a set of design proposals for Template Haskell. They are inspired by discussion with Tim Sheard, Kathleen Fisher, and Jacques Carette. It was originally triggered by several Template Haskell tickets: including #4230, #4135, #4128, #4170, #4125, #4124, #4364, #6062, #6089. (See also #7016, which work better with the suggestions below.) Taken together, these proposals would make quite a big change to TH, I think for the better. Happily, I'm pretty sure they are relatively easy to implement.

There's an interesting critique of Template Haskell on StackOverflow, some (but not all) of which is addressed by proposals here.

But I'd like to get the design right; hence this post. I'm going to treat it as a working draft, and modify it in the light of comments. So please comment.

I'm going to assume that you are more or less familiar with Template Haskell. If not, there's lots of background on the Template Haskell page. It's a Wiki so you can help to improve it.

Here's the implementation page? the describes how we are going to implement this stuff.

# Some brief background

After parsing, GHC runs two completely separate passes, one after the other:

- The
**renamer**resolves scopes, fixing precisely which*binding site*is connected which*occurrence*of every variable. For example, you writelet x = \x -> x+1 in x

and the renamer changes it tolet x_77 = \x_78 -> x_78 + 1 in x_77

The renamer also performs depdenency analysis, which sorts bindings (both value declarations and type declarations) into the smallest possible mutually recursive groups. This prior sorting is required to maximise polymorphism in mutually recursive value bindings.

- The
**typechecker**works on the renamed program, and typechecks it.

At the moment these two passes relate to Template Haskell as follows:

**Quasi-quotes are run in the renamer**. Why? Because quasi-quotes can expand to patterns.

Consider this, which has a quasi-quoted pattern:

\x -> \ [pads| blah |] -> x+1

Is the "x" in "x+1" bound by the outer

\xor by the 'x' that might be bought into scope by the[pads| blah |]quasi-quote? The only way to know is to run the quasi-quote, so that's what happens.

**All other Template Haskell stuff is run in the typechecker**. Why? Because we try to typecheck quotations before feeding them into TH functions. More on this below.

# The main issue

The big issue is this: Template Haskell is both too *weakly* typed and too *strongly* typed.

## Too weakly typed

A TH quotation has type `Q Exp`, a type that says nothing about the type of the quoted term.
For example, consider

qnot :: Q Exp -> Q Exp qnot x = [| not $x |]

Presumably the author expects `$x` to be a boolean-valued term, but
that is not checked. For example we might write

h = $(qnot [| "hello" |])

in which we pass a string-valued term to `qnot`. The splice will typecheck fine,
but the returned code will be the ill-typed `not "hello"`. There is no soundness problem
because GHC typechecks the result of the splice `$(qnot [| "hello" |])`, but
the error is reported in code that the user never wrote.

Moreover, errors can be delayed. For example, suppose `qnot` was like this:

qnot :: Q Exp -> Q Exp qnot x = [| (not $x, length $x) |]

This cannot possibly be right, becuase `$x` cannot be both a boolean and a list.
Yet TH will accept it, because a splice has type `forall a.a`. The error will
only be reported to *callers* of `qnot`.

This is bad. MetaML solves this problem by giving types to quoted terms, something like this:

qnot :: TExp Bool -> TExp Bool qnot x = [| not $x |]

Here `TExp` (short for typed expressions) has a type parameter that expresses the
type of the quoted term.

In TH we deliberately did not do this, because it restricts expressiveness; see the original TH paper. We could make this choice without losing soundness because in TH, unlike in MetaML, all splicing is done at compile time, and the result of a splice is typechecked from scratch. But still, it's a weakness and, for some users (stand up Jacques), a very serious weakness.

## Too strongly typed

Even though TH cannot guarantee to construct only type-correct code,
every quotation is typechecked. For example, the quotation `[| "hello" && True |]`
would be rejected because it is internally inconsistent.

But with the advent of type splices (a very useful feature) typechecking quotes has become hard to do. Consider this:

f :: Q Type -> Q [Dec] f t = [d| data T = MkT $t; g (MkT x) = g+1 |]

This function f returns a declaration quote, declaring T and g. You'll see that the constructor MkT takes an argument whose type is passed (as a quotation) to f -- a type splice.

The difficulty is that we can't typecheck the declaration of 'g' until we know what $t is; and we won't know that until f is called. In short,

- we can't really typecheck the declaration quote at all

An analogous problem occurs in other declaration splices, for example

f t = [d| instance C $t where ... |]

Here GHC's check that an instance decl is always of form

instance C (T a b c)

falls over, again because we don't know what $t will be. Here's another example:

[| let { f :: $t; f = e } in .. |]

We can't sensibly typecheck the term without knowing what f's type signature is, and we can't know that without expanding the splice.

Here's a rather different example, #4364:

type N0 = $( [t| Z |] ) type N1 = $( [t| Z |] )

Faced with a type splice

type N0 = $(...blah...)

the renamer doesn't know what the splice will expand to, because splices are currently run later, in the type checker. So it pessimistically assumes that the splice could expand to mention anything in scope. But that pessimistic assuption triggers the error message

Cycle in type synonym declarations: m.hs:7:1-23: type N0 = $([t| Z |]) m.hs:8:1-23: type N1 = $([t| Z |]) }}}

All this is quite annoying. Several users have said "I'm just using a quotation as a convenient way to build a syntax tree. Please don't even try to typecheck it; just wait until it is finally spliced into a top-level splice".

# A proposal

TH currently embodies an uneasy compromise between being too strongly typed and too weakly typed. So my proposal is to move TH in both directions at once:

- Part A: Move the existing structures towards the expressive but weakly-typed end.
- Part B: Add new MetaML-style constructs for strongly-typed metaprogramming.
- Part C: Clean up and improve reification
- Part D: Quasi-quotation improvements

## Part A: Reduce typechecking for quotes

On the "make-it-weaker" front, here's what I propose:

**Cease typechecking TH quotes altogether**. Instead, to use GHC's terminology, we would*rename*a quote, but not*typecheck*it. The renaming pass ensures that the scope hygiene mechanisms would remain unchanged. By not attempting to typecheck we avoid all the tricky problems sketched above.

**Add pattern splices and local declaration splices**, as requested in #1476. For example-- mkPat :: Q Pat -> Q Pat f $(mkPat [p| x |]) = x+1 -- mkDecl :: Int -> Q [Dec] g x = let $(mkDecl 3) in ...

These are not supported today because they bring new variables into scope, and hence are incompatible with running splices only after the renamer is finished; see Notes on Template Haskell, section 8.

**Run TH splices in the renamer**, uniformly with quasi-quotes. Of course, we must still typecheck the code we are about to run. But there's an*existing*TH restriction that code run in top-level splices must be imported. So we can typecheck this code even during renaming, because it can only mention imported (and hence already fully-typechecked) code.

This solves #4364 because we run the splice in the renamer, so things are sorted out by the time we are checking for cycles (in the type checker).

**Allow quoted names as patterns**as requested by Conal Eliott. This is just a variation on allowing splices in patterns, since a quoted name`'x`is really just a simple splice

These changes would essentially implement the desires of those who say "I just want to generate syntax trees". All the mentioned bug reports would be fixed. The big loss is that quotes would not be typechecked at all.

## Lexical scoping

Consider these definitions:

g :: Int -> Q Pat y :: Int y = 7 f :: Int -> Q Exp f n = [| \ $(g n) -> y+1 |]

Where is the 'y' bound in the RHS of `f`?

- Perhaps by the
`y = 7`that is in scope at the definition of`f`? - Perhaps by the pattern that
`$(g n)`expands to? - Perhaps by a 'y' that is in scope at the splice site of
`f`? - Does it depend on whether
`$(g n)`in fact binds 'y'?

A major point about TH is that we get lexical scoping (also called "hygienic"). So, to me it seems the the first of these choices is the only reasonable one. If you want the second you can instead use explicit dynamic binding by saying

f n = [| \ $(g n) -> $(return (VarE (mkName "n"))) + 1 |]

So the rule would be:

- In a quote, a variable 'v' is bound by the lexically enclosing binding of 'v', ignoring all pattern and declaration splices.

To be consistent this should apply to top level splices too.

## A variation (probably not)

A possible, rather *ad hoc*, variation would be to still typecheck quotes that are (a) top level, and (b) expression quotes. For example, we might still reject this:

f x = [| $x + (True 'c') |]

because the quote is obviously ill-typed. Only quotes nested inside top-level splices would avoid the type checker (because if the splice is run in the renamer, we can't typecheck the nexted quote). For example:

$(f [| True 'c' |])

This splice would run in the renamer, and only the *result* of the splice would be typechecked.
But what about this?

f t = [| let g :: $t-> Int; g = e in .... |]

This is still very awkward to typecheck. After all, if `$t` expands to a polymorphic type, the
result of the splice might typecheck, but it's really impossible to typecheck without
knowing the signature. Maybe we should just give up if there's a type splice? The only really
simple thing is not to typecheck quotes at all.

## Part B: Add MetaML-style typed quotes

Template Haskell has quotes for terms, types, patterns, and declarations. They are all untyped, in the sense that the type of the quote tells you nothing about the type of the quoted thing. For example

[| True |] :: Q Exp

There's no clue that the type of the quoted expression is `Bool`.

In the case of terms (only), we know how from MetaML to
have *typed* quotations. Here's a proposed extension to TH to add
typed term quotes:

**Add a new type of typed expressions**`TExp a`

**Add a new term quotation form**`[|| e ||]`, called a*typed quote*; the type of the quote is`TExp ty`, where`ty`is the type of`e`. In the type-system jargon, this is the "introduction form" for`TExp`.

**Add a new splice form**`$$e`, called a*typed splice*. The term`e`must have type`TExp ty`, and the splice`$$e`then has type`ty`. This is the "elimination form" for`TExp`.

**Add a constant which takes a typed quote and returns an untyped one**:`unType :: TExp a -> Q Exp`

**Run these new typed splices in the typechecker**, not the renamer.

(The precise syntax for typed-quotes and type-splices is of course up for grabs. But doubling the symbols seems plausible to me.)

Here's a standard example:

power :: Int -> TExp (Int -> Int) power n = [|| \x -> $$(go n [|| x ||]) ||] where go :: TExp Int -> TExp Int go 0 x = [|| 1 ||] go n x = [|| $x * $$(go (n-1)) ||]

You could do this with existing TH but there'd be no guarantee that `power` would
return a well-typed term. With `TExp` there is.

Points to notice

- Unlike TH, the
*only*way to construct a value of type`TExp`is with a quote. You cannot drop into do-ntation, nor use explicit construction of the values in the`Exp`algebraic data type. That restriction limits expressiveness, but it enables the strong typing guarantees.

- There are no declaration, type, or pattern quotes for these typed quotes. Only terms.

- You can't use an untyped splice in a typed quote, thus
`[|| ...$(e)... ||]`. Similarly, you can't splice a type, pattern, or declaration group in a typed term quote.

- Using
`unType`you can go from the typed world to the untyped one, which lets you mix the worlds. Example:f :: TExp Int -> Q Exp -> Q Exp f qt qu = [| $(unType qt) + $qu |]

- Unlike
`Exp`,`TExp`is an abstract type, so you can't decompose values of type`TExp`. All you can do with them is splice them (into a program or a larger quote). Or you can convert to a`Q Exp`and*then*decompose, using the existing TH mechanisms. For exampleg :: TExp Int -> Q Exp g qt = do { tree <- unType qt ; case tree of VarE v -> ... ConE c -> ... ...etc... }

`TExp`is not a monad, but it is an applicative type constructor, although not quite an instance of`Applicative`class:pure e === [|| e ||] f <*> g = [|| $$f $$g ||]

Reminder: the`Applicative`class looks like thisclass Applicative f where pure :: a -> f a <*> :: f (a->b) -> f a -> f b

`TExp`is only "almost an instance" because`pure`isn't a function; its argument must be syntactically quoted.

**Syntax** is always a delicate point.

- We could use some other kind of bracket, although brackets are always in short supply; eg
`(| ... |)`or`{| ... |}`. - We could add Unicode brackets too (suggestions?); but I think we should have ASCII equivalents.
- Ian asked whether
`$(...)`could accept either`Q Exp`or`TExp`. I think not; we need to know which kind of splice it is before type checking.

## Part C: Reification and typechecking

The third part of this proposal concerns reification. The Q monad gives you access to the typechecker's environment. Notably, Template Haskell provides the function

reify :: Name -> Q Info

which, given the `Name` of a variable, type, or class, looks the `Name` up in the type environment and returns what the type checker knows about it:

data Info = TyConI -- A type Dec -- Declaration of the type | ClassI -- A class Dec -- Declaration of the class [ClassInstance] -- The instances of that class ...etc...

### What reify sees

A dark corner of `reify` is this: what types does `reify` see? Consider

f x = ($(do { xi <- reify 'x; ... }), x && True)

Here, `reify` can be used to examine the type of `x`. But the type
of `x` isn't fully known until the type checker has seen the
term `(x && True)`. So in current TH it's going to be unpredicatable
what you see for `x`, which is hardly satisfactory.

It seems to me that the only decent, predictable story is to say
that `reify` can only consult the *top-level* type environment.
More specifically, Template Haskell processes a program top-down:

module M where import ... f x = x $(th1 4) h y = k y y $(blah1) $(th2 10) w z = $(blah2)

TH processes this module as follows:

- Typecheck down to, but not including, the first splice,
`$(th1 4)`. These declarations constitute the first*declaration group*. - Typecheck and run the splice, which returns a bunch of declarations D1
- Typecheck the declarations D1 combined with the declarations down to, but not including, the second splice. These declarations consitute the second declaration group.
- Typecheck and run the next splice,
`$(th2 10)` - Rinse and repeat

So the proposal is as follows. A *declaration group* is the chunk of declarations created by a top-level declaration splice, plus those following it, down to but not includig the next top-level declaration splice. Then **the type environment seen by reify includes all the declaration up to the end of the immediately preceding declaration block, but no more.**

So, in the preceding example:

- A
`reify`inside the splice`$(th1 ..)`would see the definition of`f`. - A
`reify`inside the splice`$(blah)`woudl see the definition of`f`, but would not see any bindings created by`$(th1...)`. - A
`reify`inside the splice`$(th2..)`would see the definition of`f`, all the bindings created by`$(th1..)`, and teh definition of`h`. - A
`reify`inside the splice`$(blah2)`would see the same definitions as the splice`$(th2...)`.

This would mean that you could not say

f x = x g y = $(do { info <- reify 'f; ... })

because there is no top=level splice between the declaration of `f` and the splice.
But that seems reasonable to me. If you want that behaviour you can say

f x = x $(return []) g y = $(do { info <- reify 'f; ... })

### Reifying expressions

But what about *expressions*? It would be useful (stand up Kathleen)
to have a more elaborate reify, like this:

typecheck :: [(Name,Type)] -- Extend the type environment with this -> Exp -- The expression to typecheck -> Q (Either String Type) -- Typecheck the expression, returning -- Left error-message if typechecking fails -- Right type if typechecking succeeds

(For GHCi users, `reify f` is like `:info f`, while `typecheck [] (...)` is like `:type (...)`.)

You might ask whether we *can* typeckeck an expression; remember, these `Q ty` things
are going to be run in the renamer. But if the type environment is that in force
just before the last top-level splice, then all is well: that stuff has been fully
typechecked.

## Part D: quasiquotation

This part is unrelated to the preceding proposals, and is responding to #4372 and #2041.

- For #2041, rather than the proposal made there, I think the nicest thing is for
`Language.Haskell.TH`to expose a*Haskell*quasiquoter:parseHaskell :: QuasiQuoter

Remember that a`QuasiQuoter`is a quadruple of parsers:data QuasiQuoter = QuasiQuoter { quoteExp :: String -> Q Exp, quotePat :: String -> Q Pat, quoteType :: String -> Q Type, quoteDec :: String -> Q [Dec] }

If TH provided such parsers, you could use them to parse antiquotes. That seems better to than having strings in the TH syntax.

See #4430 for an excellent point about fixities.

- For #4372, I'm a bit agnostic. There is no technical issue here; it's just about syntax. Read the notes on the ticket.

- See #4429 for a suggestion about reifying
`Names`.

## Part E: Other minor issues

This section collects other TH changes that I think should be done.

- The
`InfixE`construtor of`Syntax.Exp`should only allow a`Var`in the operator position. See Trac #4877

# Let generalisation in GHC 7.0

[Note: updated to GHC 7.2, Sept 2011]

GHC 7.2 has a completely new type inference engine. The old one had grown to resemble the closing stages of a game of Jenga, in which making any change was a delicate operation that risked bringing the whole edifice crashing down. In particular, there were a dozen open bugs concerning type families that I had no idea how to fix.

This summer Dimitrios Vytiniotis, Brent Yorgey and I built a completely new inference engine. It rests on a solid technical foundation developed over the last couple of years, in a collaboration with Dimitrios, Tom Schrijvers, and Martin Sulzmann. There is a series of papers that lead up to it, but our JFP submission "Modular type inference with local assumptions" summarises the whole thing in one consistent notation.

The new engine feels much more solid to me, and indeed I've been able to close almost all those open bugs. Doubtless there will be some new ones, but I feel vastly more confident that we can fix them than I did with the old engine.

One other thing is that the new typechecker has completely swept away
the old rather *ad-hoc* stuff about "rigid" types in GADT pattern matches. So
you may find that some GADT programs will typecheck with fewer
type annotations than before.

However, there is one way in which GHC 7.2 will type *fewer* programs
than before, and that is the focus of this post. I want explain what the
change is, and how to adapt your code to accommodate it.

## Local polymorphism

Consider this (contrived) program:

{-# LANGUAGE ScopedTypeVariables #-} f :: forall a. a -> ((a, Char), (a, Bool)) f x = (g 'v', g True) where g :: forall b. b -> (a,b) g y = (x,y)

This polymorphism is expressed in `g`'s type signature:

`g`is a*polymorphic*function, because it is applied both to the character 'v' and to the boolean`True`.- However,
`g`is*monomorphic*in`a`, because`g`'s body mentions`x`

The type signature `g :: forall b. b -> (a,b)`
reflects these two points:

- The "
`forall b`" says that`g`is polymorphic in`b`.

- The
`a`in the signature must is the`a`in the type of`x`. This type variable`a`is brought into scope, in the body of`f`, by the`forall a`in the type signature for`f`.

The `LANGUAGE ScopedTypeVariables` pragma (a) allows you to use an
explicit "`forall`" in the type signature for a function `f`, and (b)
brings the `forall`'d type variables (`a` in this case) into scope in the body of the
function `f`.

## What has changed in GHC 7.2?

GHC 6.12 will compile the above program without any type signatures at all.
It infers the polymorphic type for `g`. But, if you are using
type families or GADTs, GHC 7.0 will not. More precisely:

- The flags
`-XGADTs`or`-XTypeFamilies`, or the corresponding`LANGUAGE`pragmas, imply the (new) flag`-XMonoLocalBinds`.

- With
`-XMonoLocalBinds`, non-top-level (or*local*) let/where bindings are not generalised.

- Remember that
`-fglasgow-exts`implies`-XGADTs`and hence`-XTypeFamilies`.

So given the type-signature-free code

{-# LANGUAGE MonoLocalBinds #-} f x = (g 'v', g True) where g y = (x,y)

GHC 7.2 will reject the program with

Foo.hs:6:17: Couldn't match expected type `Char' with actual type `Bool' In the first argument of `g', namely `True' In the expression: g True In the expression: (g 'v', g True)

Why? Because the type of `g` is not generalised, so it
can only be applied to either `Char` or `Bool` but not both.

## Which bindings are affected?

In the JFP paper we propose the rule that *local bindings are not generalised*,
where "local" means "syntactically not top level". This was the rule implemented by GHC 7.0.

However GHC 7.2 relaxes the restriction slightly. Consider

{-# LANGUAGE MonoLocalBinds #-} f x = (k 'v', k True) where h y = (y,y) -- Note: x is not mentioned k z = (h z, h z)

Now the binding for `h` is "local" in the sense that it is
not syntactically top-level, but it has no free variables, so it
*could have been* top-level. Similarly, `k` is "local" but
only mentions `h` which could have been top-level, and hence `k`
could be top-level too. GHC 7.2 spots this, and generalises both
just as if they had been top level.

Here's the rule. With `-XMonoLocalBinds` (the default), a binding without a
type signature is **generalised only if all its free variables are closed**.

A binding is **closed** if and only if

- It has a type signature, and the type signature has no free variables; or
- It has no type signature, and all its free variables are closed, and it is unaffected by the monomorphism restriction. And hence it is fully generalised.

In our example, `h` has no free variables and hence is generalised;
moreover, `k` has free variable `h`, but it is closed, so `k` too can be
generalised.

Here's another example:

x = 4 + 5 y = x + 7

Both bindings are top-level, but `x` falls under the Monomorphism Restriction and is not generalised for that reason. So `x` is not closed. Hence `y` is not generalised either, since it has a non-closed free variable `x`. (This really fixes a bug in GHC 7.0 which erroneously generalised `y` because it was syntactically top level.)

## How can I fix my program?

Almost all code doesn't need local let definitions to have
a polymorphic type, because the function is only used at one type.
But not all. There are two ways to fix your program if it falls
over because of the `MonoLocalBinds` change.

- Check whether you need
`-XGADTs`or`-XTypeFamilies`. If you are using the blunderbuss`-fglasgow-exts`, replace it with proper`LANGUAGE`pragmas.

- The good way is simply give a type signature to the local definition, as I did for
`g`above. Writing such a type signature may force you to use`{-# LANGUAGE ScopedTypeVariables #-}`as the above example showed. My experience is that the code is easier to understand with the type signature.

- The
`-XGADTs`or`-XTypeFamilies`pragmas switch on`MonoLocalBinds`but, if you want, you can override it with`-XNoMonoLocalBinds`(or the equivalent`LANGUAGE`pragma). The type checker will then do its best to generalise local bindings, and your program will almost certainly work. However, I don't know how to guarantee any good properties of the type inference algorithm. So I think this is ok as as short term fix, but I'd like to encourage you to add that handful of type signatures instead.

You may not be very familiar with the code,
so it can be tricky to work out what type the local definition should have.
(That's one reason I think that the code is improved by having a type signature!)
With this in mind I've added a new warning flag `-fwarn-missing-local-sigs`, which
prints a warning, and the type, of any *polymorphic* local binding that
lacks a type signature. So you can follow this procedure:

- Compile with
`-XNoMonoLocalBinds -fwarn-missing-local-sigs`. The first flag makes it compile, and the second shows you the types. - Compile with neither flag, getting some errors.
- Add type signatures to cure the errors, using the types printed out in the first step.

Adding the type signature is completely compatible with GHC 6.12 etc, so you shouldn't need any conditional compilation if you want to compile your code with multiple versions of GHC.

## A second, bigger example

One relatively common situation in which you need a local type signature
is when you use `runST` with some auxiliary definitions.
Here is a typical example:

{-# LANGUAGE ScopedTypeVariables #-} module Test where import Control.Monad.ST import Data.STRef foo :: forall a. Bool -> a -> a -> a foo b x y = runST (do { r <- newSTRef x; fill r; readSTRef r }) where -- fill :: forall s. STRef s a -> ST s () fill r = case b of True -> return () False -> writeSTRef r y -- runST :: forall a. (forall s. ST s a) -> a -- newSTRef :: a -> ST s (STRef s a) -- readSTRef :: STRef s a -> ST s a -- writeSTRef :: STRef s a -> a -> ST s ()

The function `foo` is a bit contrived, but it's typical of the way
in which `runST` is often used. We allocate a reference cell, containing `x`,
call `fill`, and then read out what is now in the reference cell.
All `fill` does is overwrite the cell if `b` is `False`.
So `foo` is really an elaborate `if` function.

But in GHC 7.0, with `-XMonoLocalBinds` (or `-XGADTs`, `-XTypeFamilies`),
the program will be rejected with this alarming-seeming error message

Foo.hs:7:11: Couldn't match type `s' with `s1' because this skolem type variable would escape: `s1' This skolem is bound by the polymorphic type `forall s. ST s a' The following variables have types that mention s fill :: STRef s a -> ST s () (bound at Foo.hs:10:11) In the first argument of `runST', namely `(do { r <- newSTRef x; fill r; readSTRef r })'

Remember, `fill` has not been generalised, so it gets a monomorphic type.
That in turn means that the argument to `runST` is not polymorphic enough.

Despite its scariness, in some ways the error message identifies
the problem more clearly than the previous example. In particular, the error
message identifies `fill` as the culprit.
You can fix it the same way as before, by adding a signature for `fill`;
I've put it in a comment above.

## Why make this change?

At first this change seems like retrograde step, so why did we make it? It's a long story, but the short summary is this: I don't know how to build a reliable, predictable type inference engine for a type system that has both (a) generalisation of local let/where and (b) local type equality assumptions, such as those introduced by GADTs. The story is told in our paper "Let should not be generalised" and, at greater length, in the journal version "Modular type inference with local assumptions".