[Haskell-cafe] [Haskell] Lexically scoped type variables

Fri Nov 26 03:41:34 EST 2004

Hi,

let me answer your questions by comparing what's implemented in Chameleon.
(For details see
http://www.comp.nus.edu.sg/~sulzmann/chameleon/download/haskell.html#scoped)

 > ---- 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
 > instead.
 > 
 > Opinions?
 > 

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>
in <body>

(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>
in <body>

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.

Martin