# Expressions

Exp ::= Var | Con | Literal (applications) | Exp ExpArg+ (lambda abstractions) | '/\' '(' Binder ':' Type ')' '.' Exp | '\' '(' Binder ':' Type ')' '.' Exp (non-recursive and recursive let binding) | let LetBind in Exp | letrec '{' LetBindTyped;+ '}' in Exp (region introduction and region context) | private Binder+ with '{' Cap;* '}' in Exp | extend Type using Binder with '{' Cap;* '}' in Exp (case expression) | case Exp of '{' Alt;+ '}' (type casts) | weakeff '[' Type ']' in Exp | weakclo '{' Exp '}' in Exp | purify Wit in Exp | forget Wit in Exp | run Exp | box Exp ExpArg ::= Exp | '[' Type ']' | '{' Wit '}' LetBind ::= Binder '=' Exp | Binder ':' Type '=' Exp LetBindTyped ::= Binder ':' Type '=' Exp Cap ::= LetBindTyped | Type TypeSig ::= Var ':' Type Alt ::= Pat '->' Exp Pat ::= '_' | Literal | 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 square brackets, while witnesses used as arguments are wrapped in angle brackets.

Lambda abstractions have a binder, a type, and a body expression. The '/\' form is used for Spec binders, while '\' is used for both value and witness binders. The body expression must always have kind `Data`. For value functions, the parameter must also have kind `Data`. For spec and witness functions, the parameter can have any kind, but the body must be pure. If the abstraction binds a spec variable then the variable cannot already be in the environment.

The `let` expression binds a variable to the result of evaluating the body expression. The bound variable is not in scope in the body expression. The bound variable can have an optional type annotation. The type of the binding and body must have kind 'Data'. At runtime, the binding is reduced to a value before substituting the result into the body.

The `letrec` expression introduces some recursive bindings. All bound variables must have type annotations. The bound variables are in-scope in all bindings. The types of the bindings and body must have kind `Data`. The right of all bindings must be lambda abstractions.

The `private` expression introduces some private region variables, and capabilities on those regions. The region variables and capabilities are in-scope in the body expression. The body must have kind `Data`. The type of the body cannot contain the bound region variable.

The `extend` expression extends an existing region with a new subregion, and introduces capabilities for the subregion. The new region variable and capabilities are in-scope in the body expression. The body must have kind `Data`. The type of the body cannot contain the bound region variable.

The `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.

The `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 inferred effect of an expression. The witness must have kind `Purify e1` for some effect `e1`.

The `forget` expression strengthens (masks) the inferred closure of an expression. The witness must have kind `Emptify c1` for some closure `c1`.

The `run` expression runs a computation of type `S e a` for some effect `e` and data type `a`.

The `box` expression suspends the execution of its body expression, creating a suspension of type `S e a`, for some effect `e` and data type `a`.

## 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). ... Exp\(Binder1 Binder2 ... : Type). Exp= \(Binder1 : Type). \(Binder2 : Type). ... Expprivate Binder+ in Exp= private Binder+ with { } in Expextend Type using Binder in Exp= extend Type using 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 | 'Pure' | 'Empty' | '(' Type ')' AWit ::= Var | WCon | '(' Witness ')'