milly/docs/operational_semantics.md

milly's semantics

We are going to define a desugared, restricted subset of milly called core for which we define an operational semantics. Afterwards a translation from the full syntax to the core is defined.

core

For now we ignore ground types and their terms.

Let us start by defining the core syntax:

t := t t                    (function application)
   | \x. t                  (lambda abstraction)
   | x                      (variable)
   | true                   (bool literal)
   | false                  (bool literal)
   | let v = t in t         (let expression)
   | (t_1, ..., t_n)        (tuple constructor)
   | #n t                   (tuple projection)
   | <alt: t>               (variant constructor)
   | match t                (case expression)
     {
       <alt_1: x_1> -> t_1
       ...
       <alt_n: x_n> -> t_n
     }

Values we consider:

v := \x. t           (Lambda function)
   | true            (bool value)
   | false           (bool value)
   | <alt: v>        (variant value)
   | (v_1, ..., v_n) (tuple value)

Types are:

type := bool                  (ground bool type)
      | type -> type          (function type)
      | <alt_1: type_1,       (variant type)
         ...,
         alt_n: type_n>
      | (type_1, ..., type_n) (product type)

Typing rules:

Rule T-True

true : bool

Rule T-False

false : bool

Rule T-Tuple

If t_1 : T_1, ..., t_n : T_n

(t_1, ..., t_n) : (T_1, ..., T_n)

Rule T-Proj

If t : (T_1, ..., T_n)

#k t : T_k