2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
4 \section[TypeRep]{Type - friends' interface}
8 Type(..), TyNote(..), PredType(..), -- Representation visible to friends
10 Kind, ThetaType, RhoType, TauType, SigmaType, -- Synonyms
13 superKind, superBoxity, -- KX and BX respectively
14 boxedBoxity, unboxedBoxity, -- :: BX
16 typeCon, -- :: BX -> KX
17 boxedTypeKind, unboxedTypeKind, openTypeKind, -- :: KX
18 mkArrowKind, mkArrowKinds, -- :: KX -> KX -> KX
20 usageKindCon, -- :: KX
21 usageTypeKind, -- :: KX
22 usOnceTyCon, usManyTyCon, -- :: $
23 usOnce, usMany, -- :: $
28 #include "HsVersions.h"
36 import TyCon ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon )
37 import Class ( Class )
40 import PrelNames ( superKindName, superBoxityName, boxedConName,
41 unboxedConName, typeConName, openKindConName, funTyConName,
42 usageKindConName, usOnceTyConName, usManyTyConName
46 %************************************************************************
48 \subsection{Type Classifications}
50 %************************************************************************
54 *unboxed* iff its representation is other than a pointer
55 Unboxed types cannot instantiate a type variable.
56 Unboxed types are always unlifted.
58 *lifted* A type is lifted iff it has bottom as an element.
59 Closures always have lifted types: i.e. any
60 let-bound identifier in Core must have a lifted
61 type. Operationally, a lifted object is one that
63 (NOTE: previously "pointed").
65 *algebraic* A type with one or more constructors, whether declared
66 with "data" or "newtype".
67 An algebraic type is one that can be deconstructed
68 with a case expression.
69 *NOT* the same as lifted types, because we also
70 include unboxed tuples in this classification.
72 *data* A type declared with "data". Also boxed tuples.
74 *primitive* iff it is a built-in type that can't be expressed
77 Currently, all primitive types are unlifted, but that's not necessarily
78 the case. (E.g. Int could be primitive.)
80 Some primitive types are unboxed, such as Int#, whereas some are boxed
81 but unlifted (such as ByteArray#). The only primitive types that we
82 classify as algebraic are the unboxed tuples.
84 examples of type classifications:
86 Type primitive boxed lifted algebraic
87 -----------------------------------------------------------------------------
89 ByteArray# Yes Yes No No
90 (# a, b #) Yes No No Yes
91 ( a, b ) No Yes Yes Yes
94 %************************************************************************
96 \subsection{The data type}
98 %************************************************************************
102 type SuperKind = Type
105 type TyVarSubst = TyVarEnv Type
111 Type -- Function is *not* a TyConApp
114 | TyConApp -- Application of a TyCon
115 TyCon -- *Invariant* saturated appliations of FunTyCon and
116 -- synonyms have their own constructors, below.
117 [Type] -- Might not be saturated.
119 | FunTy -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
123 | ForAllTy -- A polymorphic type
127 | PredTy -- A Haskell predicate
130 | UsageTy -- A usage-annotated type
131 Type -- - Annotation of kind $ (i.e., usage annotation)
132 Type -- - Annotated type
134 | NoteTy -- A type with a note attached
136 Type -- The expanded version
139 = SynNote Type -- The unexpanded version of the type synonym; always a TyConApp
140 | FTVNote TyVarSet -- The free type variables of the noted expression
142 type ThetaType = [PredType]
145 type SigmaType = Type
148 INVARIANT: UsageTys are optional, but may *only* appear immediately
149 under a FunTy (either argument), or at top-level of a Type permitted
150 to be annotated (such as the type of an Id). NoteTys are transparent
151 for the purposes of this rule.
153 -------------------------------------
156 Consider these examples:
157 f :: (Eq a) => a -> Int
158 g :: (?x :: Int -> Int) => a -> Int
159 h :: (r\l) => {r} => {l::Int | r}
161 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
162 Predicates are represented inside GHC by PredType:
165 data PredType = Class Class [Type]
169 (We don't support TREX records yet, but the setup is designed
170 to expand to allow them.)
172 A Haskell qualified type, such as that for f,g,h above, is
174 * a FunTy for the double arrow
175 * with a PredTy as the function argument
177 The predicate really does turn into a real extra argument to the
178 function. If the argument has type (PredTy p) then the predicate p is
179 represented by evidence (a dictionary, for example, of type (predRepTy p).
182 %************************************************************************
186 %************************************************************************
190 kind :: KX = kind -> kind
192 | Type boxity -- (Type *) is printed as just *
193 -- (Type #) is printed as just #
195 | UsageKind -- Printed '$'; used for usage annotations
197 | OpenKind -- Can be boxed or unboxed
200 | kv -- A kind variable; *only* happens during kind checking
202 boxity :: BX = * -- Boxed
204 | bv -- A boxity variable; *only* happens during kind checking
206 There's a little subtyping at the kind level:
207 forall b. Type b <: OpenKind
209 That is, a type of kind (Type b) is OK in a context requiring an OpenKind
211 OpenKind, written '?', is used as the kind for certain type variables,
214 1. The universally quantified type variable(s) for special built-in
215 things like error :: forall (a::?). String -> a.
216 Here, the 'a' can be instantiated to a boxed or unboxed type.
218 2. Kind '?' is also used when the typechecker needs to create a fresh
219 type variable, one that may very well later be unified with a type.
220 For example, suppose f::a, and we see an application (f x). Then a
221 must be a function type, so we unify a with (b->c). But what kind
222 are b and c? They can be boxed or unboxed types, so we give them kind '?'.
224 When the type checker generalises over a bunch of type variables, it
225 makes any that still have kind '?' into kind '*'. So kind '?' is never
226 present in an inferred type.
229 ------------------------------------------
230 Define KX, the type of a kind
231 BX, the type of a boxity
234 superKind :: SuperKind -- KX, the type of all kinds
235 superKind = TyConApp (mkSuperKindCon superKindName) []
237 superBoxity :: SuperKind -- BX, the type of all boxities
238 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
241 ------------------------------------------
242 Define boxities: @*@ and @#@
245 boxedBoxity, unboxedBoxity :: Kind -- :: BX
246 boxedBoxity = TyConApp (mkKindCon boxedConName superBoxity) []
248 unboxedBoxity = TyConApp (mkKindCon unboxedConName superBoxity) []
251 ------------------------------------------
252 Define kinds: Type, Type *, Type #, OpenKind, and UsageKind
255 typeCon :: KindCon -- :: BX -> KX
256 typeCon = mkKindCon typeConName (superBoxity `FunTy` superKind)
258 boxedTypeKind, unboxedTypeKind, openTypeKind :: Kind -- Of superkind superKind
260 boxedTypeKind = TyConApp typeCon [boxedBoxity]
261 unboxedTypeKind = TyConApp typeCon [unboxedBoxity]
263 openKindCon = mkKindCon openKindConName superKind
264 openTypeKind = TyConApp openKindCon []
266 usageKindCon = mkKindCon usageKindConName superKind
267 usageTypeKind = TyConApp usageKindCon []
270 ------------------------------------------
274 mkArrowKind :: Kind -> Kind -> Kind
275 mkArrowKind k1 k2 = k1 `FunTy` k2
277 mkArrowKinds :: [Kind] -> Kind -> Kind
278 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
282 %************************************************************************
284 \subsection{Wired-in type constructors
286 %************************************************************************
288 We define a few wired-in type constructors here to avoid module knots
291 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [boxedTypeKind, boxedTypeKind] boxedTypeKind)
294 ------------------------------------------
295 Usage tycons @.@ and @!@
297 The usage tycons are of kind usageTypeKind (`$'). The types contain
298 no values, and are used purely for usage annotation.
301 usOnceTyCon = mkKindCon usOnceTyConName usageTypeKind
302 usOnce = TyConApp usOnceTyCon []
304 usManyTyCon = mkKindCon usManyTyConName usageTypeKind
305 usMany = TyConApp usManyTyCon []