紅色區(qū)域外:well behaved (type soundness)
紅色區(qū)域內(nèi):ill behaved
如果所有程序都是灰的乱投,strongly typed
否則如果存在紅色的程序葵腹,weakly typed
編譯時排除紅色程序责鳍,statically typed
運(yùn)行時排除紅色程序,dynamically typed
所有程序都在黃框以外雀瓢,type safe
參考:《Type Systems》 Luca Cardelli - Microsoft Research
Trapped error: An execution error that immediately results in a fault.
Untrapped error: An execution error that does not immediately result in a fault.
Forbidden error: The occurrence of one of a predetermined class of execution errors;
Typically the improper application of an operation to a value, such as not(3).
Well behaved: A program fragment that will not produce forbidden errors at run time.
Strongly checked language: A language where no forbidden errors can occur at run time (depending on the definition of forbidden error).
Weakly checked language: A language that is statically checked but provides no clear guarantee of absence of execution errors.
Statically checked language: A language where good behavior is determined before execution.
Dynamically checked language: A language where good behavior is enforced during execution.
Type safety: The property stating that programs do not cause untrapped errors.
Explicitly typed language: A typed language where types are part of the syntax.
Implicitly typed language: A typed language where types are not part of the syntax.