\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
\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}
+ TODO: This section should be reviewed and expanded.
+
Ideal: Type synonyms, since there is no additional code overhead for
packing and unpacking. Downside: there is no explicit conversion in Core
either, so type synonyms tend to get lost in expressions (they can be
Implementation issues: state splitting, linking input to output state,
checking usage constraints on state variables.
- Implementation issues
- \subsection[sec:prototype:separate]{Separate compilation}
- - Simplified core?
-
- \section{Haskell language coverage and constraints}
- Recursion
- Builtin types
- Custom types (Sum types, product types)
- Function types / higher order expressions
+ TODO: Implementation issues
+ TODO: \subsection[sec:prototype:separate]{Separate compilation}
+ TODO: Simplified core?
projects / matthijs / master-project / report.git / blobdiff