五分鐘了解 Databend 全新 SQL 類型系統(tǒng)
引言
類型系統(tǒng)是數(shù)據(jù)庫的一個(gè)重要組成部分，它提供了一種一致的方式來確定 SQL 中的數(shù)據(jù)類型。類型系統(tǒng)的設(shè)計(jì)很大程度影響數(shù)據(jù)庫的易用性和健壯性，一個(gè)設(shè)計(jì)合理且一致的類型系統(tǒng)容易讓使用者判斷 SQL 的行為。反之，一個(gè)沒有經(jīng)過正式設(shè)計(jì)的類型系統(tǒng)會(huì)帶來各種暗坑和不一致行為在暗中背刺用戶。我們用編程語言舉個(gè)例子，JavaScript 被詬病的類型系統(tǒng)總是成為茶余飯后的談資：
因此我們希望在 Databend 中實(shí)現(xiàn)一個(gè)易于理解而又功能強(qiáng)大的類型推導(dǎo)系統(tǒng)，為此我們借鑒了不少優(yōu)秀編程語言的編譯器內(nèi)部設(shè)計(jì)，然后從中精簡出適用于 SQL 使用的子集。下文將會(huì)詳細(xì)展開介紹這個(gè)系統(tǒng)的設(shè)計(jì)原理。
接口設(shè)計(jì)
"低耦合高內(nèi)聚" 是我們經(jīng)常說的口頭禪，講的是要把做相同事情的代碼歸攏到一起，然后定義簡單的接口供外部使用。類型推導(dǎo)作為一個(gè)相對(duì)復(fù)雜的系統(tǒng)，在設(shè)計(jì)之初需要先定義好對(duì)外暴露的接口，也即能做什么以及外部怎么使用。
簡單來說，我們?cè)O(shè)計(jì)的類型推導(dǎo)系統(tǒng)可以做三件事：
輸入 SQL 文本（
RawExpr），檢查 SQL 是否符合類型規(guī)則，為函數(shù)調(diào)用選擇合適重載，返回可執(zhí)行的表達(dá)式 (Expr)。
輸入可執(zhí)行的表達(dá)式和數(shù)據(jù)，執(zhí)行然后返回結(jié)果。
輸入可執(zhí)行的表達(dá)式和數(shù)據(jù)取值范圍（存儲(chǔ)在元數(shù)據(jù)中），返回結(jié)果的取值范圍。
為此調(diào)用者只需：
定義所有可用函數(shù)的類型簽名、函數(shù)定義域到值域的映射、函數(shù)執(zhí)行體。
在執(zhí)行 SQL 或 constant folding 時(shí)調(diào)用執(zhí)行器。用布爾?
and?函數(shù)舉個(gè)例子，函數(shù)定義大致如下：
完整執(zhí)行的例子：
類型推導(dǎo)原理
新的類型系統(tǒng)支持以下數(shù)據(jù)類型：
Null
Boolean
String
UInt8
UInt16
UInt32
UInt64
Int8
Int16
Int32
Int64
Float32
Float64
Date
Interval
Timestamp
Array<T>
Nullalbe<T>
Variant
我們以一個(gè)例子看看類型推導(dǎo)系統(tǒng)是如何工作的，假設(shè)外部輸入了一個(gè)表達(dá)式：
類型推導(dǎo)器首先會(huì)將表達(dá)式轉(zhuǎn)換為函數(shù)調(diào)用：
然后類型檢查器可以簡單地推斷出常量的類型：
經(jīng)過查詢 FunctionRegistry，類型檢查器得知函數(shù) plus 有這些重載：
我們可以發(fā)現(xiàn)，函數(shù) plus 參數(shù)類型 Int8 和 String 不能匹配其中任何一個(gè)重載，因此類型檢查器會(huì)返回一個(gè)錯(cuò)誤報(bào)告：
但在類型檢查中我們?cè)试S一種例外，我們?cè)试S子類型轉(zhuǎn)換為父類型（CAST），這樣就可以讓函數(shù)接受子類型的參數(shù)。我們看這樣一個(gè)例子：
類型推導(dǎo)器根據(jù)規(guī)則推導(dǎo)出常量的類型：
經(jīng)過查詢 FunctionRegistry，我們發(fā)現(xiàn)函數(shù) plus 有兩個(gè)重載看似可以使用但又不完全匹配：
這時(shí)類型檢查器會(huì)嘗試啟用 CAST 規(guī)則盡最大可能選擇一個(gè)重載。根據(jù) CAST 規(guī)則，Int8 可以無損轉(zhuǎn)化成 Float32，因此類型檢查器會(huì)改寫表達(dá)式結(jié)構(gòu)然后重新檢查類型：
這樣就能順利通過類型檢查了。
泛型
新的類型檢查器支持在函數(shù)簽名定義中包含泛型，用來減少需要手動(dòng)定義的重載函數(shù)的數(shù)量。比如我們可以定義一個(gè)函數(shù)?array_get<T0>(Array<T0>, UInt64) :: T0，它接受一個(gè)數(shù)組和一個(gè)下標(biāo)，并返回?cái)?shù)組中下標(biāo)對(duì)應(yīng)的元素。
相比上一節(jié)中講到的類型檢查，檢查含有泛型簽名的函數(shù)多了一個(gè)步驟：選擇一個(gè)合適的具體類型替換泛型，替換后的類型需要可以通過類型檢查，如果不存在這樣的具體類型則返回說明原因（比如有沖突的約束）。這個(gè)步驟一般稱為 Unification，我們也用一個(gè)例子加以說明：
假設(shè)有兩個(gè)表達(dá)式，它們的類型分別是：
如果我們需要?ty1?和?ty2?擁有相同類型（比如?ty1?是入?yún)⒈磉_(dá)式類型，ty2?類型是入?yún)⒑灻?code>unify?會(huì)嘗試將?X?和?Y?替換為具體類型：
對(duì)?unify?有興趣的讀者可以閱讀?type_check.rs?源碼。在此推薦一本好書 《Types and Programing Languages》，其中闡述了編程語言的類型推導(dǎo)發(fā)展歷史，深入討論分析各種推導(dǎo)理論的原理和取舍，各個(gè)重要概念都有配套的 toy implementation 作為例子，非常值得失眠時(shí)閱讀。
總結(jié)
本文簡述了新類型系統(tǒng)的設(shè)計(jì)背景，介紹了運(yùn)行原理和執(zhí)行器使用方法。由于篇幅關(guān)系沒有深入介紹定義 SQL 函數(shù)的方法，那部分將會(huì)類型檢查器一樣精彩還包含不少 Rust 類型黑魔法，咱們下次有機(jī)會(huì)再嘮。
關(guān)于 Databend
Databend 是一款開源、彈性、低成本，基于對(duì)象存儲(chǔ)也可以做實(shí)時(shí)分析的新式數(shù)倉。期待您的關(guān)注，一起探索云原生數(shù)倉解決方案，打造新一代開源 Data Cloud。
Databend 文檔：https://databend.rs/
Twitter：https://twitter.com/Datafuse_Labs
Slack：https://datafusecloud.slack.com/
Wechat：Databend
GitHub ：https://github.com/datafuselabs/databend
