|Version 15 (modified by dreixel, 2 years ago) (diff)|
The data type Type and its friends
GHC compiles a typed programming language, and GHC's intermediate language is explicitly typed. So the data type that GHC uses to represent types is of central importance.
The single data type Type is used to represent
- Types (possibly of higher kind); e.g. [Int], Maybe
- Coercions; e.g. trans (sym g) h
- Kinds (which classify types and coercions); e.g. (* -> *), T :=: [Int]
- Sorts (which classify types); e.g. TY, CO
GHC's use of coercions and equality constraints is important enough to deserve its own page.
The module TypeRep exposes the representation becauese a few other modules (Type, TcType, Unify, etc) work directly on its representation. However, you should not lightly pattern-match on Type; it is meant to be an abstract type. Instead, try to use functions defined by Type, TcType etc.
Views of types
Even when considering only types (not kinds, sorts, coercions) you need to know that GHC uses a single data type for types, even though there are two different "views".
- The "typechecker view" (or "source view") regards the type as a Haskell type, complete with implicit parameters, class constraints, and the like. For example:
forall a. (Eq a, %x::Int) => a -> Int
- The "core view" regards the type as a Core-language type, where class and implicit parameter constraints are treated as function arguments:
forall a. Eq a -> Int -> a -> Int
These two "views" are supported by a family of functions operating over that view:
- compiler/types/TypeRep.lhs: here is where Type is defined.
- compiler/types/Type.lhs: core-view utility functions over Type.
- compiler/typecheck/TcType.lhs: source-view utility functions over Type.
The "view" functions are shallow, not deep---a view function just looks at the root of the tree representing the type. For example, part of the coreView function (compiler/types/Type.lhs) looks like this:
coreView :: Type -> Maybe Type coreView (PredTy p) = Just (predTypeRep p) coreView (NoteTy _ ty) = Just ty coreView other = Nothing
Notice that in the NoteTy case, coreView does not call itself. Now, clients of the view look like this:
splitFunTy_maybe :: Type -> Maybe (Type,Type) splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty' splitFunTy_maybe (FunTy t1 t2) = Just (t1,t2) splitFunTy_maybe other = Nothing
Notice the first line, which uses the view, and recurses when the view 'fires'. Since coreView is non-recursive, GHC will inline it, and the optimiser will ultimately produce something like:
splitFunTy_maybe :: Type -> Maybe (Type,Type) splitFunTy_maybe (PredTy p) = splitFunTy_maybe (predTypeRep p) splitFunTy_maybe (NoteTy _ ty) = splitFunTy_maybe ty splitFunTy_maybe (FunTy t1 t2) = Just (t1,t2) splitFunTy_maybe other = Nothing
The representation of Type
Here, then is the representation of types (see compiler/types/TypeRep.lhs for more details):
data Type = TyVarTy TyVar -- Type variable | AppTy Type Type -- Application | TyConApp TyCon [Type] -- Type constructor application | FunTy Type Type -- Arrow type | ForAllTy TyVar Type -- Polymorphic type | PredTy PredType -- Type constraint | NoteTy TyNote Type -- Annotation data PredType = ClassP Class [Type] -- Class predicate | IParam (IPName Name) Type -- Implicit parameter | EqPred Type Type -- Equality predicate (ty1 :=: ty2) data TyNote = FTVNote TyVarSet -- The free type variables of the noted expression
Invariant: if the head of a type application is a TyCon, GHC always uses the TyConApp constructor, not AppTy. This invariant is maintained internally by 'smart constructors'. A similar invariant applies to FunTy; TyConApp is never used with an arrow type.
Kinds are represented as types:
type Kind = Type
Basic kinds are now represented using type constructors, e.g. the kind * is represented as
liftedTypeKind :: Kind liftedTypeKind = TyConApp liftedTypeKindTyCon 
where liftedTypeKindTyCon is a built-in PrimTyCon. The arrow type constructor is used as the arrow kind constructor, e.g. the kind * -> * is represented internally as
FunTy liftedTypeKind liftedTypeKind
It's easy to extract the kind of a type, or the sort of a kind:
typeKind :: Type -> Kind
The "sort" of a kind is always one of the sorts: TY (for kinds that classify normal types) or CO (for kinds that classify coercion evidence). The coercion kind, T1 :=: T2, is represented by PredTy (EqPred T1 T2).
(You can edit this picture here.)
* is the kind of boxed values. Things like Int and Maybe Float have kind *. # is the kind of unboxed values. Things like Int# have kind #. (#) is the kind of unboxed tuples. Things like (# Int, Int #) have kind (#). ArgKind is the kind of things that can appear as arguments to functions. OpenKind is the kind of things that can appear as results of functions.
Type variables are represented by the TyVar constructor of the data type Var.
Type variables range over both types (possibly of higher kind) or coercions. You could tell the differnece between these two by taking the typeKind of the kind of the type variable, adn seeing if you have sort TY or CO, but for efficiency the TyVar keeps a boolean flag, and offes a function:
isCoercionVar :: TyVar -> Bool
GHC uses the following nomenclature for types:
- A type is unboxed iff its representation is other than a pointer. Unboxed types are also unlifted.
- A type is lifted iff it has bottom as an element. Closures always have lifted types: i.e. any let-bound identifier in Core must have a lifted type. Operationally, a lifted object is one that can be entered. Only lifted types may be unified with a type variable.
- A type declared with data. Also boxed tuples.
- An algebraic data type is a data type with one or more constructors, whether declared with data or newtype. An algebraic type is one that can be deconstructed with a case expression. "Algebraic" is NOT the same as "lifted", because unboxed tuples count as "algebraic".
- a type is primitive iff it is a built-in type that can't be expressed in Haskell. Currently, all primitive types are unlifted, but that's not necessarily the case. (E.g. Int could be primitive.)
Some primitive types are unboxed, such as Int#, whereas some are boxed but unlifted (such as ByteArray?#). The only primitive types that we classify as algebraic are the unboxed tuples.
Examples of type classifications:
|(# a, b #)||Yes||No||No||Yes|
|( a, b )||No||Yes||Yes||Yes|