|
|
| | |
|
|
|
Static vs. Dynamic Typing
has to do with what&when we type/type-check:
«In a dynamically typed language
most operations are type-checked just before they are performed.
In a statically typed language,
every expression of the language is assigned a type at compile time.
If the type system can ensure that the value of each expression
has a type compatible with the type of the expression [Ulf: type correctness],
then type checking can be moved to compile type »
[TyOOL].
|
|
|
|
|
specifies
|
|
| IN STATICALLY TYPED PL
| 
|
|
|
|
type (& effects) inference
«[E]very expression of the language is assigned a type
at compile time »
[TyOOL]
| 
|
|
|
|
static checking
The types assigned to expressions
determine which compositions of expressions are valid
|
|
|
| | STATIC GRAMMATICAL (val/exc/efx) TYPE
| |
-> Linguistics:
grammatical feature aka. distribution class
|
|
|
compatible?
(correctness of type inference)
|
|
prog. lang.
| STATICALLY TYPED PL
|
«Only program sources that comply with a type system should be considered
real programs of a typed language;
the other sources should be discarded before they are run »
[TS]
| 
| |
| STATIC TYPE SYSTEM
|
«A [static] type system
is that component of a [statically] typed language
that keeps track of variables and, in general,
of the types of all expression in a program »
[TS]
| |
|
|
For example, the Java spec:
«The type [of a variable or expression] limits the possible values
that the variable can hold or the expression can produce at run time.
If a run-time value is a reference that is not null,
it refers to an object or array that has a class ...
that will necessarily be compatible with the compile-time type » [GJS96].
|
|
«As soon as we start working in an untyped universe,
we begin to organize it in different ways for different purposes.
Types arise informally in any domain to categorize objects
according to their usage and behavior.
The classification of objects in terms of the purposes for which they are used
eventually results in a more or less well-defined type system.
Types arise naturally, even starting from untyped universes »
[UTDAP].
|
|
«[Static] Type systems
are used to determine whether programs are well behaved ... »
«The fundamental purpose of a [static] type system is to prevent
the occurence of execution errors during the running of a program »
[TS]
|
Formal statements of type correctness
(correctness of type inference / of static type system)
have the basic form
A |- e : t
/\ s |= A
/\ (e,s) ->* v
=> v  [[t]]
| A |- e : t | - formal typing rules assign to expression e the type term t under assumptions A
| s |= A | - state s satisfies assumptions A
| (e,s) ->* v | - e evaluates to value v in state s
| v [[t]]
| - v is in the extension (set of values) [[t]] of type term t
| | | |
|
|
|
| | |
|
