CCNS 定期聚 — 函數式程式設計與型別理論

課程簡介

FP 的概念其來有自,早在 20 世紀初,就有數學家與電腦科學家證明,邏輯跟型別(Type)可以做對應,甚至可以完全相等,因此在足夠強的語言中,能被寫成邏輯式的數學式,其實都可以被寫為程式的型別。後來依照這樣的思路發展出 Coq, Agda 等定理證明器,讓數學家可以將證明寫成程式,並讓電腦檢查正確性。接著便很多人發現「程式就是證明」並不只有助於數學領域的發展,反過來說,寫程式也可以被當作在寫證明,一般的程式開發也能獲得很多好處。 常見的說法是,Functional Programming(函數式程式設計)是一種思維,任何語言都可以寫出 FP Style,一方面這是事實,但另一方面,FP Style 還不能算是真・函數式程式。

一般 FP 語言會有幾個特點:
- First-class Function: 函數是一等公民
- Strong Typing: 很強的型別系統
- Algebraic Data Types: 代數資料型別

講者將會分享如何在這些保障下,用函數式語言寫出正確性與可讀性都很高且漂亮的程式。
當然這樣的語言會犧牲一些受歡迎的特性,但在真理 λ 的面前,這點犧牲不足掛齒,希望聽眾在這場分享後都能棄暗投明,走上真・函數式程式設計之路。

 


講者介紹

林子期:臺大哲學系畢業,不是肥宅

 


關於 CCNS

成立於1995年,電腦網路愛好社為成大的開源人社群之一,目標在於打造開源系統,使校園更便利,同時培養開發能力。若你對開放校園或其他應用懷抱想法,想一同參與,打造,歡迎加入我們。

 
 

 

 
 

 

 

Event Tickets

Ticket Type Sale Period Price
一般チケット 2020/05/14 00:00(+0800) ~ 2020/05/21 19:00(+0800) End of Sale
  • Free
Next Step

10 Attendees