寫一篇真正的導引文章

[dannypsnl]

現在放在 README 的話閱讀順序很亂，還是得找個時間整理看看應該怎麼樣導引讀者

[dannypsnl]

如果初步寫的話我覺得會需要按順序

1. 用 FP 有什麼不同
2. 一個實際的案例是什麼
3. FP 的基礎概念

[FizzyElt]

導引文章應該會放首頁，然後其他用連結的方式

[dannypsnl]

對啊，在導引文章裡面深入概念就可以開始放連結

[dannypsnl]

初稿

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

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

作為入門網站，這裡會著重在第二類語言，因為 macro 與這類語言並沒有顯著衝突，並且遠非入門概念。那麼，第二類的語言裡面，同樣有許多著重不同的變體

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

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

[dannypsnl]

寫完這我有幾個想法

1. 分類
   1. 屬於實際使用問題的需要自己一國，在現存裡面是指 data first/last
   2. 數學概念自己一圈，也就是幾個原始代數 magma, semigroup, ...
2. 需要增加 lambda calculus 的描述
3. 需要對接下來的發展設定地圖，讓導引有效果

[dannypsnl]

另外，因為網站有 cmd+k 或是 ctrl+k 這種功能，需要有網站使用教學作為一張卡，教導使用者

[FizzyElt]

補一下我的想法，看可不可以加進去
「作為一個 Functional Programming 學習者，我們都知道 FP 背後包含了一些數學概念，而當我們想把實際應用跟數學聯繫在一起時卻困難重重，因為現有 FP 網路資源過於兩極化，要麼純數學，要麼純應用，所以很難體會 FP 的奧妙之處。」

「我們期望透過這個網站，讓正在使用/學習 FP 的人了解，你每個使用的手法背後所隱含的想法，並且在想更深入時給予指引」

[FizzyElt]

使用教學應該會順便把關於網站的資訊順便放進去

[dannypsnl]

對於地圖，我的基本想法是

1. lambda calculus
2. 用 recursion 解釋可計算性
3. 加上 simply type
4. 解釋型別規則
5. 建立 STLC categorical semantic
6. 加上 polymorphism $\lambda 2$
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 fundenmental theorem
    • presheaf
    • representable natural transformation
15. 進入真正的應用
16. side effect
17. concurrency
18. 安全性
    • 記憶體安全與子結構類型
      • (?) proof nets
    • 整體安全性不是只關乎記憶體
19. domain language

在實際應用方面，在任何合適的時機都可以提及，並且作為入門，必須有相當多的應用案例

[FizzyElt]

是否先以這份當作 roadmap 整理到 首頁跟 README 內

[dannypsnl]

對啊，我有 draft PR