Many texts are rejected by lexical analysis and parsing phases as incorrect programs.
Many languages, however, have well-formed criteria that cannot be met only by the approaches described thus far on type checking and advanced type checking. Static type-correctness, for example, or the requirement that pattern-matching or case statements be exhaustive are examples of these needs. Most of these qualities aren't context-free, which means they can't be tested by being a member of a context-free language. As a result, they are verified by a step that (theoretically) follows syntax analysis (though it may be interleaved with it). These tests might be performed separately or in conjunction with the actual translation (see Translation of Expressions).
Because the translator frequently uses or relies on type information, it's logical to mix type computation with the exact translation.
For simplicity, we'll suppose that type checking and associated checks are performed in a separate phase and that any information acquired by this phase is available in other stages.
Syntax of Programming Language
To demonstrate the fundamentals of type checking, we'll use a simple (and somewhat artificial) language. The language has recursive definitions and is a first-order functional language. The presented grammar is unclear, but it doesn't matter because we're working with abstract syntax, which has already handled such ambiguities.
A program is a set of function declarations in the example language.
No function may be defined more than once because they are all mutually recursive. Each function specifies the type of its output and the types and names of its parameters. There may not be any repeats in a function's parameter list. There are separate namespaces for functions and variables. An expression can be an integer constant, a variable name, a sum expression, a comparison, a conditional, a function call, or an expression with a local declaration in the body of a function.
Both booleans and integers are forbidden in comparison, while only integers are prohibited in addition.
Type-checking language example
Program → Funs
Funs → Fun
Funs → Fun Funs
Fun → TypeId ( TypeIds ) = Exp
TypeId → int id
TypeId → bool id
TypeIds → TypeId
TypeIds → TypeId, TypeIds
Exp → num
Exp → id
Exp → Exp + Exp
Exp → Exp = Exp
Exp → if Exp then Exp else Exp
Exp → id ( Exps )
Exp → let id = Exp in Exp
Exps → Exp
Exps → Exp , Exps
Function Declarations in Type Checking
When type-checking the body of a function, the types of its arguments are explicitly declared in the function declaration, and this information is utilized to generate a symbol table for variables. The function body type must match the declared result type.
In the symbol table for functions, ‘CheckFun’ has an inherited attribute that is handed down to the type check function for expressions.
CheckFun checks for internal issues with the TypeId and TypeIds functions and returns null. GetTypeId returns a pair of the declared type's name and type. CheckTypeIds creates a symbol table from the (name, type) pair and also checks for distinct names for arguments.
Type Checking of Function Declarations
The kinds of parameters are clearly declared in a function declaration.
This data is used to create a symbol table for variables, which is then used to type-check the function's body. The body's type must match the function's specified result type. The symbol table for functions is given down to the type check function for expressions as an inherited attribute of the type check function for functions, CheckFun. CheckFun does not return any data; it just checks for internal issues. CheckFun is depicted in the diagram, along with the TypeId and TypeIds functions that it employs.
GetTypeId simply returns a pair of the stated name and type, which CheckTypeIds uses to generate a symbol table. CheckTypeIds also looks to see whether all of the arguments have unique names. An empty symbol table is called an emptytable. Unbound is the result of looking up any name in the empty symbol table.
CheckFun(Fun, ftable) =
case Fun of
TypeId ( TypeIds ) = Exp
(x, t0) = GetTypeId(TypeId)
vtable = CheckTypeIds(TypeIds)
t1 = CheckExp(Exp, vtable, ftable)
if t0 ≠ t1
then error()
GetTypeId(TypeId) =
case TypeId of
int id
(name(id), int)
bool id
(name(id), bool)
CheckTypeIds(TypeIds) =
case TypeIds of
TypeId
(x, t) = GetTypeId(TypeId)
bind(emptytable, x, t)
TypeId , TypeIds
(x, t) = GetTypeId(TypeId)
vtable = CheckTypeIds(TypeIds)
if lookup(vtable, x) = unbound
then bind(vtable, x, t)
else error(); vtable
Type Checking a Program
If all functions are of type correct and no two definitions define the same function name, a program is considered correct. In addition, the ‘main’ function should take one integer input and return one integer value.
The symbol table is used to type check functions, then tied to their types.
There will be two functions acting over ‘Fun’ and two functions operating over ‘Funs’ since this requires two passes, the first to generate the symbol table and the second to validate function definitions from the built table.
The illustration in the preceding section shows one of the functions for ‘Funs’.
The ‘GetTypes’ auxiliary function returns the pair(name, type) of the defined function, which comprises type parameters and result type, and is returned by the other ‘GetFun’.
The ‘GetFuns’ method constructs the symbol table and checks for duplicate definitions for the syntactic category ‘Funs’, whereas the ‘CheckFuns’ function executes the CheckFun function for all functions. The main function is the ‘Checkprogram’ function.
A program is a collection of functions that is type-correct if all of the functions are type-correct. No two function definitions define the same function. Because all functions are mutually recursive, they must be type-checked using a symbol table that binds all functions to their type. This necessitates two runs over the list of functions: one to construct the symbol table and the other to validate the function definitions using this table. As a result, we'll need two functions that operate on Funs and two functions that operate on Fun. One of the latter, CheckFun, has already been spotted.
Our little example language's type checking is now complete.
CheckProgram(Program) =
case Program of
Funs
ftable = GetFuns(Funs)
CheckFuns(Funs, ftable)
GetFuns(Funs) =
case Funs of
Fun
(f, t) = GetFun(Fun)
bind(emptytable, f, t)
Fun Funs
(f, t) = GetFun(Fun)
ftable = GetFuns(Funs)
if lookup(ftable, f) = unbound
then bind(ftable, f, t)
else error(); ftable
GetFun(Fun) =
case Fun of
TypeId ( TypeIds ) = Exp
(f, t0) = GetTypeId(TypeId)
[t1, . . . , tn] = GetTypes(TypeIds)
(f,(t1, . . . , tn) → t0)
GetTypes(T ypeIds) =
case TypeIds of
TypeId
(x, t) = GetTypeId(TypeId)
[t]
TypeId TypeIds
(x1, t1) = GetTypeId(TypeId)
[t2, . . . , tn] = GetTypes(TypeIds)
[t1, t2, . . . , tn]
CheckFuns(Funs, ftable) =
case Funs of
Fun
CheckFun(Fun, ftable)
Fun Funs
CheckFun(Fun, ftable)
CheckFuns(Funs, ftable)
Frequently Asked Questions
What do you mean by type checking of function declarations?
When type verifying the body of a function, the types of its arguments are explicitly declared in the function declaration, and this information is utilised to generate a symbol table for variables. The function body type must match the defined result type.
What GetTypeId returns?
GetTypeId returns a pair of the declared type's name and type.
When a program is said to be correct on behalf of type checking?
If all functions are type accurate and no two definitions define the same function name, a program is considered to be correct, and the main should take one integer input and return one integer value.
What is an auxiliary function?
An auxiliary function is one that exists to assist another function in completing its task. Because many auxiliaries are designed to address specialised sub-problems, the choice of auxiliaries frequently dictates the simplicity of solutions.
By using which table functions are type-checked?
The symbol table is used to type check functions, which are then tied to their types.
Conclusion
In this article, we have discussed type-checking a Program and function declarations, a small example of language. With the help of that example, we have discussed the type checking of a program and function declarations.
306+ registered