This removes the ambiguity between using :: for explicitly casting and for
showing the type of an expression.
let
-- Unpack the state by coercion (\eg, cast from
-- State (Word, Word) to (Word, Word))
let
-- Unpack the state by coercion (\eg, cast from
-- State (Word, Word) to (Word, Word))
-- Extract both registers from the state
r1 = case s of (a, b) -> a
r2 = case s of (a, b) -> b
-- Extract both registers from the state
r1 = case s of (a, b) -> a
r2 = case s of (a, b) -> b
s' = (,) r1' r2'
-- pack the state by coercion (\eg, cast from
-- (Word, Word) to State (Word, Word))
s' = (,) r1' r2'
-- pack the state by coercion (\eg, cast from
-- (Word, Word) to State (Word, Word))
- sp' = s' :: State (Word, Word)
+ sp' = s' ▶ State (Word, Word)
-- Pack our return value
res = (,) sp' out
in
-- Pack our return value
res = (,) sp' out
in
\italic{toplet} = letrec [\italic{binding}...] in var (representable(varvar))
\italic{binding} = var = \italic{rhs} (representable(rhs))
-- State packing and unpacking by coercion
\italic{toplet} = letrec [\italic{binding}...] in var (representable(varvar))
\italic{binding} = var = \italic{rhs} (representable(rhs))
-- State packing and unpacking by coercion
- | var0 = var1 :: State ty (lvar(var1))
- | var0 = var1 :: ty (var0 :: State ty) (lvar(var1))
+ | var0 = var1 ▶ State ty (lvar(var1))
+ | var0 = var1 ▶ ty (var0 :: State ty) (lvar(var1))
\italic{rhs} = userapp
| builtinapp
-- Extractor case
\italic{rhs} = userapp
| builtinapp
-- Extractor case
\startdesc{Cast expression}
\defref{cast expression}
\startlambda
\startdesc{Cast expression}
\defref{cast expression}
\startlambda
\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
\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.
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
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