Abstract Syntax¶

Names¶

Con   (c)   ⟶ (named constructors)
Var   (n)   ⟶ (named variables)

Types¶

Type (τ,k,σ)
        ::= TyCon                         (type constructors)
         |  Var                           (type variables)
         |  'λ' Var ':' Type '.' Type     (type abstraction)
         |  Type Type                     (type application)

TyCon   ::= Con                           (primitive type constructors)
         |  'Data' | 'Effect' | 'Region'  (basic kind constructors)
         |  '(→)'  | 'Unit'   | 'Void'    (basic data type constructors)
         |  'Read' | 'Write'  | 'Alloc'   (basic effect type constructors)
         |  '⋁' Type Nat                  (least upper bound of types)
         |  '⊥' Type                      (least element of a type)
         |  '∀' Type                      (universal quantification)

The basic kind constructors are Data, Effect and Region for the kind of data, effect and region type respectively. The function type constructor (→) is usally written infix in sugared presentations. The Unit type classifies a set of values with the single element (). The Void type classifies the empty set.

The ⋁ type constructor is used to express type sums, where ⊥ is an empty sum. Both are annotated with the kind of their result types.

The quantifier constructor ∀ is annotated with the kind of its result type.

Syntactic Sugar¶

t1 → t2       ≡ (→) t1 t2

t1 + t2       ≡ ⋁ k 2 t1 t2
t1 + t2 + t3  ≡ ⋁ k 3 t1 t2 t3

⊥             ≡ ⊥ k

∀ n : k. t    ≡ (∀ k) (λ n : k. t)

The function type constructor (→) is usually written infix.

When the kind is clear from context we use the infix (+) operator to express type sums.

When the kind is clear from context, the kind argument on (⊥) is elided.

Quantifiers that bind names are desugared to an application of the associated type constructor and a type abstraction. Representing the different quantifiers as constructors allows us to retain a single binding form for types.

Terms¶

Exp (e)
       ::= DaCon                                (data constructor)
        |  Var                                  (variable)

        |  'λ' Var ':' Type '.' Exp             (term abstraction)
        |  Exp Exp                              (term application)

        |  'Λ' Var ':' Type '.' Exp             (type abstraction)
        |  Exp Type                             (type application)

        |  'let'    Bind   'in' Exp             (let binding)
        |  'letrec' BindT+ 'in' Exp             (recursive let binding)

        |  'case'   Exp  'of' Alt+              (case matching)

        |  'private' Var 'with' Sig+ 'in' Exp   (region introduction)

        |  'extend'  Var
             'using' Var 'with' Sig+ 'in' Exp   (region extension)

        |  'weakeff' Type 'in' Exp              (effect weakening)
        |  'box' Exp                            (box a computation)
        |  'run' Exp                            (run a suspension)

DaCon  ::= '()'                                 (builtin unit data constructor)
        |   Con                                 (named data constructor)

Bind   ::= Var '=' Exp                          (binding)
BindT  ::= Var ':' Type '=' Exp                 (typed binding)
Sig    ::= Var ':' Type                         (type signature)

Alt    ::= Pat '→' Exp                          (case alternative)
Pat    ::= _ | DaCon Sig+                       (case pattern)

The syntax of constructors and variables, term abstraction and application, type abstraction and application, case-matching and let-binding is standard.

The private construct introduces a new region variable along with capabilities of the given signatures. Both the region variable and names of the capabilities are in scope in the body expression.