+ Here, there is only a single alternative (but no \lam{DEFAULT}
+ alternative, since the single alternative is already exhaustive). When
+ it's body is evaluated, the arguments to the tuple constructor \lam{(,)}
+ (\eg, the elements of the tuple) are bound to \lam{a} and \lam{b}.
+ \stopdesc
+
+ \startdesc{Cast expression}
+ \defref{cast expression}
+ \startlambda
+ body ▶ targettype
+ \stoplambda
+ A cast expression allows you to change the type of an expression to an
+ equivalent type. Note that this is not meant to do any actual work, like
+ conversion of data from one format to another, or force a complete type
+ change. Instead, it is meant to change between different representations
+ of the same type, \eg switch between types that are provably equal (but
+ look different).
+
+ In our hardware descriptions, we typically see casts to change between a
+ Haskell newtype and its contained type, since those are effectively
+ different types (so a cast is needed) with the same representation (but
+ no work is done by the cast).
+
+ More complex are types that are proven to be equal by the typechecker,
+ but look different at first glance. To ensure that, once the typechecker
+ has proven equality, this information sticks around, explicit casts are
+ added. In our notation we only write the target type, but in reality a
+ cast expressions carries around a \emph{coercion}, which can be seen as a
+ proof of equality. \todo{Example}
+
+ The value of a cast is the value of its body, unchanged. The type of this
+ value is equal to the target type, not the type of its body.
+
+ \todo{Move and update this paragraph}
+ Note that this syntax is also used sometimes to indicate that a particular
+ expression has a particular type, even when no cast expression is
+ involved. This is then purely informational, since the only elements that
+ are explicitely typed in the Core language are the binder references and
+ cast expressions, the types of all other elements are determined at
+ runtime.
+ \stopdesc
+
+ \startdesc{Note}
+ The Core language in \small{GHC} allows adding \emph{notes}, which serve
+ as hints to the inliner or add custom (string) annotations to a core
+ expression. These shouldn't be generated normally, so these are not
+ handled in any way in the prototype.
+ \stopdesc
+
+ \startdesc{Type}
+ \defref{type expression}
+ \startlambda
+ @type
+ \stoplambda
+ It is possibly to use a Core type as a Core expression. For the actual
+ types supported by Core, see \in{section}[sec:prototype:coretypes]. This
+ \quote{lifting} of a type into the value domain is done to allow for
+ type abstractions and applications to be handled as normal lambda
+ abstractions and applications above. This means that a type expression
+ in Core can only ever occur in the argument position of an application,
+ and only if the type of the function that is applied to expects a type
+ as the first argument. This happens for all polymorphic functions, for
+ example, the \lam{fst} function:
+
+ \startlambda
+ fst :: \forall a. \forall b. (a, b) -> a
+ fst = λtup.case tup of (,) a b -> a
+
+ fstint :: (Int, Int) -> Int
+ fstint = λa.λb.fst @Int @Int a b
+ \stoplambda
+
+ The type of \lam{fst} has two universally quantified type variables. When
+ \lam{fst} is applied in \lam{fstint}, it is first applied to two types.
+ (which are substitued for \lam{a} and \lam{b} in the type of \lam{fst}, so
+ the type of \lam{fst} actual type of arguments and result can be found:
+ \lam{fst @Int @Int :: (Int, Int) -> Int}).
+ \stopdesc
+
+ \subsection[sec:prototype:coretypes]{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, \small{GADT}s, 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
+ t
+ \stoplambda
+
+ This is a reference to a type defined elsewhere. This can either be a
+ polymorphic type (like the latter two \lam{t}'s in \lam{id :: \forall t.
+ t -> t}), or a type constructor (like \lam{Bool} in \lam{not :: Bool ->
+ Bool}). Like in Haskell, polymorphic type variables always
+ start with a lowercase letter, while type constructors always start
+ with an uppercase letter.
+
+ \todo{How to define (new) type constructors?}
+
+ A special case of a type constructor is the \emph{function type
+ constructor}, \lam{->}. This is a type constructor taking two arguments
+ (using application below). The function type constructor is commonly
+ written inline, so we write \lam{a -> b} when we really mean \lam{-> a
+ b}, the function type constructor applied to \lam{a} and \lam{b}.
+
+ Polymorphic type variables can only be defined by a lambda
+ abstraction, see the forall type below.
+ \stopdesc