強類型

维基百科，自由的百科全书

在電腦科學以及程式設計中，術語強類型用以描述程式語言對於混入不同資料類型的值，這方面的運算限制中所處的地位。它的反義詞是弱類型。然而，這些術語在短短的電腦歷史中，早已含括了更多的意義，而且時常很難知道寫的人究竟要表達哪個意思。

[编辑] 解釋

程式語言專家 Benjamin C. Pierce，Types and Programming Languages 和 Advanced Types and Programming Languages 的作者，曾說︰

「我花了幾個星期…試著弄清楚「強類型」、「靜態類型」、「安全」等術語，但我發現這異常的困難…這些術語的用法不盡相同，所以也就近乎無用。」^[1]

大致而言，「強類型」隱含著程式語言對容許混合情況出現加上了嚴格的限制，以避免程式碼以無效的資料使用方式編譯或執行。例如，整數除法運算不可用於字串；鏈表上的運算步驟不可用於數字。然而，這些限制的本質和效力是極易改變的。

[编辑] 強類型在文獻中的含義

Some of the factors which writers have qualified as "strong typing" include:

靜態類型不同於動態類型。在靜態類型系統中，類型是與變數相連繫的名稱（通常是在宣告時），而不是值（通常是在建立時）。類型也可籍由編譯器來推斷。
The mandatory requirement, by a language definition, of compile-time checks for type constraint violations. That is, the compiler ensures that operations only occur on operand types that are valid for the operation.
Type safety; that is, the rejection (at either compile or run time) of operations or function calls which attempt to disregard data types. In a more rigorous setting, type safety is proved about a formal language by proving progress and preservation.
禁止類型轉換。某個類型的值，不論是不是以顯式或隱式的方式，都不可轉換為另一個類型。
Some authors, however, reserve the phrase "strongly-typed language" for languages that omit implicit type conversion (that is, conversions that are inserted by the compiler on the programmer's behalf). For these authors, a programming language is strongly typed if types must be converted by an explicit notation, often called a cast.
無法規避類型系統。某些語言允許程式員取得值的表示法之下的東西（即，位元組合），這有可能規避類型系統。
A complex, fine-grained type system with compound types.
資料物件中固定且不變的類型。The type of a given data object does not vary over that object's lifetime. Class instances, for example, may not have their class altered.
在執行程式之前，強類型就保證了執行時期的程式行為，其以靜態分析或其它的機制提供。

[编辑] 程式語言中的含義變異

Note that some of these definitions are contradictory, while others are merely orthogonal. Because of the wide divergence among these definitions, it is possible to defend claims about most programming languages that they are either strongly- or weakly-typed. For instance:

Java, Pascal and C require all variables to have a defined type and support the use of explicit casts of arithmetic values to other arithmetic types. Java and Pascal are often said to be more strongly typed than C, a claim that is probably based on the fact that C supports more kinds of implicit conversions than Pascal and C also allows pointer values to be explicitly cast while Java & Pascal do not. Java itself may be considered more strongly typed than Pascal as manners of evading the static type system in Java are controlled by the Java Virtual Machine's dynamic type system.
OCaml or Haskell have purely static type systems, in which the compiler automatically infers a precise type for all values. Both languages are considered to have stronger type systems than Java, as they permit no type conversions at runtime. While OCaml's libraries allow one form of evasion (Object magic), this feature remains unused in most applications.
Common Lisp has a complex, fine-grained system of data types, but is almost entirely dynamically typed.
Visual Basic is a hybrid language. In addition to including statically typed variables, it includes a "Variant" data type that can store data of any type. Its implicit casts are fairly liberal where, for example, one can sum string variants and pass the result into an integer literal.

For this reason, writers who wish to write unambiguously about type systems often eschew the term "strong typing" in favor of specific expressions such as "static typing" or "type safety".