Changes between Version 3 and Version 4 of IntermediateTypes

Timestamp:

08/04/06 05:44:59 (7 years ago)

Author:

guest

Comment:

--

IntermediateTypes

@@ -8 +8 @@
 
 Most of the system is fairly standard, with the exception of
-coercions.  A coercion c, is a type-level term, with a kind of the
-form T1 :=: T2. (c :: T1 :=: T2) is a proof that a term of type T1
-can be coerced to type T2.  It is used as argument of a cast
-expression; if t :: T1 then (t `cast` c) :: T2.
-
+coercions.  A coercion `c`, is a type-level term, with a kind of the
+form `T1 :=: T2`. (`c :: T1 :=: T2`) is a proof that a term of type `T1`
+can be coerced to type `T2`.  It is used as argument of a cast
+expression; if `t :: T1` then {{{(t `cast` c) :: T2}}}.  
+
+= What's New? =
+
+If you are already familiar with the intermediate language and its type system as it existed in 6.4.2 (and probably before) then
+the key aspects that have changed are (and are further described in several sections below):
+
+ * Coercions have been added - The syntax of types now includes coercions which are evidence for type equalities.  There are distinguished coercion variables and a new variant of `TyCon`, with constructor `CoercionTyCon`.  There is also a new `Expr` variant, with constructor `Cast`, which performs a cast given an expression and evidence of the safety of the cast.
+
+ * Kinds are now Types - The type Kind is just a synonym for Type.  There are special PrimitiveTyCons that represent kinds.
+
+ * Newtypes are implemented with coercions - The previous ad-hoc mechanism has been replaced with one that uses coercions.
+
+ * GADTs are implemented with coercions - The complex typing rules for case expressions on GADTs have been removed and instead the data constructors of GADTs carry coercions inside them.  Consequently, typechecking Core is simpler (though type inference is just as hard as ever).
+
+For anyone not familiar with the system as it existed previously, the rest of this note attempts to describe most of the type system of the intermediate language.
 
 == Types ==
 
-The representation of types is defined (as the datatype Type) in
+The representation of types is defined (as the datatype `Type`) in
 !TypeRep, and most of the useful functions on types are defined in
 Type.  TypeRep exports the representation concretely, and should