Add a section on the Core type system.

diff --git a/Chapters/Prototype.tex b/Chapters/Prototype.tex
index 67957718b112c1c81899b79de79428a6165184ff..c17a41dfbaf7c6342ef91d9cff5ac11327bd4246 100644 (file)
--- a/Chapters/Prototype.tex
+++ b/Chapters/Prototype.tex
@@ -311,7 +311,11 @@
       \stoplambda
       This is the basic lambda abstraction, as it occurs in labmda calculus.
       It consists of a binder part and a body part.  A lambda abstraction
-      creates a function, that can be applied to an argument. 
+      creates a function, that can be applied to an argument. The binder is
+      usually a value binder, but it can also be a \emph{type binder} (or
+      \emph{type variable}). The latter case introduces a new polymorphic
+      variable, which can be used in types later on. See
+      \in{section}[sec:prototype:coretypes] for details.
      
       Note that the body of a lambda abstraction extends all the way to the
       end of the expression, or the closing bracket surrounding the lambda. In
@@ -502,8 +506,135 @@
       \lam{fst @Int @Int :: (Int, Int) -> Int}).
     \stopdesc
 
-    TODO: Core type system
+    \subsection{Core type system}
+      Whereas the expression syntax of Core is very simple, its type system is
+      a bit more complicated. It turns out it is harder to \quote{desugar}
+      Haskell's complex type system into something more simple. Most of the
+      type system is thus very similar to that of Haskell.
 
+      We will slightly limit our view on Core's type system, since the more
+      complicated parts of it are only meant to support Haskell's (or rather,
+      \GHC's) type extensions, such as existential types, type families and
+      other non-standard Haskell stuff which we don't (plan to) support.
+
+      In Core, every expression is typed. The translation to Core happens
+      after the typechecker, so types in Core are always correct as well
+      (though you could of course construct invalidly typed expressions).
+
+      Any type in core is one of the following:
+
+      \startdesc{A type variable}
+        \startlambda
+        a
+        \stoplambda
+
+        This is a reference to a type defined elsewhere. This can either be a
+        polymorphic type (like \hs{a} in \hs{id :: a -> a}), or a type
+        constructor (like \hs{Bool} in \hs{null :: [a] -> Bool}).
+
+        A special case of a type constructor is the \emph{function type
+        constructor}, \hs{->}. This is a type constructor taking two arguments
+        (using application below). The function type constructor is commonly
+        written inline, so we write \hs{a -> b} when we really mean \hs{-> a
+        b}, the function type constructor applied to a and b.
+
+        Polymorphic type variables can only be defined by a lambda
+        abstraction, see the forall type below.
+      \stopdesc
+
+      \startdesc{A type application}
+        \startlambda
+          Maybe Int
+        \stoplambda
+
+        This applies a some type to another type. This is particularly used to
+        apply type variables (type constructors) to their arguments.
+
+        As mentioned above, some type applications have special notation. In
+        particular, these are applications of the \emph{function type
+        constructor} and \emph{tuple type constructors}:
+        \starthaskell
+          foo :: a -> b
+          foo' :: -> a b
+          bar :: (a, b, c)
+          bar' :: (,,) a b c
+        \stophaskell
+      \stopdesc
+
+      \startdesc{The forall type}
+        \startlambda
+          id :: \forall a . a -> a
+        \stoplambda
+        The forall type introduces polymorphism. It is the only way to
+        introduce new type variables, which are completely unconstrained (Any
+        possible type can be assigned to it). Constraints can be added later
+        using predicate types, see below.
+
+        A forall type is always (and only) introduced by a type lambda
+        expression. For example, the Core translation of the
+        id function is:
+        \startlambda
+          id = λa.λx.x
+        \stoplambda
+
+        here, type type of the binder \lam{x} is \lam{a}, referring to the
+        binder in the topmost lambda.
+
+        When using a value with a forall type, the actual type
+        used must be applied first. For example haskell expression \hs{id
+        True} translates to the following Core:
+
+        \startlambda
+        id @Bool True
+        \stoplambda
+
+        Here, id is first applied to the type to work with. Note that the type
+        then changes from \lam{id :: \forall a . a -> a} to \lam{id @Bool ::
+        Bool -> Bool}. Note that the type variable \lam{a} has been
+        substituted with the actual type.
+      \stopdesc
+
+      \startdesc{Predicate type}
+        \startlambda
+          show :: \forall a. Show s => s -> String
+        \stoplambda
+       
+        TODO: Introduce type classes?
+
+        A predicate type introduces a constraint on a type variable introduced
+        by a forall type (or type lambda). In the example above, the type
+        variable \lam{a} can only contain types that are an \emph{instance} of
+        the \emph{type class} \lam{Show}.
+
+        There are other sorts of predicate types, used for the type families
+        extension, which we will not discuss here.
+
+        A predicate type is introduced by a lambda abstraction. Unlike with
+        the forall type, this is a value lambda abstraction, that must be
+        applied to a value. We call this value a \emph{dictionary}.
+
+        Without going into the implementation details, a dictionary can be
+        seen as a lookup table all the methods for a given (single) type class
+        instance. This means that all the dictionaries for the same type class
+        look the same (\eg contain methods with the same names). However,
+        dictionaries for different instances of the same class contain
+        different methods, of course.
+
+        A dictionary is introduced by \small{GHC} whenever it encounters an
+        instance declaration. This dictionary, as well as the binder
+        introduced by a lambda that introduces a dictionary, have the
+        predicate type as their type. These binders are usually named starting
+        with a \lam{\$}. Usually the name of the type concerned is not
+        reflected in the name of the dictionary, but the name of the type
+        class is. The Haskell expression \hs{show True} thus becomes:
+
+        \startlambda
+        show @Bool $dShow True
+        \stoplambda
+      \stopdesc
+
+      Using this set of types, all types in basic Haskell can be represented.
+        
   \section[sec:prototype:statetype]{State annotations in Haskell}
       Ideal: Type synonyms, since there is no additional code overhead for
       packing and unpacking. Downside: there is no explicit conversion in Core