Question

Explain the type checking of function with example

Answer 1

The purpose of types

To define what the program should do.

e.g. read an array of integers and return a double

To guarantee that the program is meaningful.

that it does not add a string to an integer

that variables are declared before they are used

To document the programmer's intentions.

better than comments, which are not checked by the compiler

To optimize the use of hardware.

reserve the minimal amount of memory, but not more

use the most appropriate machine instructions

What belongs to type checking

Depending on language, the type checker can prevent

application of a function to wrong number of arguments,

application of integer functions to floats,

use of undeclared variables in expressions,

functions that do not return values,

division by zero

array indices out of bounds,

nonterminating recursion,

sorting algorithms that don't sort...

Languages differ greatly in how strict their static semantics is: none of the things above is checked by all programming languages!

In general, the more there is static checking in the compiler, the less need there is for manual debugging.

Description formats for different compiler phases

These formats are independent of implementation language.

Lexer: regular expressions

Parser: BNF grammars

Type checker: typing rules

Interpreter: operational semantic rules

Code generator: compilation schemes

Typing judgements and rules

Typing rules concern judgements of the form

E => e : T

where E is an environment, which contains e.g. typings of identifiers. The judgement says

in the environment E, expression e has type T

Judgements are used in typing rules of the form

J1 J2 ... Jn --------------- C J

(n >= 0) which says

from the judgements J1, J2, ..., Jn you may conclude J, if condition C holds.

The judgements above the line in a rule are the premisses.

The judgement under the line is the conclusion.

The condition C beside is a side condition, typically not expressible as a judgement, therefore not a premiss.

The judgement are written in a formal language, whereas side conditions can be written in natural language.

Examples of typing rules and derivation

Typing rules for arithmetic expressions

E => e1 : int E => e2 : int E => e1 : int E => e2 : int ------------------------------- ------------------------------- E => e1 + e2 : int E => e1 * e2 : int ---------- x : T is in E ------------ i is an integer literal E => x : T E => i : int

Derivation of judgement x : int, y : int => x + 12 * y : int

x:int, y:int => 12 : int x:int, y:int => y : int --------------------------------------------------- x:int, y:int => x : int x:int, y:int => 12 * y : int -----------------------------------------------------------