From 9fa1f25e41b0b35bb8aeff7639cccc6f6abcaec6 Mon Sep 17 00:00:00 2001 From: chak Date: Sun, 14 Sep 2003 13:50:58 +0000 Subject: [PATCH] [project @ 2003-09-14 13:50:57 by chak] * Corrected some outdated comments re variables and type checking * Added some more details about type checking --- ghc/docs/comm/index.html | 6 +- ghc/docs/comm/the-beast/typecheck.html | 106 +++++++++++++++++++++++++++----- ghc/docs/comm/the-beast/vars.html | 27 +++++--- 3 files changed, 112 insertions(+), 27 deletions(-) diff --git a/ghc/docs/comm/index.html b/ghc/docs/comm/index.html index 32b07f2..bf83fcb 100644 --- a/ghc/docs/comm/index.html +++ b/ghc/docs/comm/index.html @@ -6,7 +6,7 @@ -

The Glasgow Haskell Compiler (GHC) Commentary [v0.13]

The Glasgow Haskell Compiler (GHC) Commentary [v0.14]

-Last modified: Sat Nov 9 15:01:44 EST 2002 +Last modified: Sat Sep 13 01:15:05 BST 2003 diff --git a/ghc/docs/comm/the-beast/typecheck.html b/ghc/docs/comm/the-beast/typecheck.html index 6f3c07c..2b9b553 100644 --- a/ghc/docs/comm/the-beast/typecheck.html +++ b/ghc/docs/comm/the-beast/typecheck.html @@ -16,6 +16,7 @@ checker as it has to handle the much more verbose Haskell AST, but it improves error messages, as the those message are based on the same structure that the user sees. +

GHC defines the abstract syntax of Haskell programs in HsSyn @@ -23,51 +24,128 @@ bound occurences of identifiers and patterns. The module TcHsSyn instantiates this structure for the type checker using TcEnv.TcId + href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcRnTypes.lhs">TcRnTypes.TcId to represent identifiers - in fact, a TcId is currently nothing but just a synonym for a plain Id. +

+ +

Entry Points Into the Type Checker

+ The interface of the type checker (and renamer) to the rest of the + compiler is provided by TcRnDriver. + Entire modules are processed by calling tcRnModule and GHCi + uses tcRnStmt and tcRnExpr to typecheck + statements and expressions, respectively. Moreover, + tcRnIface and tcRnExtCore are provided to + typecheck interface files and external Core code. +

Types Variables and Zonking

During type checking type variables are represented by mutable variables - cf. the variable story. Consequently, unification can instantiate type variables by updating those mutable - variables. This process of instantiation is (for reasons that elude - me) called zonking in GHC's sources. The zonking routines for the various forms of Haskell constructs are responsible for most of the code in the module TcHsSyn, whereas the routines that actually operate on mutable types are defined in TcMTypes; - this includes routines to create mutable structures and update them as - well as routines that check constraints, such as that type variables in - function signatures have not been instantiated during type checking. - The actual type unification routine is uTys in the same - module. + href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcMType.lhs">TcMType; + this includes the zonking of type variables and type terms, routines to + create mutable structures and update them as well as routines that check + constraints, such as that type variables in function signatures have not + been instantiated during type checking. The actual type unification + routine is uTys in the module TcUnify. +

All type variables that may be instantiated (those in signatures may not), but haven't been instantiated during type checking, are zonked to (), so that after type checking all mutable variables have been eliminated. +

+ +

Type Representation

+ The representation of types is fixed in the module TcRep + and exported as the data type Type. As explained in TcType, + GHC supports rank-N types, but, in the type checker, maintains the + restriction that type variables cannot be instantiated to quantified + types (i.e., the type system is predicative). The type checker floats + universal quantifiers outside and maintains types in prenex form. + (However, quantifiers can, of course, not float out of negative + positions.) Overall, we have +

+sigma -> forall tyvars. phi
+phi   -> theta => rho
+rho   -> sigma -> rho
+       | tau
+tau   -> tyvar
+       | tycon tau_1 .. tau_n
+       | tau_1 tau_2
+       | tau_1 -> tau_2

+ where sigma is in prenex form; i.e., there is never a + forall to the right of an arrow in a phi type. Moreover, a + type of the form tau never contains a quantifier (which + includes arguments to type constructors). +

+ Of particular interest are the variants SourceTy and + NoteTy of TypeRep.Type. + The constructor SourceTy :: SourceType -> Type represents a + type constraint; that is, a predicate over types represented by a + dictionary. The type checker treats a SourceTy as opaque, + but during the translation to core it will be expanded into its concrete + representation (i.e., a dictionary type) by the function Type.sourceTypeRep. + Note that newtypes are not covered by SourceTypes anymore, + even if some comments in GHC still suggest this. Instead, all newtype + applications are initially represented as a NewTcApp, until + they are eliminated by calls to Type.newTypeRep. +

+ The NoteTy constructor is used to add non-essential + information to a type term. Such information has the type + TypeRep.TyNote and is either the set of free type variables + of the annotated expression or the unexpanded version of a type synonym. + Free variables sets are cached as notes to save the overhead of + repeatedly computing the same set for a given term. Unexpanded type + synonyms are useful for generating comprehensible error messages, but + have no influence on the process of type checking. +

Type Checking Environment

During type checking, GHC maintains a type environment whose - details are fixed in TcEnv.lhs. + type definitions are fixed in the module TcRnTypes with the operations defined in +TcEnv. Among other things, the environment contains all imported and local instances as well as a list of global entities (imported and local types and classes together with imported identifiers) and local entities (locally defined identifiers). This environment - is threaded through the type checking monad. + is threaded through the type checking monad, whose support functions + including initialisation can be found in the module TcRnMonad.

Expressions

Expressions are type checked by TcExpr.lhs. + href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcExpr.lhs">TcExpr.

Usage occurences of identifiers are processed by the function tcId whose main purpose is to instantiate @@ -130,7 +208,7 @@

-Last modified: Tue Nov 13 14:28:44 EST 2001 +Last modified: Sat Sep 13 23:35:24 BST 2003 diff --git a/ghc/docs/comm/the-beast/vars.html b/ghc/docs/comm/the-beast/vars.html index c2c1ce0..9bbd310 100644 --- a/ghc/docs/comm/the-beast/vars.html +++ b/ghc/docs/comm/the-beast/vars.html @@ -73,21 +73,28 @@ data VarDetails | TyVar | MutTyVar (IORef (Maybe Type)) -- Used during unification; - Bool -- True <=> this is a type signature variable, which - -- should not be unified with a non-tyvar type + TyVarDetails

Type variables (`TyVar`)

-The TyVar case is self-explanatory. The -MutTyVar case is used only during type checking. Then a -type variable can be unified, using an imperative update, with a type, -and that is what the IORef is for. The Bool -field records whether the type variable arose from a type signature, -in which case it should not be unified with a type (only with another -type variable). +The TyVar case is self-explanatory. The MutTyVar +case is used only during type checking. Then a type variable can be unified, +using an imperative update, with a type, and that is what the +IORef is for. The TcType.TyVarDetails field records +the sort of type variable we are dealing with. It is defined as +

+data TyVarDetails = SigTv | ClsTv | InstTv | VanillaTv
+

+SigTv marks type variables that were introduced when +instantiating a type signature prior to matching it against the inferred type +of a definition. The variants ClsTv and InstTv mark +scoped type variables introduced by class and instance heads, respectively. +These first three sorts of type variables are skolem variables (tested by the +predicate isSkolemTyVar); i.e., they must not be +instantiated. All other type variables are marked as VanillaTv.

For a long time I tried to keep mutable Vars statically type-distinct from immutable Vars, but I've finally given up. It's just too painful. @@ -220,7 +227,7 @@ not the same as whether the Id has an ExternaName or an Inter -Last modified: Tue Nov 13 14:11:35 EST 2001 +Last modified: Fri Sep 12 15:17:18 BST 2003 -- 1.7.10.4