lexically-scoped type variables in GHC 6.6
With reference to the documentation that just appeared in darcs: Result type signatures are now equivalent to attaching the signature to the rhs, i.e. redundant. 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]
| 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
Ross Paterson wrote:
data T = forall a. MkT [a]
k :: T -> T k (forall a. MkT [t]) = MkT t3 where t3::[a] = [t,t,t]
What was wrong with the example in the documentation? k :: T -> T k (MkT [t::a]) = MkT t3 where t3::[a] = [t,t,t] The type of (t) is (a) - what could possibly be simpler? No doubt I'm missing something because the docs then go on to say "If this seems a little odd..." - but it doesn't. It makes perfect sense. Why shouldn't a pattern type signature introduce a scoped type variable? It also has the advantage that you can see what the type variable is supposed to represent without having to track down the original data declaration. Regards, Brian. -- Logic empowers us and Love gives us purpose. Yet still phantoms restless for eras long past, congealed in the present in unthought forms, strive mightily unseen to destroy us. http://www.metamilk.com
Brian Hulley wrote:
Ross Paterson wrote:
data T = forall a. MkT [a]
k :: T -> T k (forall a. MkT [t]) = MkT t3 where t3::[a] = [t,t,t]
What was wrong with the example in the documentation?
k :: T -> T k (MkT [t::a]) = MkT t3 where t3::[a] = [t,t,t]
The type of (t) is (a) - what could possibly be simpler?
No doubt I'm missing something because the docs then go on to say "If this seems a little odd..." - but it doesn't. It makes perfect sense. Why shouldn't a pattern type signature introduce a scoped type variable? It also has the advantage that you can see what the type variable is supposed to represent without having to track down the original data declaration.
If the problem is that pattern type signatures normally have an implicit forall (which stops them introducing lexically scoped type variables), perhaps the implicit forall could be discarded so that any type variables in a pattern signature not in the scope of an *explicit* forall would be lexically scoped over the whole of an equation (or the guarded part if they occur first in the guard) eg: foo (f :: a -> b) (x:: a) = ((f x) :: b) meaning: forall a b. (foo (f :: a -> b) (x :: a) = ((f x) :: b)) and foo (f :: forall a. a-> b) x = ((f x) :: b) meaning: forall b. (foo (f :: forall a. a-> b) x = ((f x) :: b)) Apologies if I'm still missing what the real problem is, Brian.
participants (3)
-
Brian Hulley -
Ross Paterson -
Simon Peyton-Jones