第 11 章 OCaml 語言

8 類型和例外定義

8.1 類型定義

類型定義將類型建構子綁定到資料類型:變體類型、記錄類型、類型縮寫或抽象資料類型。它們也綁定與定義相關的值建構子和記錄欄位。

類型定義::= type [nonrec] typedef { andtypedef }
 
typedef::=[type-params] typeconstr-nametype-information
 
類型資訊::=[type-equation] [type-representation] { type-constraint }
 
類型方程式::= =typexpr
 
類型表示::= = [|] constr-decl { |constr-decl }
 =record-decl
 =|
 
類型參數::= 類型參數
 (type-param { ,type-param } )
 
類型參數::=[ext-variance] 'ident
 
外部變異性::= variance [injectivity]
 injectivity [variance]
 
變異性::= +
 -
 
單射性::=!
 
記錄宣告::= {field-decl { ;field-decl } [;] }
 
建構子宣告::=(constr-name ∣ [] ∣ (::)) [ ofconstr-args ]
 
建構子參數::= typexpr { *typexpr }
 
欄位宣告::=[mutable] field-name:poly-typexpr
 
類型約束::= constrainttypexpr=typexpr

另請參閱以下語言擴展:私有類型廣義代數資料類型屬性擴展節點可擴展變體類型內聯記錄

類型定義由 type 關鍵字引入,並由一個或多個簡單定義組成,這些定義可能是相互遞迴的,並以 and 關鍵字分隔。每個簡單定義都定義一個類型建構子。

一個簡單定義由一個小寫識別符號組成,前面可能有一個或多個類型參數,後面接著一個可選的類型方程式,然後是一個可選的類型表示,然後是一個約束子句。該識別符號是正在定義的類型建構子的名稱。

type colour =
  | Red | Green | Blue | Yellow | Black | White
  | RGB of {r : int; g : int; b : int}

type 'a tree = Lf | Br of 'a * 'a tree * 'a;;

type t = {decoration : string; substance : t'}
and t' = Int of int | List of t list

在類型定義的右側,對正在定義的類型建構子名稱的引用被視為遞迴的,除非 type 後面跟著 nonrecnonrec 關鍵字是在 OCaml 4.02.2 中引入的。

可選的類型參數是一個類型變數 ' ident,用於具有一個參數的類型建構子,或者是一個類型變數列表 ('ident1,…,'identn),用於具有多個參數的類型建構子。每個類型參數可能以變異性約束 + (resp. -) 作為前綴,表示該參數是協變的(resp. 反變的),以及單射性註解 !,表示該參數可以從整個類型中推斷出來。這些類型參數可以出現在定義的右側的類型表達式中,可選地受限於變異性約束; 協變參數只能出現在函數箭頭的右側(更精確地說,遵循偶數個箭頭的左分支),而反變參數只能出現在左側(奇數個箭頭的左分支)。如果類型具有表示或方程式,並且該參數是自由的( 沒有透過類型約束綁定到建構的類型),則會檢查其變異性約束,但子類型化等等將使用參數的推斷變異性,這可能不那麼嚴格;否則( 對於抽象類型或非自由參數),必須明確給出變異性,並且如果沒有給出變異性,則參數是不變的。

可選的類型方程式 = typexpr 使定義的類型等效於類型表達式 typexpr:可以在類型檢查期間將一個替換為另一個。如果沒有給出類型方程式,則會產生一個新類型:定義的類型與任何其他類型都不相容。

可選的類型表示透過給出相關的建構子列表(如果它是變體類型)或相關的欄位列表(如果它是記錄類型)來描述表示定義的類型的資料結構。如果沒有給出類型表示,則除了在可選的類型方程式中聲明之外,不會對類型的結構做出任何假設。

類型表示 = [|] constr-decl { | constr-decl } 描述變體類型。建構子宣告 constr-decl1, …, constr-decln 描述與此變體類型相關的建構子。建構子宣告 constr-name of typexpr1 ** typexprn 將名稱 constr-name 宣告為非常數建構子,其參數的類型為 typexpr1typexprn。建構子宣告 constr-name 將名稱 constr-name 宣告為常數建構子。建構子名稱必須大寫。

類型表示 = { field-decl { ; field-decl } [;] } 描述記錄類型。欄位宣告 field-decl1, …, field-decln 描述與此記錄類型相關的欄位。欄位宣告 field-name : poly-typexprfield-name 宣告為欄位,其參數類型為 poly-typexpr。欄位宣告 mutable field-name : poly-typexpr 行為類似;此外,它允許對此欄位進行實體修改。不可變欄位是協變的,可變欄位是不變的。可變欄位和不可變欄位都可能具有明確的多型類型。每當建立或修改記錄值時,都會靜態檢查內容的多型性。提取的值可能會實例化其類型。

類型定義的兩個組件,可選的方程式和可選的表示,可以獨立組合,產生四種典型情況

抽象類型:無方程式,無表示。
 ‍
當出現在模組簽章中時,此定義除了參數的數量外,不會指定類型建構子的任何資訊:其表示形式是隱藏的,並且假設與任何其他類型都不相容。
類型縮寫:有方程式,無表示。
 ‍
這將類型建構子定義為 = 符號右側的類型表達式的縮寫。
新變體類型或記錄類型:無方程式,有表示。
 ‍
這會產生一個新的類型建構子,並定義相關的建構子或欄位,透過這些建構子或欄位可以直接建立或檢查該類型的值。
重新匯出的變體類型或記錄類型:有方程式,有表示。
 ‍
在這種情況下,類型建構子被定義為方程式中給出的類型表達式的縮寫,但此外,表示形式中給出的建構子或欄位仍然附加到定義的類型建構子。方程式部分的類型表達式必須與表示形式一致:它必須是相同的類型(記錄或變體),並且具有完全相同的建構子或欄位,以相同的順序,並具有相同的參數。此外,新的類型建構子必須與原始類型建構子具有相同的元數和相同的類型約束。

作為型別參數出現的型別變數,可以選擇性地加上前綴 +-,以表明該型別建構子對於此參數是協變的或逆變的。當檢查 :> 強制轉換的有效性時(請參閱 11.7.7 節),會使用此變異資訊來決定子型別關係。

例如,type +'a t 宣告 t 為一個在其參數中協變的抽象型別;這表示如果型別 τ 是型別 σ 的子型別,則 τ t 是 σ t 的子型別。類似地,type -'a t 宣告抽象型別 t 在其參數中是逆變的:如果 τ 是 σ 的子型別,則 σ t 是 τ t 的子型別。如果沒有給定 +- 變異註解,則假設該型別建構子在相應的參數中是不變的。例如,抽象型別宣告 type 'a t 表示如果 τ 是 σ 的子型別,則 τ t 既不是 σ t 的子型別,也不是超型別。

參數上由 +- 註解指示的變異僅對抽象型別和私有型別強制執行,或者當存在型別約束時。否則,對於沒有型別約束的縮寫、變體和記錄型別,型別建構子的變異屬性會從其定義中推斷出來,而變異註解僅會檢查是否與定義一致。

注入性註解僅對於抽象型別和私有列型別是必要的,因為它們可以從型別宣告中推斷出來:所有參數對於記錄和變體型別宣告(包括可擴展型別)都是注入的;對於型別縮寫,如果參數在其定義方程式中具有注入性出現(無論是否為私有),則該參數是注入的。對於型別縮寫中的受約束型別參數,如果它們出現在主體的注入性位置,或者如果它們的所有型別變數都是注入的,則它們是注入的;特別是,如果受約束型別參數包含一個沒有出現在主體中的變數,則它不能是注入的。

建構子 constraint ' ident = typexpr 允許指定型別參數。對應於型別參數 ident 的任何實際型別引數都必須是 typexpr 的實例(更精確地說,identtypexpr 被統一)。typexpr 的型別變數可以出現在型別方程式和型別宣告中。

8.2 例外定義

例外-定義::= exceptionconstr-decl
 exceptionconstr-name=constr

例外定義會將新的建構子添加到例外值內建的變體型別 exn 中。這些建構子的宣告方式與變體型別的定義相同。

# exception E of int * string;;
exception E of int * string

形式 exception constr-decl 會產生一個新的例外,與系統中所有其他例外不同。形式 exception constr-name = constr 會為現有的例外提供另一個名稱。

# exception E of int * string exception F = E let eq = E (1, "one") = F (1, "one");;
exception E of int * string exception F of int * string val eq : bool = true