Soundness and Completeness of type system [tt-000S]

1. 我們說型別系統 sound 的時候，意思是如果一隻程式的型別不正確，系統就不會接受這隻程式。這蘊含了如果程式被系統接受 (type-checked)，那就一定是沒有類型錯誤的程式。

2. 我們說型別系統 complete 的時候，意思是如果一隻程式的型別正確，就一定會被系統接受。

我們通常更偏好滿足 soundness，因為有型別錯誤卻被接受的程式，因為比起有幾個需要改寫幾隻程式的麻煩，unsound 往往能造成更大的問題。