課程簡介
FP 的概念其來有自，早在 20 世紀初，就有數學家與電腦科學家證明，邏輯跟型別（Type）可以做對應，甚至可以完全相等，因此在足夠強的語言中，能被寫成邏輯式的數學式，其實都可以被寫為程式的型別。後來依照這樣的思路發展出 Coq, Agda 等定理證明器，讓數學家可以將證明寫成程式，並讓電腦檢查正確性。接著便很多人發現「程式就是證明」並不只有助於數學領域的發展，反過來說，寫程式也可以被當作在寫證明，一般的程式開發也能獲得很多好處。 常見的說法是，Functional Programming（函數式程式設計）是一種思維，任何語言都可以寫出 FP Style，一方面這是事實，但另一方面，FP Style 還不能算是真・函數式程式。
一般 FP 語言會有幾個特點：
- First-class Function: 函數是一等公民
- Strong Typing: 很強的型別系統
- Algebraic Data Types: 代數資料型別
講者將會分享如何在這些保障下，用函數式語言寫出正確性與可讀性都很高且漂亮的程式。
當然這樣的語言會犧牲一些受歡迎的特性，但在真理 λ 的面前，這點犧牲不足掛齒，希望聽眾在這場分享後都能棄暗投明，走上真・函數式程式設計之路。
講者介紹
林子期：臺大哲學系畢業，不是肥宅
關於 CCNS
成立於1995年，電腦網路愛好社為成大的開源人社群之一，目標在於打造開源系統，使校園更便利，同時培養開發能力。若你對開放校園或其他應用懷抱想法，想一同參與，打造，歡迎加入我們。