查看“︁型別安全”︁的源代码

{{noteTA|G1=IT
|1=zh:型別;zh-tw:型別;zh-cn:类型;}}{{Type systems}}
在[[電腦科學]]中，一部分[[程式語言]]具備'''型別安全'''（-{zh:中國大陸;zh-tw:中國大陸;zh-cn:中国台湾;}-用語習慣稱型別為-{zh:类型;zh-tw:类型;zh-cn:型别;}-；-{zh:稱資料為数据;zh-tw:稱資料為数据;zh-cn:依据上下文、意思、特定用语的不同，常称数据为资料;}-）的性質。這個術語在不同的社群中有不同的定義，特別是正規的[[型別理論]]上的定義遠遠強過大多數的程式員的理解，但對於使用[[型別系統]]的認知，皆旨在避免必然的錯誤形式，和不良的程式行為（稱為'''型別錯誤'''）。

类型错误（type error）是错误或不期望的程序行为，由不同数据类型的差别所引起，适用于程序的常量、变量、方法（函数），如把整型（int）当作了浮点型（float）。 

型別安全可以靜態方式實施，及早在編譯時期就捕捉到潛藏的錯誤；或者以動態方式，在執行時期關聯型別的資訊，並在必要時檢測即將發生的錯誤。型別安全是程式語言的性質，而不是程式所自有的。例如，有可能以型別不安全的語言，編寫出型別安全的程式。在此是以程式語言為主，而不討論以個人能力維護的型別安全。

某個行為之所以會被程式語言歸類為型別錯誤，通常是因為試圖對不適當型別的[[值 (電腦科學)|值]]進行運算。其分類的基本原則是：部分語言設計者和程式員的看法認為，如果所有運算不引起程式瓦解、安全上的瑕疵、或其它明顯故障，即為合理的，而不視之為一個錯誤；其他人則認為所有違背程式員意圖的，就是錯誤的，而且應該標上「不安全」。在靜態型別系統中，型別安全通常包含一個保證，所有[[運算式]]最終的值都是合理的靜態型別成員（比[[子型別]]和[[多態性]]所要求的還要更加精確細微）。

型別安全近似於所謂的記憶體安全（就是限制從記憶體的某處，將任意的位元組合複製到另一處的能力）。例如，某個語言的實作具有若干型別 <math>t</math>，假如存在若干適當長度的位元，且其不為 <math>t</math> 的正統成員。若該語言允許把那些資料複製到 <math>t</math> 型別的[[變數]]，那個語言就不是型別安全的，因為這些運算可將非 <math>t</math> 型別的值-{zh:指派;zh-tw:指派;zh-cn:赋;}-給該變數。反過來說，若該語言型別不安全的程度，最高只到允許將任意整數用作為指標，顯然它就不是記憶體安全的。

大部分的靜態型別語言，都提供了一定程度的型別安全，而且其嚴格性更勝於記憶體的安全性。因其型別系統強迫程式員以適當的[[抽象資料型別]]定義來使用，即使對記憶體安全或任何可能的災難而言，並不需如此嚴格的要求。

==定義==
[[Robin Milner]] 對於型別安全所喊出的口號：
:''「具備良好型別的程式從不出錯。」''
这一口號的涵义，取決於语言形式化語義的类别。在[[指称語義學]]裡，型別安全意謂着一個運算式的值具有良好型別τ，则表达式是一個属于τ的集合的真正的成員。

1994年，Andrew Wright 和 [[Matthias Felleisen]] 以[[操作語義學]]定義的公式描述：何謂現今的標準定義，以及對於型別安全的檢驗技術。根據上述方法，型別安全是以程式語言語義中的兩個性質所決定的：

;藏存性:程式中的'''良好型別這一性質'''，即使轉換了語言的法則（即，評價法則或約簡法則），也不會有所改變。
;進行性:具備良好型別的程式從不'''卡住'''，即從不進入一個使其無法進一步轉換的未知狀態。

這些性質不是無中生有的，而是和程式語言所描述出來的語義相連繫，而且各式各樣的語言存在著可以此基準來充實的廣大的空間。因為「型別良好」程式的概念已是靜態語義學的一部分，而「卡住」（或者「搞錯」）則是動態語義學方面的屬性。

==語言的型別安全性==
學術研究用途的玩具語言，常會提出型別安全方面的需求。另一方面，許多語言以人工方式所產生的型別安全，證實經常需要上千次的檢查。不過，某些語言，如[[Standard ML]]，其嚴格定義了語義，且 [[Java]] 也已提供型別安全{{Fact|time=2007-11-01T17:17:16Z|date=February 2007}}。其它語言如 [[Haskell]] 也被認為是型別安全。暫且不理會語言定義的性質，在[[執行時期]]發生的某些錯誤，應歸於實作時的缺陷，或是用了其它語言撰寫的程式庫；這種錯誤可能使給定的實作，在某些情況下的型別不再安全。

===型別安全語言的記憶體管理===
要實現完善的型別安全語言，它至少需要[[垃圾回收 (計算機科學)|垃圾回收]]或增加記憶體配置和解配置的限制（本節主要針對前者）。更明確地說，不允許[[懸置指標]]橫跨不同結構型別的存在。這有一技術上的原因：假定型別語言（如[[Pascal語言|Pascal]]要求分配的記憶體必須顯式釋放）。如果存在一個仍舊指向之前的記憶體位址的[[懸置指標]]，新的資料結構可能會分配到同一空間。例如，如果初始化一個指向整數區域資料結構的指標，但新物件的指標區域卻分配在整數的地方，然後指標區域可藉由改變整數區域的值簡單改變成任可東西（經由間接引用[[懸置指標]]）。因為當指標改變時，尚未指定將會發生什麼，所以這個語言就不是型別安全的。大部分型別安全的語言滿足使用垃圾回收實現記憶體的管理。

在允許[[指標算術]]的語言中，實作垃圾回收器是最好的，所以在型別不安全的語言或型別安全可能失效的語言中，如此實作回收器的程式庫是最好的。C 和 C++ 經常使用。

===型別安全與強型別===
在各種[[強型別]]的定義中，其往往成為型別安全的同義詞；然而，型別安全與[[動態型別]]並不互相排斥。也可將動態型別視為非常寬鬆的靜態型別語言，而且所有語法正確的程式皆具備良好型別；只要它的動態語義學能夠保證絕不會有程式「搞錯」，它就可以滿足上述定義，且可稱為型別安全。

==參閱==
*[[資料型別]]
*[[型別理論]]

==參考資料==
*[[Benjamin C. Pierce]], ''Types and Programming Languages,'' MIT Press, 2002. (ISBN 0-262-16209-1) [http://www.cis.upenn.edu/~bcpierce/tapl/]{{Wayback|url=http://www.cis.upenn.edu/~bcpierce/tapl/ |date=20070319234547 }}
*''Type Safe'' defined in the Portland Pattern Repository's Wiki [http://c2.com/cgi/wiki?TypeSafe]{{Wayback|url=http://c2.com/cgi/wiki?TypeSafe |date=20140401164414 }}
*Andrew K. Wright and [[Matthias Felleisen]], "A Syntactic Approach to Type Soundness," ''Information and Computation'' 115(1), pp. 38-94, 1994. [http://citeseer.ist.psu.edu/wright92syntactic.html]{{Wayback|url=http://citeseer.ist.psu.edu/wright92syntactic.html |date=20080726074305 }}
*Stavros Macrakis, "Safety and power", ''ACM SIGSOFT Software Engineering Notes'' '''7''':2:25 (April 1982)[http://portal.acm.org/citation.cfm?id=1005937.1005941 requires subscription]

[[Category:类型论]]
[[Category:計算機語言]]