Version 10 (modified by benl, 8 years ago) (diff) |
---|

# Expressions

EXP ::= VAR | CON | LITERAL (applications) | EXP XARG (lambda abstractions) | \( BINDER : TYPE ) . EXP (non-recursive and recursive let binding) | let LETBIND in EXP | lazy LETBIND in EXP | letrec { LETBINDTYPED;+ } in EXP (region introduction and context) | letregion BINDER with { TYPESIG;* } in EXP | withregion VAR in EXP (case expression) | case EXP of { ALT;+ } (type casts) | weakeff [ TYPE ] EXP | weakclo [ TYPE ] EXP | purify < WITNESS > EXP | forget < WITNESS > EXP XARGS ::= EXP | [ TYPE ] | < WITNESS > LETBIND ::= BINDER = EXP | BINDER : TYPE = EXP LETBINDTYPED ::= BINDER : TYPE = EXP TYPESIG ::= VAR : TYPE ALT ::= PAT -> EXP PAT ::= UNDERSCORE | CON PATBIND+ PATBIND ::= BINDER | ( BINDER : TYPE )

Applications are between an expression and an argument. The argument may be another expression, a type or a witness. Types used as arguments are wrapped in braces, while witnesses used as arguments are wrapped in angle brackets.

Lambda abstractions have a binder, a type, and a body expression. The same syntax is used for value, type and witness functions. This also implies the type annotation can be in universe Spec or Kind. The body expression must always have kind `*`. If the type annotation is in the Comp universe it must have kind `*`. If the abstraction binds a type variable, this variable cannot already be present in the environment. If the type annotation is in the Spec or Witness universe the body expression must be pure.

A `let` expression contains a binder and a body expression. The bound variable can have an optional type annotation. The bound variable is not in scope in the body expression. At runtime, the binding is reduced to a value before substituting the result into the body.

A `lazy` expression is similar to a `let` expression except the binding must be pure and empty. At runtime the binding is substituted into the body without reducing it first.

A `letrec` expression contains some bindings and a body expression. All bound variables must have type annotations. The bound variables are in-scope in all bindings. The right of all bindings must be syntactic values.

A `letregion` expression contains a region variable binder, a set of witness types, and a body expression. The body must have kind `*`. The witness types can be any of ` Global r, Const r, Mutable r, Lazy r, Manifest r`. The region variable `r` must be the same as the binder. The set cannot contain both `Const r` and `Mutable r`, or both `Lazy r` and `Manifest r`. The type of the body cannot contain the bound region variable.

A `withregion` expression contains a region variable and a body expression. A `withregion` is used in the operational semantics and interpreter for the core language, but does not normally appear in source programs. It holds the region handle while terms using that region are evaluated.

A `case` expression expression contains a discriminant expression and a list of alternatives. The alternatives must be exhaustive.

The `weakeff` expression weakens the effect of an expression to that given by the first argument, which must be at least as big as the actual effect of the second argument. The `weakclo` expression is similar.

The `purify` expression strengthens (masks) the effect of an expression. The witness must have kind `(Pure e1` for some effect `e1`. This effect is masked from the inferred effect of the body.

The `forget` expression strengthens (masks) the closure of an expression. The witness must have kind `Empty c1` for some closure `c1`. This closure is masked from the inferred closure of the body.

### Sugar and Equilvalences

( EXP )= EXPEXP1 EXP2 EXP3= (EXP1 EXP2) EXP3EXP [ATYPE1] [ATYPE2] ... [ATYPEN]= EXP [:ATYPE1 ATYPE2 ... ATYPEN:]Note A EXP <AWIT1> <AWIT2> ... <AWITN>= EXP <:AWIT1 AWIT2 ... AWITN:>Note A \(BINDER1 BINDER2 ... : TYPE). EXP= \(BINDER1 : TYPE). \(BINDER2 : TYPE). ... EXPletregion BINDER in EXP= letregion BINDER with { } in EXP

Note A: In the type and witness application sugar, the types and witnesses in the lists must have the following syntax. This ensures there is no ambiguity between successive arguments.

ATYPE ::= VAR | CON | !0 | $0 | ( TYPE ) AWIT ::= VAR | WCON | ( WITNESS )