wiki:ScopedTypeVariables

Version 8 (modified by malcolm.wallace@…, 9 years ago) (diff)

--

Scoped Type Variables

See ExtensionDescriptionHowto for information on how to write these extension descriptions. Please add any new extensions to the list of HaskellExtensions.

Brief Explanation

Type annotations, which Haskell 98 allows in expressions, are also allowed in patterns and (currently in GHC only) in result type signatures, attached to the left side of a function definition. New type variables in these annotations scope over the function body, permitting locally defined variables to be given signatures in situations where it would be impossible in Haskell 98, e.g.

sortImage :: Ord b => (a -> b) -> [a] -> [a]
sortImage (f::a->b) = sortBy cmp
  where cmp :: a -> a -> Ordering
        cmp x y = compare (f x) (f y)

References

Note that although GHC and Hugs use the same syntax, the meaning of type variables is quite different, and there are other differences too.

Pros

  • Allows better documentation (without them, some expressions cannot be annotated with their types).
  • Extensions such as RankNTypes and GADTs require such annotations, so even more important in conjunction with them.

Cons

  • Many different forms of scoped type variables in GHC makes them hard to reason about. For example:
        f :: a -> a 
        f = \x -> (x :: a)
    
    is rejected but
        g = let f :: a -> a = \x -> (x :: a) in f 
    
    is allowed.

Proposal 1

Both let-bound and lambda-bound type variables are in scope in the body of a function, and can be used in expression signatures. However, just as a let-binding can shadow other values of the same name, let-bound type variables may shadow other type variables. Thus no type variables are ever already in scope in a let-bound signature. Lambda-bound type variables (e.g. in a pattern) do not shadow but rather refer to the same type. ExplicitQuantification is required for all expression type signatures but not let-bound signatures.

This proposal tries to strike a balance between backwards compatibility, avoiding accidental type errors, and simplicity. Let-bound type signatures always create a new scope, lambda-bound ones are always in the same scope, and it is clear from expression type signatures which are the scoped type vars.

(perhaps this text can be cleaned up further? what is a better term for expression type signature?)