From ede08656f90d99fbafc54cf00085ab53e2504d71 Mon Sep 17 00:00:00 2001 From: simonpj Date: Fri, 25 Feb 2005 17:06:43 +0000 Subject: [PATCH] [project @ 2005-02-25 17:06:43 by simonpj] improve docs for scoped type vars --- ghc/docs/users_guide/glasgow_exts.xml | 57 +++++++++++++++++++++++---------- 1 file changed, 40 insertions(+), 17 deletions(-) diff --git a/ghc/docs/users_guide/glasgow_exts.xml b/ghc/docs/users_guide/glasgow_exts.xml index 93237d0..b986247 100644 --- a/ghc/docs/users_guide/glasgow_exts.xml +++ b/ghc/docs/users_guide/glasgow_exts.xml @@ -2673,22 +2673,19 @@ for rank-2 types. -A pattern type signature can introduce a scoped type -variable. For example - - - - +A lexically scoped type variable can be bound by: + +A declaration type signature () +A pattern type signature () +A result type signature () + +For example: f (xs::[a]) = ys ++ ys where ys :: [a] ys = reverse xs - - - - The pattern (xs::[a]) includes a type signature for xs. This brings the type variable a into scope; it scopes over all the patterns and right hand sides for this equation for f. @@ -2696,8 +2693,6 @@ In particular, it is in scope at the type signature for y. - Pattern type signatures are completely orthogonal to ordinary, separate -type signatures. The two can be used independently or together. At ordinary type signatures, such as that for ys, any type variables mentioned in the type signature that are not in scope are implicitly universally quantified. (If there are no type variables in @@ -2720,10 +2715,10 @@ So much for the basic idea. Here are the details. -What a pattern type signature means +What a scoped type variable means -A type variable brought into scope by a pattern type signature is simply -the name for a type. The restriction they express is that all occurrences +A lexically-scoped type variable is simply +the name for a type. The restriction it expresses is that all occurrences of the same name mean the same type. For example: f :: [Int] -> Int -> Int @@ -2893,7 +2888,33 @@ scope over the methods defined in the where part. For exampl - + +Declaration type signatures +A declaration type signature that has explicit +quantification (using forall) brings into scope the +explicitly-quantified +type variables, in the definition of the named function(s). For example: + + f :: forall a. [a] -> [a] + f (x:xs) = xs ++ [ x :: a ] + +The "forall a" brings "a" into scope in +the definition of "f". + +This only happens if the quantification in f's type +signature is explicit. For example: + + g :: [a] -> [a] + g (x:xs) = xs ++ [ x :: a ] + +This program will be rejected, because "a" does not scope +over the definition of "f", so "x::a" +means "x::forall a. a" by Haskell's usual implicit +quantification rules. + + + + Where a pattern type signature can occur @@ -3010,10 +3031,12 @@ in f4's scope. +Pattern type signatures are completely orthogonal to ordinary, separate +type signatures. The two can be used independently or together. - + Result type signatures -- 1.7.10.4