lexically-scoped type variables in GHC 6.6

Simon Peyton-Jones simonpj at microsoft.com
Thu Sep 7 04:36:06 EDT 2006


| With reference to the documentation [about lexically scoped type
variables] that just appeared in darcs:

For the benefit of others, the draft 6.6 documentation is here
	
http://www.haskell.org/ghc/dist/current/docs/users_guide/type-extensions
.html#scoped-type-variables

| Result type signatures are now equivalent to attaching the signature
| to the rhs, i.e. redundant.

Yes, that's true.  I don't think I had fully absorbed that.  They didn't
*use* to be redundant, because they used to bind type variables, but now
that they don't they are entirely redundant.  It is perhaps sometimes a
bit more convenient to write the (small) type before the (big)
expression, but that's true of type signatures in general.  If we cared
about that we should provide a prefix form of expression type signature

I think I will therefore remove them from the documentation, and (in due
course) from the code.  

| How about finishing the decoupling of type variable binding from
pattern
| type signatures by introducing an (optional) pattern form
| 
| 	forall v1 ... vk. C p1 ... pn
| 
| mimicking the datatype declaration for an existential (with vi scoping
| over pj, guards, where decls and the rhs), so the example would become
| 
| 	data T = forall a. MkT [a]
| 
| 	k :: T -> T
| 	k (forall a. MkT [t]) = MkT t3
| 		where
| 		t3::[a] = [t,t,t]

Stepanie and I have discussed this idea -- but in a different syntax.
We were thinking of writing a pattern like

	k (MkT {a} [t]) = ...

where the {a} binds the polymorphic parameters.  But that's new syntax
and I quite like your idea of re-using forall.

The other awkward question is: when there are several existential type
variables, which order do they come in?  You may say "the foralls in the
data type decl must match the foralls in the pattern".  Thus
	data T = forall a b. MkT ...
	k (forall a b. MkT ...) = ...
But with GADTs, you don't necessarily write a forall.  Suppose T was
declared thus:
	data T where
	  MkT :: b -> a -> T
Now, which order should the foralls in the pattern come in?

Simon


More information about the Glasgow-haskell-users mailing list