Abstract syntax describes the structure of Olaf programs. Typing rules help us guarantee that our programs are well-typed and will not go wrong.

In this section we describe the typing rules for Olaf. We begin by providing definitions for contexts and forms that our typing judgements take. Finally we go through each term and detail how the types work to ensure correct operation.

Typing Contexts

We provide distinct typing contexts for both global (g) method declarations, and local (l) binders.

g := {} | g, (mref, m)
l := {} | l, (xref, t)

For both contexts, we will use the operation x \in xs to check if x occurs within xs.

Typing Judgements

Expressions and Constants

The judgement form for expressions is:

g;l |- e : t

which says that under contexts g and l the expression e will have type t.

Statements

The judgement form for statements is:

g;l |- s : t

which says that under contexts g and l the statement e will return something of type t.

Methods

The judgement form for methods is:

g |- m : mty

which says that under context g the method m will have type mty.

Programs

The judgement form for programs is:

g |- p

which says that under context g the program p will be well-typed.

Constants

We begin with the introduction rules for constants, expressions that are typed.

Int

---- [ Intro Int ]

g;l |- i : int

Strings

---- [ Intro String ]

g;l |- s : string

Booleans

---- [ Intro Bool True ]

g;l |- true : bool
---- [ Intro Bool False ]

g;l |- false : bool

Unit

---- [ Intro Unt ]

g;l |- unit : unit

Expressions

We now look at expressions that require some evidence for typing to work.

Variables

For both method and variable references, if the name points to a location in their respective contexts then then that reference will have that type pointed to.

(mref,mty) \in g

---- [ Method References ]

g;l |- mref : mty
(xref,t) \in j

---- [ Variable References ]

g;l |- xref : t

Operations

Boolean operations will produce a term of type bool. For not and other binary boolean operations, all operands must also be of type bool.

g;l |- a : bool

---- [ Not ]

g;l |- not(a) : bool

The rules for many binary operations are generic, we ensure that the type of operands match the return type of the operator itself.

g;l |- a : t
g;l |- b : t

---- [ Binary Operations ]

g;l |- bop(a,b) : t

For binary numerical operations, such as add, t will be int.

For comparison operations, the types of the operands must come from the specified set of allowed comparison types and each operand must have the same type. The type of comparison operations will be bool.

g;l |- a : t
g;l |- b : t
t \in {bool,int,string}

---- [ Comparison Operations ]

g;l |- cop(a,b) : bool

Casting

Casting is a unary operation with a twist. We provide an explicit annotation to tell us what the type of the expression being cast should be.

g;l |- a : t
t \in {bool,int,string}

---- [ Casting ]

g;l |- cast(t,a) : string

Memory access

Accessing a memory location will have type &t, where t can be any other type even a reference. The result of accessing that location will result in an expression of type t, the inner type.

g;l |- a : &t

---- [ Deferencing ]

g;l |- &e : a

Method Calls

We know that mref will point to a method type. We must ensure that all arguments in the call have types that correspond to the types in the method prototype. All being well, then the method call will return an expression of type t.

g;l |- mref : {t_{0},...,t_{n}} -> t
g;l |- e_{0} : t_{0}
...
g;l |- e_{n} : t_{n}

---- [ Method Call ]

g;l |- mref({e_{0},...,e_{n}})) : t

Statements

Statements are control structures for sequencing computations.

Leaf Statements

Leaf statements stop computation.

The statement stop ‘inherits’ the type of the value being returned.

---- [ Intro Stop ]

g;l |- stop : t

The statement return will return something of type t, if the expression e also has type t.

g;l |- e : t

---- [ Intro Return ]

g;l |- return e : t

Sequencing Statements

We can only print strings, and printing strings has no value. Thereby, we use the unit type.

g;l |- e : string

---- [ Print ]

g;l |- print e : unit

We can only mutate references (things of type &t) with expressions that are of type t. As with printing, mutating does not return a value.

g;l |- xref : &t
g;l |- e    :  t

---- [ Mutate ]

g;l |- xref = e : unit

Binders

We use binders to expand the local typing context with an expression,

For let-binding, we extend l with a name associated with the type t.

g;l,(xref,t) |- s : t_2

---- [ Let binding ]

g;l |- let xref : t = e; s : t_2

With variables, we extend the local typing context with a reference, which when evaluating statements, will represent an address in our heap.

g;l,(xref,&t) |- s : t_2

---- [ Var binding ]

g;l |- var xref : t = e; s : t_2

Although we appear to be binding e to xref, we are creating an instruction to insert the value v, produced from evaluating e, onto the heap. The binder xref contains the address of where v is stored.

Control Flow

Sequencing two statements must have the same type. The left operand may return early, and the right operand must return a value.

g;l |- s_1 : t
g;l |- s_2 : t

---- [ Sequence ]

g;l |- s_1; s_2 : t

Similarly to sequencing, both branches in a conditional may return early and must have the same type. Our conditions are boolean.

g;l |- c  : bool
g;l |- tt : t
g;l |- ff : t

---- [ Conditional ]

g;l |- if c { tt } else { ff } : t

Similar to conditionals, a while-loop’s body may return early and the condition must be boolean.

g;l |- c  : bool
g;l |- ss : t

---- [ While ]

g;l |- while c { ss } : t

Methods

Methods are a statement s that has been given a set of arguments of different types. These arguments must match the types in the method type provided, and the statement must return something of the return type t.

g, { (xref_{0}, t_{0}),..., (xref_{n}, t_{n})} |- s : t

---- [ Method ]

g |- (\{ xref_{0} : t_{0},..., xref_{n} : t_{n}} => s)
       : { t_0,..., t_n } -> t

Programs

Our programs can contain method declarations, that associate a name mref with a method body and type.

g |- m : mty

---- [ Method Declarations ]

g |- mref = m : mty

We can sequencing method declarations much like let-binders, extending the global declarations as required.

g             |- mref = m : mty
g, (mref,mty) |- p

---- [ Method Declarations]

g |- mref = m; p

The final method in a program (the main method) will have no arguments and return nothing i.e. the unit type.

g |- m : {} -> unit

---- [ Main Method]

g |- m