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