455 index.rss.xml fp-0001 index.xml 帶你入門 functional programming false

什麼是函數式程式設計是一個大哉問，但作為一個入門導引，我們簡單的定義成受 lambda calculus 啟發，並且格外注重可組合性的語言。在其上有兩種變體

  1. 一種現在相當著重在對形式計算時機的控制，也就是 macro 上，也就是 Lisp 與其延伸語言
  2. 一種則注重對數學概念的引進，乃自裡面有一種叫做代數類型的型別定義方法，其基本出發自 F-algebra，但其內涵相當深遠，並不止於此，例如定理證明器往往只使用其中的 inductives 這一類變體。

作為入門網站，這裡著重在第二類語言，因為 macro 與這類語言並沒有顯著衝突，並且也非入門概念，引進理論討論 macro 的運算控制也沒有問題，因此沒有理由特別用入門時的觀點分類。那麼，第二類語言裡面，同樣有許多著重不同的變體

  1. OCaml 著重類型正確，卻不在意 side effect
  2. Haskell 注重類型也注重 side effect 控制，同時對 type level 有一定的操作能力
  3. Agda, Coq, Lean 等語言作為寫程式的工具可能有點失格，但主要是因為目標完全不同，分類作語言的子類別：定理證明器 比較合適

這個網站的準則，是教導抽象的數學概念，讓學習者最終對實際 functional programming 有一定的了解，並大致理解現代語義學研究，或許能夠應用其成果。那麼，我們開始回顧 lambda calculus 與可計算性的沿革，開始學習 functional programming 吧

456 roadmap.rss.xml roadmap roadmap.xml 地圖 false

此地圖為一大方向，每個主體內會有延伸，包含實例、名詞解釋等等，類似於心智圖，而未來也有可能異動

  1. lambda calculus
  2. 用 recursion 解釋可計算性
  3. 加上 simply type
  4. 解釋型別規則
  5. 建立 STLC categorical semantic
  6. 加上 polymorphism
  7. 解釋型別規則
  8. 建立 E \to B categorical semantic
  9. 解釋 \lambda 2 的 polymorphic property
  10. 解釋 recursive type
  11. 連結 F-algebra
  12. 變成 dependent type
  13. 解釋型別規則
  14. 解釋模型（The natural model）
    • topos
    • topos fundamental theorem
    • presheaf
    • representable natural transformation
  15. 進入真正的應用
  16. side effect
  17. concurrency
  18. 安全性
    • 記憶體安全與子結構類型
      • (?) proof nets
    • 整體安全性不是只關乎記憶體
  19. domain language