Week 4 我們主要介紹 type inference 和 module 系統。

What is type inference？

對於 靜態型別語言 (Statically typed languages) 如 ML，Java 與 C，每一個 binding 的型別是在編譯時確定的。type-checker 在編譯時決定是否要執行整個程式。與之不同的是動態型別語言 (Dynamically typed languages) 例如 Racket，Ruby 與 Python。
ML 語言又和其他靜態型別語言不同，它是 隱式型別的 (implicitly typed)，意味著編寫程式時我們很少需要直接宣告 bindings 的型別，type-checker 推斷出我們想要的型別。當某些函式的引數或者返回值可以是任何一種型別時，type-checker 會向它們分配多型類 'a, 'b, 'c... 這體現了 ML 語言型別推斷與引數化多型 (parametric polymorphism) 的融合。

Overview of the type inference

• It determines the types of bindings in order. 使用之前的 binding types 來推斷之後的 binding types
• 對於每個 fun val bindings, 分析一些 necessary fact 來決定 binding 的型別。例如，當我們發現表達 x+1 時，可以確認 x 一定是 int type。
• 對於任何 函式引數或是返回值中的 unconstrained types，分配多型型別 'a, 'b, 'c...
• 執行 value restriction
• 若不存在某一種 solution，不執行該程式並丟擲 type error
  、

關於 value restriction

當 可變型別 reference 與 多型類結合時，存在一種情況能夠破壞我們目前已知的 type inference 系統。

val r = ref NONE         (* a val binding : r has the type 'a option reference *)
val _ = r := SOME "hi"   (* type check operator := : instantiate (but do not change) 'a with string, type checked *)
val i = 1 + valOf (!r)   (* type check operator ! : 'a option reference => 'a option, type check func valOf : 'a option => 'a, instantiate 'a with int, type checked *)
(* though the above 3 lines all type checked, it use + to add a int and a string *)
 

為了解決這個問題，ML 採用了 value restriction 的方法：只有 val x = e 中的 e 是一個 value 或者是一個 valuable 時才有可能分配多型型別給 x。在上面的例子中，ref NONE 是一個函式呼叫，是需要計算的，不屬於 value 或 valuable，因此係統拒絕給 r 分配多型類，取而代之的是所謂的 "dummy type : ?X1 option ref" 而不是一個型別變數。dummy type 在接下來的語句中將不能 type check。
value restriction 的存在解決了以上這個問題，但同時也使得某些 partial application 與 currying 的結合無法實現。

Mutual recursion

使用 and 關鍵字來連結需要相互呼叫的函式。

Modules for namespace management

一個好的程式應當是模組化的。我們將所有的 bindings 按照其功能分成不同的類並歸於對應的 namespace module。這使得程式更加模組化並且能夠避免由於變數名稱相同引起的 shadowing。
我們用關鍵字 structure 來定義一個包含眾多 bindings 的 module。格式如下 structure ModuleName = struct bindings end
module 內部同樣遵循 lexical scope 等規則。在 module 外部需要呼叫內部的 binding b 時，使用 ModuleName.b 的形式。

Signatures

目前為止，structures 提供了 namespace management 的能力，這非常有用，但是本質上並沒有改變程式的功能。
如果我們賦予 structure 簽名 (signature, which are types for module)，可以對模組外部程式碼呼叫模組內部模組是提供嚴格的限制，也就是說，我們可以創造 structure 的介面 (interface)。
這對我們實現抽象化資料結構等功能十分有用。
如以下程式碼：

signature MATHLIB =
sig
val fact : int -> int
val half_pi : real
val doubler : int -> int
end
structure MyMathLib :> MATHLIB =
struct
fun fact x =
  if x=0
  then 1
  else x * fact (x - 1)
val half_pi = Math.pi / 2.0
fun doubler y = y + y
end

因為 :> MATHLIB, 只有當 structure MyMathLib 正確提供了 signature MATHLIB 中宣告的所有內容時才能 type check。MATHLIB 還可以宣告各種 datatype，exception 等內容。