From: Matthijs Kooijman Date: Thu, 12 Nov 2009 14:10:39 +0000 (+0100) Subject: Add a section on the Core type system. X-Git-Tag: final-thesis~153 X-Git-Url: https://git.stderr.nl/gitweb?a=commitdiff_plain;h=060fd977e54d940afbd80accbf49bfef8964dde9;p=matthijs%2Fmaster-project%2Freport.git Add a section on the Core type system. --- diff --git a/Chapters/Prototype.tex b/Chapters/Prototype.tex index 6795771..c17a41d 100644 --- 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