-
類型檢查
鎖定
- 中文名
- 類型檢查
- 外文名
- type checking
- 領 域
- 計算機
- 分 類
- 動態檢查、靜態檢查
- 類型檢查規則
- 類型綜合、類型推導
- 方 法
- 一致化方法、替換方法
類型檢查數據類型
數據類型是程序設計語言中的一個重要概念。類型的引入有着如下基本動機：
（1）類型可幫助更好地理解和組織關於客觀對象的思想；
（2）類型系統可幫助瞭解和討論某些特殊類型的獨特性質；
（3）類型可幫助檢測錯誤，防止對象的不合適使用。
大多數程序設計語言都使用類型系統來分類數據並防止錯誤，程序中的類型信息一方面增加了程序的易讀性，另一方面也用於防止無意義的程序構造。
類型檢查數據類型分類及其類型檢查
程序設計語言從對類型的考慮大體可分為三類：
（1）無類型語言，如BCPL和Blsis，這類語言不考慮類型及類型檢查，其編程中最常見的錯誤是不可檢測操作符對錯誤類型操作數的作用；
（2）弱附類型語言，如Lisp。這類語言允許對程序附上部分類型信息，類型檢查是在程序運行過程中進行的，即所謂動態檢查或運行時檢查；
（3）強附類型語言，如Algol和PASCAL等，這類語言需對程序附上完全的類型信息，類型檢查是在程序運行前的編譯過程中完成的，即所謂靜態檢查或編譯時檢查，這是大多數傳統命令型語言所採用的方式。
[1]
類型檢查類型檢查的簡介
為了進行類型檢查，編譯器需要給源程序的侮一個組成部分賦予一個類型表達式。然後，編譯器要確定這些類型表達式是否滿足一組邏輯規則。這些規則稱為源語言的類型系統。
類型檢查具有發現程序中的錯誤的潛能。原則上，如果目標代碼在保存元素值的同時保存了元素類型的信息，那麼任何檢查都可以動態地進行。一個健全的類型系統可以消除對動態類型錯誤檢查的需要，因為它可以幫助人們靜態地確定這些錯誤不會在目標程序運行的時候發生。如果編譯器可以保證它接受的程序在運行時刻不會發生類型錯誤，那麼該語言的這個實現就被稱為強類型的。
除了用於編譯，類型檢查的思想還可以用於提高系統的安全性，使得人們安全地導人和執行軟件模塊。Java程序被編譯成為機器無關的字節碼，在字節碼中包含了有關字節碼中的運算的詳細類型信息。導入的代碼在被執行之前首先要進行類型檢查，以防止因疏忽造成的錯誤和惡意攻擊。
[2]
類型檢查類型檢查的分類
類型檢查可分為動態檢查(即運行時檢查)和靜態檢查(即編譯時檢查)。
類型檢查動態檢查
類型檢查最自然的方式是認為檢查發生在運行時，即當涉及到具體的數據值時，即動態類型檢查。動態檢查有着幾個缺陷：（1）增加了程序運行時間，影響了效率；（2）需要數據具有類型標誌；（3）錯誤發現太晚，不能防止運行錯的出現。
動態檢查的一個顯著優點是它提供了寬鬆、少限制的程序設計環境，這在交互式語言中是十分有用的；動態檢查允許對變量的後期約束，從而給予編程較大靈活性，還可以在引入某些新定義類型時，不需改變現行程序代碼,即具有動態多態性；動態檢查可允許更豐富的類型系統，特別地，易於將類型作為一階對象處理，可允許異質的結構類型，便於數組下標分析。
類型檢查靜態檢查
靜態檢查則可去除上述動態檢查的缺點，它通過對程序的靜態分析，檢查所有涉及值的使用的操作、調用和賦值，在程序運行前排除潛在的類型錯誤。靜態分析有利於錯誤的早時發現和代碼優化、效率提高，也防止了關於類型的運行出錯。
靜態檢查要求對程序的完全附類型，變量必須早期約束，從而沒有了動態方式所具有的靈活性，引入新的類型可能需對原程序的修改和重編譯；靜態檢查也必須要求類型系統是可判定的以保證終止性，從而使類型系統有較大限制，許多類型是不允許的。
[1]
類型檢查類型檢查規則
類型檢查規則有兩種形式：綜合和推導。
類型檢查類型綜合
類型綜合(type synthesis)根據子表達式的類型構造出表達式的類型。它要求名字先聲明再使用。表達式
的類型是根據
和
的類型定義的。一個典型的類型綜合規則具有如下形式：
if f的類型為
且x的類型為s
then 表達式f(x)的類型為t
這裏，f和x表示表達式，而
表示從s到t的函數。這個針對單參數函數的規則可以推廣到帶有多個參數的函數。只要稍做修改，上述規則就可以用於
，只需要把它看作一個函數應用add(
,，
)就可以了。
類型檢查類型推導
if f(x)是一個表達式，
then 對某些
和
， f的類型為
且x的類型為
類型檢查類型檢查方法
一致化方法和替換方法是類型檢查特別是對類屬類型進行處理的有力工具。
類型檢查一致化方法
類型一致化就是尋找兩個類型表達式的最一般的一致化符mgu(使兩個類型表達式一致的最小結構)。類型一致化有兩個目的：一是比較兩個類型是否一致；二是獲得表達式的結果類型。
一致化有如下功能：
(1)用於類型推導：程序語言中的每個表達式(由常量、變量、模式名通過各類算符構成的式子)都有一個可決定的類型，但是表達式的類型有的是通過直接聲明得到的(如常量、變量的類型)，有的則需要經過類型推導而得到。類型推導中對代表不確定類型的類型變量的賦值由一致化過程實現。
(2)用於比較：對類型環境中謂詞良類型的判別中是利用操作數的已有類型，再根據算符對操作數的類型要求，構造新的類型表達式進行一致化比較，如成功則謂詞為良類型。
例如：環境Env下表達式E1的類型為t，表達式E2的類型為power t，需判別謂詞
是否為良類型。如果
是良類型，則E1類型的冪類型應與E2的類型一致。用表達式E1的類型t構造新類型power t，然後與E2的類型power t進行一致化操作，如果一致化成功，則
是良類型。
類型檢查替換方法
類屬定義的常量或變量是從定義處開始的全程量，為了使其能夠被共享，每次對它進行不同的引用就有必要進行類型結構的複製，這在類型檢查器中由替換函數實現。替換保證了類屬類型重複引用的正確性。替換方法有如下功能：
(1)實現顯式規則：在實例化等情況下，以實在的類屬參數替換定義中給出的形式類屬參數。
(2)實現隱式規則：在對類屬類型變量標識的單獨引用中，以未經約束的類型變量替換定義中給出的形式類屬參數，以便獲得實在的參數類型。
