課程簡介
型別論與邏輯
資訊系學生常問的一個問題是學習數學 — 特別是數學證明 — 對寫程式有什麼幫助，答案不外乎是特定領域（如機器學習、訊號處理等）會用到，或是較為模糊的「訓練邏輯思考」。第二個答案其實有完全精確的版本，無需模糊帶過：寫程式和寫證明完全是同一件事！
不過，在給這個答案之前，我們必須切換到另一個對數學本質的看法。古典數學 (classical mathematics) 的看法是數學物件獨立於人類心智存在，構成一個理型世界；數學家如同記者，工作是報導那個世界的實況。另一方面，直構數學 (intuitionistic mathematics) 認為數學物件 — 包括證明 — 是人類心智的主觀產物，而非客觀存在；數學家如同作家，工作是以心智構築出數學理論。直構觀點下，由於數學純粹是人類心智的活動（無涉理型），故構造出的數學物件必須符合「人類心智感知之先天條件」。這個神秘條件到了近代 — 特別因為計算機的發明與普及 — 終於能夠簡單且具體地解釋：直構數學的產物必須有計算意義。換句話說，直構數學家的工作本質正是程式編寫。
傳統的數理邏輯系統源於古典數學，多忽略計算意義；另一方面，一般程式語言的表達能力不夠細緻，遠不足以描述常見數學構造的精密性質。瑞典邏輯學家 Per Martin-Löf 於是在 ’70 年代設計出直構型別論 (intuitionistic type theory) 作為直構數學的邏輯基礎，至今其理論延伸和應用均仍蓬勃發展中。本次 FLOLAC 首度專課介紹型別論如何融合數理邏輯之性質表達能力以及函數編程之計算模型，並另有專課介紹以型別論為基礎的新一代函數編程（請待下回分解）。
回到最先問題：學習數學證明對寫程式有幫助嗎？我們的答案是：顯然有，因為閱讀證明就是研究數學家歷經數千年去蕪存菁的程式庫，而習寫證明則是練習在更全面的語意考量下編寫程式。一言以蔽之：資訊系學生應該多修點數學系的課（無誤）。
依值型別編程
D. E. Knuth 的名言 “Beware of bugs in the above code; I have only proved it correct, not tried it.” 被程式員譽為傳奇，因為現實情境中大家整天疲於除錯。於是當 E. W. Dijkstra 說出 “In programming, nothing is cheaper than not introducing the bugs in the first place.” 時，程式員只是嗤之以鼻 — 程式哪有不寫錯的！但事實上，依值型別編程 (dependently typed programming) 的相關研究正帶我們走向一個「程式不可能寫錯」的新世界！
當今主流程式語言的描述能力難以表達程式員的完整意圖，例如我們可描述樹狀資料結構但無法描述其平衡性質和元素排序，於是需要另外寫證明解釋程式之目的 — 當然，主流語言也無法表達型式證明，於是程式目的之解釋就退化為註釋。前篇介紹的直構型別論 (intuitionistic type theory) 造出一個證明與程式共存的環境，讓我們能在程式語言內直接證明程式的性質，但證明仍需另外寫就。踏在直構型別論的基礎上，依值型別編程的目標是更進一步融合證明與程式，藉著巧妙設計程式型別，使程式性質的證明能夠隱寓於程式本身，無需分開處理 — 如此一來，程式本身便足以表達原先需另以證明解釋之意義。例如，與其先寫程式將兩份樹狀資料結構合併為一份，再寫證明解釋此操作保持平衡性質和元素排序，我們可直接設計一個「平衡搜尋樹」資料型別，再寫出型別描述「將兩棵平衡搜尋樹合併為一棵」這樣的操作。依值型別系統確保任何具此型別的程式必須妥適處理嵌於「平衡搜尋樹型別」的平衡性質和元素排序，因此程式只要通過型別檢驗就必定正確。不僅如此，依值型別更能在程式編寫過程中提供語意上的提示，有時甚至能直接從型別自動推得符合的程式。
本次 FLOLAC 首度開課簡介依值型別編程這項尖端研究，以學界廣泛使用的依值型別語言 Agda 為例，讓大家搶先體驗新世界的編程工具！
操作與指稱語意
兩年前我們提到 CompCert 這個計劃，用 Coq 證明輔助系統（其理論基礎乃衍生自直構型別論）實作一個 C 編譯器（支援絕大部分的 C89）並完整證明輸入的 C 程式和編譯出的 PowerPC 組合語言程式語意相同。C 的語意由 C 標準書所規範，但 C 標準書的英文敘述無法作為嚴格證明的對象 — 只有將語意型式化才可能完整證明其性質。本次 FLOLAC 介紹函數程式的兩種型式語意：操作語意和指稱語意。前者制定一套符號推演規則，嚴謹地定義函數程式如何一步步運行、計算出結果；後者則是將函數程式詮釋為數學上適當意義的連續函數，除寫法簡潔外更揭露計算與拓樸連續性的優雅關聯。命令式語言的語意是改變機器狀態，和函數程式語意相比較為複雜，但操作語意或指稱語意經些許調整即足以描述命令式語言的語意 — CompCert 選用的是較方便撰寫型式證明的操作語意。如果你覺得 C/C++ 標準書不僅冗長又漏洞百出，請不要錯過這次的型式語意學，了解如何精簡定義語意、甚至證明語言的安全性質。
- 兩年前對 CompCert 的介紹在此：https://www.facebook.com/flolac.tw/posts/385496908176663
內嵌式領域特定語言
本屆 FLOLAC 除了以 Haskell 介紹基礎的函數編程 (functional programming), 還特別邀請到牛津大學 Jeremy Gibbons 教授介紹函數編程於「領域特定語言」(domain-specific languages) 的應用。
領域特定語言常對比於「泛用型語言」(general-purpose languages)：一般提到的程式語言如 Haskell, C/C++, Python 等皆屬後者，設計原則是達成豐富的表達能力，以求在同一語言內能寫出各式各樣的程式；領域特定語言則是聚焦於一個特定應用領域並為其設計專門語法，藉以更精準地捕捉專屬該領域的概念與慣用技巧和提供專門支援，一個重要例子是 parser generators 如 yacc 所接受的文法定義。
yacc 所接受的文法是完全獨立的語言，需要獨立程式處理，使得 yacc 和一般泛用型語言接軌的成本較高；相對比，函數編程能便利地處理具遞迴結構的資料，又提供絕佳的抽象能力，於是我們能非常輕鬆地直接在函數式語言內定義、使用領域特定語言。一個著名的用例是 parser combinators, 文法片段不僅能直接以 Haskell 自然寫出，本身還是可進一步任意操作的一級物件 (first-class objects).
Gibbons 教授將在課堂上講解領域特定語言的基礎概念，並帶領大家以 Haskell 實作 parser combinators 和 SVG 繪圖等領域特定語言。
