wiki:Language/Core/Expressions

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 ) = Exp
Exp1 Exp2 Exp3 = (Exp1 Exp2) Exp3
Exp [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). ... Exp
private Binder+ in Exp = private Binder+ with { } in Exp
extend 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 ')'
Last modified 7 months ago Last modified on Sep 6, 2016, 10:22:58 AM