wiki:Language/Core/Expressions

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 ) = 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
letregion 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 )