[Haskell] Lexically scoped type variables

26 Nov 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

Martin Sulzmann

tags

participants (1)