文章目錄
-
-
- Week5 Introduction
- What is Type Inference
- ML Type Inference
- Type Inference Examples
- Polymorphic Examples
- Optional: The Value Restriction and Other Type-Inference Challenges
- Mutual Recursion
- Modules for Namespace
- Signatures and Hiding Things
- A Module Example
- Signatures for Our Example
- Signature Matching
- An Equivalent Structure
- Another Equivalent Structure
- Different Modules Define Different Types
- Equivalent Functions
- Standard Equivalences
- Equivalence Versus Performance
-
Week5 Introduction
第五周内容的簡單導引
What is Type Inference
關于type-checking。ML屬于靜态類型語言（雖然在編寫代碼時并不要求顯式标出變量類型），在編譯時會判斷變量類型。
是以ML語言其實是一種隐含類型(Implicitly typed)的靜态類型語言
類型推斷，為每個bingding或者表達式給定一個類型，這樣就判斷type-chcking成功
ML Type Inference
ML的類型推斷
類型推斷的關鍵步驟：
類型推斷的簡單例子：
ML中為無法判斷的類型給定一個Type Variable （例如 'a, 'b，可用于實作多态）。但需要注意的是并不是所有type inference的語言都有type variable（例如Java），有type variable的語言也不一定會做type inference
Type Inference Examples
類型推斷始終遵循幾大步驟（與上一節相同的步驟）
1、按照順序收集所有binding，并決定類型
2、對于每個binding（變量或者表達式或者函數等）
（1）收集所有類型檢查需要的事實，分析限制條件**（Constraints）**來确定類型
（2）類型的事實有沖突，抛出type error （Over-Constrained）
（3）對沒有事實可以判斷類型的binding給定一個type variable （Unconstrained）
其中2-(1)是本節闡述的内容，如何通過事實分析限制條件
例子1：
例子2：
Polymorphic Examples
多态的例子，首先仍然是同樣的判斷準則：
例子1
例子2，T4存在兩種情況，因為編譯器不知道會執行哪一條語句，隻知道type的可能性。隻有在運作時才能确定執行哪條語句。
例子3：
Optional: The Value Restriction and Other Type-Inference Challenges
截至目前，課程講述的ML 類型推斷體系是不完全的，但想要讓它更完善就不得不引入更進階但更不優雅的内容
例如如下問題：
我們不能隻是為reference類型制定特殊規則來避免這個問題，因為ML的函數可傳遞，同時類型又可以取别名，type-checker不知道reference的别名（type-chekcer在運作之前檢查）。
解決方案是為整個語言引入Value restriction的機制，隻讓變量binding（變量或者值的表達式或者函數定義時）獲得多态類型，但函數調用不能獲得多态類型（會給出一個警告和無限制的假類型）：
當編譯器無法判斷是否有reference參加或者是否生成reference的時候，也會使用value restriction
關于子類型的讨論，子類型 所實作的多态（類似于其他語言中子類和超類的關系，例如超類指針指向子類位址），在一定的細節限制下也可以支援，但會讓語言中的類型更難以推斷和了解（是以在C++和Java這類靜态類型語言中需要顯式聲明變量的類型）
Mutual Recursion
互遞歸就是兩個函數互相調用，有一定用處，例如可以實作狀态機，但也會帶來一些問題（由于互相調用，難以厘清binding的先後順序）：
ML的做法是定義一套新的結構，使用and關鍵詞來連接配接多個函數或datatype（因為datatype定義時也可以遞歸定義）等，這些使用and連接配接的變量将會作為一個整體（bundle），同時被type-check或valuate
例子：
第二個例子：
同時，也可以使用高等函數（傳遞一等函數）來替代and結構，實作同樣的功能
Modules for Namespace
使用structure關鍵詞定義modules 。modules的概念在ML中類似于C++的命名空間和類的混合概念（可以用來定義ADT，見後面的例子）。
例子:
open關鍵詞用于直接引入一個module，可以不帶module名直接使用其中的bindings（類似python的
from xxx import *
)。也可以通過函數傳遞的方式，将module的某個函數binding到某個變量上，直接使用。
Signatures and Hiding Things
Signature是module的一種類型，其中定義有哪些binding與binding的類型，可以通過 :> 符号作用于module。（這裡的signature和module又有點像Java的接口和類的關系了，但也不太一樣）。
** signatures的真正價值是用來隐藏某些bindings及其類型的定義，并對外隐藏實作細節（從這個意義上來說，signatures實際上也确實類似接口的功能）。
通過signatures我們可以實作private和public的bindings。
- 在signatures中定義的bindings可以在module外部使用（public）
- 不在signatures中定義的bindings 不能在module外部使用，但可以在内部使用（private）
A Module Example
定義一個ADT，表示實數及其運算
(* Section 4: A Module Example *)
(* will assign different signatures to this module in later segments *)
structure Rational1 =
struct
(* Invariant 1: all denominators > 0
Invariant 2: rationals kept in reduced form *)
datatype rational = Whole of int | Frac of int*int
exception BadFrac
(* gcd and reduce help keep fractions reduced,
but clients need not know about them *)
(* they _assume_ their inputs are not negative *)
fun gcd (x,y) =
if x=y
then x
else if x < y
then gcd(x,y-x)
else gcd(y,x)
fun reduce r =
case r of
Whole _ => r
| Frac(x,y) =>
if x=0
then Whole 0
else let val d = gcd(abs x,y) in (* using invariant 1 *)
if d=y
then Whole(x div d)
else Frac(x div d, y div d)
end
(* when making a frac, we ban zero denominators *)
fun make_frac (x,y) =
if y = 0
then raise BadFrac
else if y < 0
then reduce(Frac(~x,~y))
else reduce(Frac(x,y))
(* using math properties, both invariants hold of the result
assuming they hold of the arguments *)
fun add (r1,r2) =
case (r1,r2) of
(Whole(i),Whole(j)) => Whole(i+j)
| (Whole(i),Frac(j,k)) => Frac(j+k*i,k)
| (Frac(j,k),Whole(i)) => Frac(j+k*i,k)
| (Frac(a,b),Frac(c,d)) => reduce (Frac(a*d + b*c, b*d))
(* given invariant, prints in reduced form *)
fun toString r =
case r of
Whole i => Int.toString i
| Frac(a,b) => (Int.toString a) ^ "/" ^ (Int.toString b)
end
Signatures for Our Example
使用signatures，隐藏上一節的例子中的gcd和reduce，将bindings私有化
但是隻隐藏函數當然會有問題，我們的變量并沒有得到有效封裝（暴露給了使用者），使用者可以通過例如Rationall.Frac(1,0)來自己産生這個變量。我們應該把這些部分封裝起來。
是以需要将内部datatype定義的類型一并設為私有，并留出給使用者定義變量的接口 make_frac。但問題在于signatures中開放的函數需要用到datatype定義的rational類型，但現在signatures不知道它存在。
要解決這個問題，ML中可以通過type關鍵詞在signatures中标明某種類型的存在（一種抽象類型），但不開放給使用者（使用者不知道其定義）
是以，使用signatures的兩大關鍵在于：
另外，比較有趣的事情是，由于Whole不會引發異常帶來問題，我們也可以對使用者開放Whole（相當于開放rational的一部分），記得datatype的Constructor本身就是一個函數，是以我們可以直接在signatures中寫上Whole函數的部分，而不需要在module中重複定義（因為定義datatype的時候已經寫了
datatype rational = Whole of int | Frac of int*int
，Whole在這裡就會被認為是一個int->rational的函數定義）
Signature Matching
An Equivalent Structure
抽象的一大目的是讓不同實作（implementation）相等（equivalent）（對使用者而言），例如接口的抽象也是需要讓類實作對使用者等效。使用者不關心具體實作細節，但相同的接口（即使實作不同），也應該得到等效的結果。
例如，以前面的三種RATIONAL signatures為例：
老師給出的例子：
(* Section 4: An Equivalent Structure *)
(* this signature hides gcd and reduce.
That way clients cannot assume they exist or
call them with unexpected inputs. *)
signature RATIONAL_A =
sig
datatype rational = Frac of int * int | Whole of int
exception BadFrac
val make_frac : int * int -> rational
val add : rational * rational -> rational
val toString : rational -> string
end
(* the previous signature lets clients build
any value of type rational they
want by exposing the Frac and Whole constructors.
This makes it impossible to maintain invariants
about rationals, so we might have negative denominators,
which some functions do not handle,
and print_rat may print a non-reduced fraction.
We fix this by making rational abstract. *)
signature RATIONAL_B =
sig
type rational (* type now abstract *)
exception BadFrac
val make_frac : int * int -> rational
val add : rational * rational -> rational
val toString : rational -> string
end
(* as a cute trick, it is actually okay to expose
the Whole function since no value breaks
our invariants, and different implementations
can still implement Whole differently.
*)
signature RATIONAL_C =
sig
type rational (* type still abstract *)
exception BadFrac
val Whole : int -> rational
(* client knows only that Whole is a function *)
val make_frac : int * int -> rational
val add : rational * rational -> rational
val toString : rational -> string
end
(* this structure can have all three signatures we gave
Rationa1 in previous segments, and/but it is
/equivalent/ under signatures RATIONAL_B and RATIONAL_C
this structure does not reduce fractions until printing
*)
structure Rational2 :> RATIONAL_A (* or B or C *) =
struct
datatype rational = Whole of int | Frac of int*int
exception BadFrac
fun make_frac (x,y) =
if y = 0
then raise BadFrac
else if y < 0
then Frac(~x,~y)
else Frac(x,y)
fun add (r1,r2) =
case (r1,r2) of
(Whole(i),Whole(j)) => Whole(i+j)
| (Whole(i),Frac(j,k)) => Frac(j+k*i,k)
| (Frac(j,k),Whole(i)) => Frac(j+k*i,k)
| (Frac(a,b),Frac(c,d)) => Frac(a*d + b*c, b*d)
fun toString r =
let fun gcd (x,y) =
if x=y
then x
else if x < y
then gcd(x,y-x)
else gcd(y,x)
fun reduce r =
case r of
Whole _ => r
| Frac(x,y) =>
if x=0
then Whole 0
else
let val d = gcd(abs x,y) in
if d=y
then Whole(x div d)
else Frac(x div d, y div d)
end
in
(* 注意這裡調用的reduce，Rational1中沒有reduce *)
case reduce r of
Whole i => Int.toString i
| Frac(a,b) => (Int.toString a) ^ "/" ^ (Int.toString b)
end
end
可以發現，如果給使用者過多的權限（例如在signatures中定義了rational類型，使用者能直接調用Frac構造器）就會導緻如下的不同實作中結果不相等的情況，這樣的抽象就不是一個好的抽象。是以将rational在signature中作為一個抽象類型是非常重要的。
結論是：當signature的公共接口暴露的越少（抽象程度越高），不同實作對使用者的呈現結果越可能實作equivalent。
Another Equivalent Structure
不同的structures可以為signature中的抽象類型提供不同實作，例如讓type rational = int * int
注意第二點細節，雖然signature規定Whole需要int -> rational，但這是對外部而言（signature規定都是對外部而言），在内部由于目前的例子中Whole沒有定義，是以可以自行定義，甚至可以實作多态’a -> 'a * int（在内部調用時），但在外部就必須是int->int*int ,也就是目前的int -> rational
Different Modules Define Different Types
即使是實作了同一個signature的modules，不同的實作都定義了不同的類型。
例子，當多個不同的modules互相調用時會抛出異常，這也很容易了解（畢竟module首先具有命名空間的作用，每個module内部函數生成的内部變量都要帶上一個命名空間的字首，例如Rational3.rational）
從這些子產品的函數類型可以看出，不同的子產品就是不同的類型
Equivalent Functions
為什麼我們需要Equivalence
（1）為了代碼維護或重構
（2）為了代碼疊代向下相容
（3）為了優化代碼運作效率
（4）為了代碼抽象
例如我們需要在重構垃圾代碼時保持函數功能（包括接口）不變，這就是一種Equivalence
兩個函數什麼時候能夠實作等效？在他們在任何地方都擁有觀察起來相同的行為的時候
這裡注意一下副作用（side-effect），在函數式程式設計中，我們盡可能讓所有的函數都定義成實作一種類似于數學函數的行為模式（接受自變量，傳回因變量），而沒有多餘的操作。這些多餘的操作，例如在函數中（不是通過傳回值shadowing的方式）改變某個變量的現有值（mutation），讀取裝置或檔案等的輸入或者向裝置或檔案輸出（input/output），抛出異常和處理異常（exception raise and handle）等，都相當于是函數的副作用。
純粹的函數更可能讓事物（讓更多事物）等效（Pure functions make more things equivalent）
Standard Equivalences
其他一些标準的等效情況
（1）先是文法糖 andalso orelse之類的等效
（2）然後是替換函數内部的一些參數名
（3）是否使用helper function不影響等效情況（在使用的函數的scope沒改變的情況下）
（4）不必要的function wrapping不影響等效
值得注意的是，下面例子中的反例，左側g會表現為定義時不會print（因為是函數定義，不會調用），但調用時print every time，右側g表現為定義（實際上不是定義函數，而是傳遞(h())的調用結果）時print一次，之後調用不會再print
(5) 在忽略類型的時候，下面的兩種表達式等效（let 和 匿名函數）
但事實上兩者的類型不同，左側的x可以多态，而右側不可。右側的涵蓋範圍相對小一些。（why？這裡其實沒太了解）
Equivalence Versus Performance
Equivalence雖然是外部表現相同，但由于内部實作不同，會導緻運作表現上的差異（例如時間、空間差異）。這也是為什麼我們能夠優化代碼效率（内部）并保持Equivalence（外部）。
為不同的任務定義不同的等效定義：