\startdesc{Variable reference}
\defref{variable reference}
\startlambda
- x
+ x :: T
\stoplambda
This is a reference to a binder. It's written down as the
- name of the binder that is being referred to, which should of course be
- bound in a containing scope (including top level scope, so a reference
- to a top level function is also a variable reference). Additionally,
- constructors from algebraic datatypes also become variable references.
+ name of the binder that is being referred to along with its type. The
+ binder name should of course be bound in a containing scope (including
+ top level scope, so a reference to a top level function is also a
+ variable reference). Additionally, constructors from algebraic datatypes
+ also become variable references.
The value of this expression is the value bound to the given binder.
- Each binder also carries around its type, but this is usually not shown
- in the Core expressions. Occasionally, the type of an entire expression
- or function is shown for clarity, but this is only informational. In
- practice, the type of an expression is easily determined from the
- structure of the expression and the types of the binders and occasional
- cast expressions. This minimize the amount of bookkeeping needed to keep
- the typing consistent.
+ Each binder also carries around its type (explicitly shown above), but
+ this is usually not shown in the Core expressions. Only when the type is
+ relevant (when a new binder is introduced, for example) will it be
+ shown. In other cases, the binder is either not relevant, or easily
+ derived from the context of the expression. \todo{Ref sidenote on type
+ annotations}
\stopdesc
\startdesc{Literal}
\startdesc{Cast expression}
\defref{cast expression}
\startlambda
- body :: targettype
+ 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
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 this paragraph}
+ \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
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
+ 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
+ show @Bool \$dShow True
\stoplambda
\stopdesc
here)}.
\section[sec:prototype:statetype]{State annotations in Haskell}
+ As noted in \in{section}[sec:description:stateann], Cλash needs some
+ way to let the programmer explicitly specify which of a function's
+ arguments and which part of a function's result represent the
+ function's state.
\fxnote{This entire section on state annotations should be reviewed}
Ideal: Type synonyms, since there is no additional code overhead for
checking usage constraints on state variables.
\todo{Implementation issues: Separate compilation, simplified core.}
+
+% vim: set sw=2 sts=2 expandtab:
projects / matthijs / master-project / report.git / blobdiff