這篇文章簡單地介紹了 haskell 怎麼做型別推導 (type inference)， 以及討論這中間會產生的議題，與我們怎麼處理或使用這些議題。

1. universal quantification 與 parametric polymorphism

在 Haskell 中，對一個 polymorphic typed function 例如

f :: a -> (a, [a])
f x = (x,[x])

我們可以合法地將不同的參數餵進去：

exp = (f 1, f "str")

這裡的重點是，pair 裡面左邊的 f 和右邊的 f 事實上具有不同型別。 要理解這裡這個情況是怎麼回事，關鍵的一點是要先了解： haskell 中，對每個沒被指明的 type variables 而言， 其最外面都有一個隱藏的 universal quantifier (\(\forall\))。

也就是說一個 type，以上面的 f 為例，事實上應該要寫成 f :: forall a. a -> (a, [a])。 因此， exp 可以看成是

exp = ( (f :: forall a. a -> (a, [a])) $ 1,
        (f :: forall a. a -> (a, [a])) $ "str")

而，因為這兩個 forall 是各自獨立的，所以 pair 的兩邊的 f 就會根據不同的參數而有了不同的型別：

exp = ( f 1     -- f :: Num t => t -> (t, [t]))
      , f "str" -- f :: String -> (String, [String]))
      )

這種由 “universal type variable” 所構造出來的 polymorphic function 就被稱為 parametric polymorphism。

2. type inference 與 generalization

haskell 推導 (infer) types 的過程簡易來說有兩步：

1. (Hindley–Milner) type inference - 推導出整個式子的 type signature。
2. generalization - 對所有 free variable 加上 universal quantifier。

這裡我們舉一個有助想像的實際例子：

h x =
    let f y = (x, y)
    in f x

首先，haskell 看到第 1 行的時候會想說「阿，這邊有個 x ，那先假裝它的 type 叫做 t 好了」。 也就是說 haskell 會在 context 裡面加上 x :: t 這筆資訊。 而一進入到第 2 行， haskell 會可以馬上 infer 出 f :: a -> (t, a)。 接著，haskell 會開始試圖對 f 做 generalization，也就是，試著對所有 f 的 type variables 加上 forall：

對 type variable a ：
顯然 a 是 free 的，所以要對 a 加上 forall。
對 type variable t ：
這裡的 t 不是 free 的，他已經在 context 裡面有出現了。

最終，haskell 會推導出 f :: forall a. a -> (t, a)。 接著，根據 f 的 type，我們可以輕易地進一步推導出 h :: forall t. t -> (t, t)。

3. Monomorphic type

就字面上直譯來說，monomorphic 就是相對於 polymorphic 的存在。 例如說 f1 :: forall a. a -> a 是 polymorphic， 而 f2 :: Int -> Int 則被稱為 monomorphic。

承接上面的例子。對 f 來說， t 沒有被 forall 綁住會造成一些容易被我們的影響。例如說我們改寫一下 h 的定義：

h x =
    let f y = (x, y)
    in (f 1, f False)

此時，整個 h 語法上還是合法的，也可以被正確編譯以及執行。但是，下面這段程式就不行了。

h x =
    let f y = [x, y]
    in (f 1, f False)

不行的原因其實相當簡單。前面是因為 x 和 y 是放在 pair 裡面，所以兩者之間的 types 會是各自獨立的，因此沒有問題。但是這裡的 x 和 y 是放在同一個 list 裡面，所以 x 和 y 的 type 必須要是同一個。也就是說，在 inference 的階段我們會得到 f :: t -> [t]。而這裡面出現的那個 t 會是 context 中已經有的，所以 t 不會被進一步 generalize (也就是說，對 f 而言 t 是沒有 forall 的)。那，t 的 forall 哪裡去了？事實上，它會是出現在 h 的 type signature 上面。這就表示，對整個 h 裡面來說，雖然我們可以任意選定一個 t 沒錯，但是在 h 的定義裡面的 t 都必須是同一個。這就好比說， cons 的 type 會是 (:) :: forall a. a -> [a] -> [a] ，但是我們只能寫 1 : [2] 而不能寫 '1' : [2]。

… TBC …

.

如果在 .hs 檔案中寫了

pie = sum $ take 1000000 $ zipWith (/) (iterate negate 4) [1,3..]

然後用 ghci 讀取進去以後詢問說 :t pie ，會發現說 pie :: Double，但是 :t sum $ take 1000000 $ zipWith (/) (iterate negate 4) [1,3..] 會得到 (Enum a, Fractional a) => a。

Defaulting: preset a type for deciding a class Num involved ambiguous type variable.

module GHC.Num (module GHC.Num, module GHC.Integer) where

-- skipped

default ()              
-- Double isn't available yet,
-- and we shouldn't be using defaults anyway

The monomorphism restriction states that a function with no explicit arguments, but with class constraints, must be given a type annotation.

f1 x = show x
f2 = \x -> show x
f4 = show

• f1 OK: 這是 function binding => unrestricted (apply no MR)
• f2, f4 BAD: 都是 (simple?) pattern binding => 不保證用的時候不會有 side effect, 所以要限制一下

MR, basically, it solves one practical problem (without the restriction, there would be some ambiguous types) and one semantic problem (without the restriction, there would be some repeated evaluation where a programmer might expect the evaluation to be shared).

For semantic problem,

genericLength :: Num a => [b] -> a

f xs = (len,len)
     where
       len = genericLength xs

len has type Num a => a, without MR, it will be computed twice in (len,len).

ambiguous type
=>
defaulting (Num only)
=>

The monomorphism restriction depends on the binding syntax of a variable.

Recall that a variable is bound by either a function binding; or, a pattern binding, and that a simple pattern binding is a pattern binding in which the pattern consists of only a single variable (Section 4.4.3).

MR on in ghc, and, MR off in ghci

Rule 1 - a

Rule 1 - b

Rule 2

Any monomorphic type variables (that remain when type inference for an entire module is complete) are considered ambiguous, and are resolved to particular types using the defaulting rules

show :: forall a. Show a => a -> String
read :: forall a. Read a => String -> a

let x = read "..."
in show x