[Haskell-cafe] [Haskell] Lexically scoped type variables
sulzmann at comp.nus.edu.sg
Fri Nov 26 03:41:34 EST 2004
let me answer your questions by comparing what's implemented in Chameleon.
(For details see
> ---- QUESTION 1 -----
> In short, I'm considering adopting the Mondrian/Chameleon rule for GHC.
> There are two variations
> 1a) In the example, 'a' is only brought into scope in the
> right hand side if there's an explicit 'forall' written by
> the programmer
> 1b) It's brought into scope even if the forall is implicit; e.g.
> f :: a -> a
> f x = (x::a)
> I'm inclined to (1a). Coments?
Currently, Chameleon goes for 1b), i.e. foralls are implicit. I agree
that 1a) might help the programmer to immediately see which variables
are bound by the outer scope.
> ----- QUESTION 2 ------
> The alternatives I can see are
> 2a) Make an arbitrary choice of (A) or (B); GHC currently chooses (B)
> 2b) Decide that the scoped type variables arising from pattern
> bindings scope only over the right hand side, not over
> the body of the let
> 2b) Get rid of result type signatures altogether; instead,
> use choice (1a) or (1b), and use a separate type signature
Chameleon goes for 2c)
A Chameleon speciality is that we can write
f ::: a->a
f x = True
f ::: a->a states that f has type a->a for some a.
::: follows the same scoping rules as ::
Then, the following statement
let f (x::[a],ys) = <rhs>
(I assume that x::[a] states here that x has type [a] for some a)
can be encoded as
let f ::: ([a],b)->c
f (x::[a],ys) = <rhs>
The main motivation behind Chameleon's lexically scoped annotations
was to allow for programs such as
class Eval a b where eval::a->b
f :: Eval a (b,c) => a->b
f x = let g :: (b,c)
g = eval x
in fst g
As Josef pointed out, there are also examples where it might be useful
that some inner annotations refer to variable a from the outer annotation.
More information about the Haskell-Cafe