... | ... | @@ -295,11 +295,11 @@ In this section, we review the dynamic semantics of unlifted types. These are n |
|
|
|
|
|
**Case binding.** Given `case e of x1 -> e1`, where `e` is `Unlifted`, `e` is evaluated to whnf, and then the result is case-matched upon. (i.e. it is always as if it is a strict pattern match.)
|
|
|
|
|
|
**Let bindings.** Given `let x = e in e'`, where `x` is `Unlifted)`, this desugars to `let !x = e in e'` which desugars to `case e of !x -> e'`. Mutually recursive let bindings of unlifted variables are not allowed. Let bindings are evaluated bottom up (but see #10824).
|
|
|
**Let bindings.** Given `let x = e in e'`, where `x` is `Unlifted)`, this desugars to `let !x = e in e'` which desugars to `case e of x -> e'`. Mutually recursive let bindings of unlifted variables are not allowed. Let bindings are evaluated bottom up (but see #10824).
|
|
|
|
|
|
**Conditionals.** Given `if e then e1 else e2` where `e1` and `e2` are `Unlifted`, this desugars into the obvious case. (NB: this means `e1` and `e2` are not eagerly evaluated, as they would be for an `ifthenelse` function.)
|
|
|
|
|
|
**Constructors and function application.** Given `K e` where `e` is `Unlifted`, this desugars into `case e of !x -> K x`. NB: if `K` is in kind star, then this expression admits bottom!
|
|
|
**Constructors and function application.** Given `K e` where `e` is `Unlifted`, this desugars into `case e of x -> K x`. NB: if `K` is in kind star, then this expression admits bottom!
|
|
|
|
|
|
|
|
|
|
... | ... | |