類型安全

在計算機科學中，類型安全和類型健全是指一種編程語言阻止或防止類型錯誤的程度。類型安全有時也被認為是一種計算機語言設施的屬性；也就是說，有些設施是類型安全的，它們的使用不會導致類型錯誤，而同一語言中的其他設施可能是類型不安全的，使用它們的程序可能遇到類型錯誤。被某個編程語言歸類為類型錯誤的行為通常是那些試圖對不屬于適當數據類型的值進行操作而導致的行為，例如，在沒有定義如何處理這種情況時，將一個字符串添加到一個整數中。這種分類有一部分是基于觀點的。類型執行可以是靜態的，在編譯時捕捉潛在的錯誤，也可以是動態的，在運行時將類型信息與值相關聯，并在需要時查詢它們以檢測即將發生的錯誤，或者兩者的結合。動態類型執行通常允許程序運行，而在靜態執行下，這些程序是無效的。在靜態（編譯時）類型系統的背景下，類型安全通常包括（除其他外）保證任何表達式的最終值將是該表達式靜態類型的合法成員。精確的要求比這更微妙--例如，請參閱子類型和多態性的復雜情況。

直觀地說，類型健全性是由RobinMilner的精辟論述所概括的，即類型良好的程序不會出錯。換句話說，如果一個類型系統是健全的，那么該類型系統所接受的表達式必須評估為一個適當類型的值。如果一種語言中可以對數據進行的xxx操作是數據類型所認可的，那么這種語言就是類型安全的。然而，對于一個程序來說，良好的類型化或出錯的確切含義是其靜態和動態語義的屬性，這對于每一種編程語言來說都是特定的。因此，類型健全性的精確、正式的定義取決于用于指定語言的正式語義學的風格。

一個類型良好的程序永遠不會被卡住：每個表達式要么已經是一個值，要么可以以某種定義良好的方式被還原為一個值。換句話說，程序永遠不會進入不可能有進一步轉換的未定義狀態。保存（或主題還原）在每個評價步驟之后，每個表達式的類型保持不變（也就是說，它的類型被保存了）。在指稱語義學和結構性操作語義學方面，也發表了一些其他類型健全性的正式處理方法。

孤立地說，類型健全性是一個相對較弱的屬性，因為它基本上只是說明類型系統的規則是內部一致的，不能被顛覆。然而，在實踐中，編程語言被設計成良好的類型性也包含了其他更強的屬性，其中一些包括。防止非法操作。內存安全類型系統可以防止野生指針，否則就會出現一種類型對象的指針被當作另一種類型的指針。更復雜的類型系統，例如那些支持從屬類型的系統，可以檢測并拒絕越界訪問，防止潛在的緩沖區溢出。源于不同類型語義的邏輯錯誤。

一個類型系統可以為它們強制執行兩種不同類型的整數。類型安全和類型不安全的語言類型安全通常是學術編程語言研究中提出的任何玩具語言（即深奧的語言）的要求。另一方面，許多語言對于人類生成的類型安全證明來說太大了，因為它們經常需要檢查成千上萬的情況。盡管如此，一些語言如StandardML，它有嚴格定義的語義，已經被證明符合類型安全的一個定義。