類型分析，個人理解就是（通過靜態分析技術）分析出代碼中，哪些地方只能是某種或某幾種數據類型，這是一種約束。

?

例如，給定一個程序:

其中，我們可以很直接地得到一些約束：

最後，經過簡化可以得到：

對於給定的變量類型，如果他們不符合這個約束，則說明，他們是不合法的。

那麽，怎麽去提取以及維護這些約束呢？

采用一種“並查集”的結構：一個有向圖，每個節點有一條邊指向父節點（父節點則指向自己）。如果兩個節點具有相同的父節點，那麽，這個兩節點就認為是等價的，即含有相同的數據類型。

以下是並查集的基本算法：

The unification algorithm uses union-find by associating a node with each term (including sub-terms) in the constraint system.

For each term τ we initially invoke MakeSet(τ ).

Note that each term at this point is either a type variable or a proper type (i.e. integer, heap pointer, or function); μ terms are only produced for presenting solutions to constraints, as explained below.

For each constraint τ1 = τ2 we invoke Unify(

Unification fails if attempting to unify two terms with different constructor (where function constructors are considered different if they have different arity).?

再來看個例子：

對於遞歸：

Limitations of the Type Analysis?

例子：

?

運行的時候沒問題，但是，遵循之前的方法會報錯，之前的方法並不考慮程序的順序執行給數據類型轉換的影響。即X=42在X=alloc之後，因此，最終返回的一定是int型。

另一個例子：

【Static Program Analysis - Chapter 3】Type Analysis