Chapter 3  The Flow Caml language

Notations

3.1  Lexical conventions

    and         as          assert      asr         begin       class  
    closed      constraint  do          done        downto      else   
    end         exception   external    false       for         fun    
    function    functor     if          in          include     inherit
    land        lazy        let         lor         lsl         lsr    
    lxor        match       method      mod         module      mutable
    new         of          open        or          parser      private
    rec         sig         struct      then        to          true   
    try         type        val         virtual     when        while  
    with                                                               

    affects     content     finally     flow        greater     less   
    level       noneq       propagate   raise       raises      row    
    than                                                               

    #     &     '     (     )     *     ,     ->    ? 
    ??    .     ..    .(    .[    :     ::    :=    ; 
    ;;    <-    =     [     [|    [<    {<    ]     |]
    >]    >}    _     `     {     |     }     ~       

    -{    }->   ={    }=>

3.2  The core language

3.2.1  Values

3.2.2  Names

Naming objects

Referring to named objects

3.2.3  Security levels

• The inequalities between principals provided in flow declarations (see section 3.3.3),
• and the assumptions made in level definitions (see section 3.2.4).

3.2.4  Level definitions

• If a clause greater than security-level₁ , ... , security-level_n is provided, then the new level is made greater than or equal to security-level_i, for all i.
• If a clause less than security-level₁ , ... , security-level_n is provided, then the new level is made less than or equal to security-level_i, for all i.

3.2.5  Type expressions

3.2.6  Type schemes

• A simple constant level security-level stands for a fresh level variable 'a with the two constraints security-level < 'a and 'a < security-level.
• [< security-level₁ , ... , security-level_n] is a shorthand for a fresh level variable 'a with the constraint 'a < security-level₁ , ... , security-level_n. Similarly, [> security-level₁ , ... , security-level_n] is a shorthand for a fresh level variable 'a with the constraint security-level₁ , ... , security-level_n < 'a. Lastly, [< security-level₁ , ... , security-level_n |> security-level_{n+ 1} , ... , security-level_{n+ k}] is a shorthand for a fresh level variable 'a with the constraints security-level₁ , ... , security-level_n < 'a and 'a < security-level_{n+ 1} , ... , security-level_{n+ k}.
• _ stands for an anonymous fresh variable of any kind.
• On functions arrows, anonymous variables can be omitted. For instance, -{| typexpr₁ | typexpr₂ }-> is a shorthand for -{ 'a | typexpr₁ | typexpr₂ }-> where 'a is a fresh variable. Furthermore, an arrow whose three annotations are omitted, -{ | | | }->, can be written ->.

3.2.7  Type definitions

• The type representation = constr-decl <| constr-decl> [# ' ident] describes a variant type. The optional annotation [# ' ident] declares the security level attached to variant values. It must be one of the parameters of the type constructor and it is required if the variant type comprises several constructors.
• The type representation = { field-decl <; field-decl > } describes a record type. The optional annotation [# ' ident] declares the security level attached to records values. It must be one of the parameter of the type constructor and it is required if the record type comprises one or several mutable fields.

3.2.8  Exception definitions

3.2.9  Constants

3.2.10  Patterns

3.2.11  Expressions

Evaluation order

3.3  The module language

3.3.1  Module types (module specifications)

• A new for of specifications, level definitions, may appear in signatures.
• In Flow Caml signatures, exception declarations (introduced by the keyword exception) may mention an equality between exceptions (as in structures). This is made necessary because exceptions appears in types for values.
• Functors arrows may mention two lists of security levels, a pair of bounds whose purpose is explained in section 2.7.3 of the tutorial.

3.3.2  Module expressions (module implementations)

Evaluation order

3.3.3  Compilation units