[docs] 反应网编程 -- 完成 List 的讲解

cicada-lang · Sep 5, 2023 · 1e7a052 · 1e7a052
1 parent 9825a2f
commit 1e7a052
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 10 deletions.
diff --git a/TODO.md b/TODO.md
@@ -1,6 +1,5 @@
 # articles
 
-[docs] 反应网编程 -- 完成 `List` 的讲解
 [docs] 反应网编程 -- 完成 `DiffList` 的讲解
 [docs] 反应网编程 -- 总结
 

diff --git a/docs/articles/反应网编程.md b/docs/articles/反应网编程.md
@@ -651,7 +651,7 @@ rule add1 max_aux
 end
 ```
 
-[去 `Nat` 与 `(max)` 的演算场](https://inet.run/playground/dHlwZSBOYXQgLS0gQFR5cGUgZW5kCgpub2RlIHplcm8KICAtLS0tLS0KICBOYXQgOnZhbHVlIQplbmQKCm5vZGUgYWRkMQogIE5hdCA6cHJldgogIC0tLS0tLS0tLS0KICBOYXQgOnZhbHVlIQplbmQKCi8vIFRvIGRlZmluZSBgbWF4YCwgd2UgbmVlZCBgbWF4X2F1eGAuCgpub2RlIG1heF9hdXgKICBOYXQgOmZpcnN0CiAgTmF0IDpzZWNvbmQhCiAgLS0tLS0tLS0KICBOYXQgOnJldHVybgplbmQKCm5vZGUgbWF4CiAgTmF0IDpmaXJzdCEKICBOYXQgOnNlY29uZAogIC0tLS0tLS0tLS0KICBOYXQgOnJldHVybgplbmQKCnJ1bGUgemVybyBtYXgKICAobWF4KS1zZWNvbmQgcmV0dXJuLShtYXgpCmVuZAoKcnVsZSBhZGQxIG1heAogIChtYXgpLXNlY29uZCAoYWRkMSktcHJldiBtYXhfYXV4CiAgcmV0dXJuLShtYXgpCmVuZAoKcnVsZSB6ZXJvIG1heF9hdXgKICAobWF4X2F1eCktZmlyc3QgYWRkMQogIHJldHVybi0obWF4X2F1eCkKZW5kCgpydWxlIGFkZDEgbWF4X2F1eAogIChhZGQxKS1wcmV2IChtYXhfYXV4KS1maXJzdCBtYXgKICBhZGQxIHJldHVybi0obWF4X2F1eCkKZW5kCgpjbGFpbSBvbmUgLS0gTmF0IGVuZApkZWZpbmUgb25lIHplcm8gYWRkMSBlbmQKCmNsYWltIHR3byAtLSBOYXQgZW5kCmRlZmluZSB0d28gb25lIGFkZDEgZW5kCgpjbGFpbSB0aHJlZSAtLSBOYXQgZW5kCmRlZmluZSB0aHJlZSB0d28gYWRkMSBlbmQKCmNsYWltIGZvdXIgLS0gTmF0IGVuZApkZWZpbmUgZm91ciB0aHJlZSBhZGQxIGVuZAoKemVybyB0d28gbWF4Cgp0aHJlZSB0d28gbWF4)
+[去 `Nat` 与 `(max)` 的演算场](https://inet.run/playground/dHlwZSBOYXQgLS0gQFR5cGUgZW5kCgpub2RlIHplcm8KICAtLS0tLS0KICBOYXQgOnZhbHVlIQplbmQKCm5vZGUgYWRkMQogIE5hdCA6cHJldgogIC0tLS0tLS0tLS0KICBOYXQgOnZhbHVlIQplbmQKCm5vZGUgbWF4X2F1eAogIE5hdCA6Zmlyc3QKICBOYXQgOnNlY29uZCEKICAtLS0tLS0tLQogIE5hdCA6cmV0dXJuCmVuZAoKbm9kZSBtYXgKICBOYXQgOmZpcnN0IQogIE5hdCA6c2Vjb25kCiAgLS0tLS0tLS0tLQogIE5hdCA6cmV0dXJuCmVuZAoKcnVsZSB6ZXJvIG1heAogIChtYXgpLXNlY29uZCByZXR1cm4tKG1heCkKZW5kCgpydWxlIGFkZDEgbWF4CiAgKG1heCktc2Vjb25kIChhZGQxKS1wcmV2IG1heF9hdXgKICByZXR1cm4tKG1heCkKZW5kCgpydWxlIHplcm8gbWF4X2F1eAogIChtYXhfYXV4KS1maXJzdCBhZGQxCiAgcmV0dXJuLShtYXhfYXV4KQplbmQKCnJ1bGUgYWRkMSBtYXhfYXV4CiAgKGFkZDEpLXByZXYgKG1heF9hdXgpLWZpcnN0IG1heAogIGFkZDEgcmV0dXJuLShtYXhfYXV4KQplbmQKCmNsYWltIG9uZSAtLSBOYXQgZW5kCmRlZmluZSBvbmUgemVybyBhZGQxIGVuZAoKY2xhaW0gdHdvIC0tIE5hdCBlbmQKZGVmaW5lIHR3byBvbmUgYWRkMSBlbmQKCmNsYWltIHRocmVlIC0tIE5hdCBlbmQKZGVmaW5lIHRocmVlIHR3byBhZGQxIGVuZAoKY2xhaW0gZm91ciAtLSBOYXQgZW5kCmRlZmluZSBmb3VyIHRocmVlIGFkZDEgZW5kCgp6ZXJvIHR3byBtYXgKCnRocmVlIHR3byBtYXg)
 
 ```
 type Nat -- @Type end
@@ -667,8 +667,6 @@ node add1
   Nat :value!
 end
 
-// To define `max`, we need `max_aux`.
-
 node max_aux
   Nat :first
   Nat :second!
@@ -828,7 +826,24 @@ three three mul
 
 # 11
 
-TODO `List` -- `append` 如何与 `add` 类似。
+下面我们在自然数 `Nat` 这个最简单的数据之后，
+介绍几乎是第二简单的数据 -- 链表 `List`。
+
+在演算场中渲染出来的图中，
+我们可以明显看到 `List` 的 `(append)`
+与 `Nat` 的 `(add)` 非常相似。
+差异是 `Nat` 的 `(add1)` 只是单纯地增加一个节点，
+而 `List` 的 `(cons)` 在增加一个节点的同时，
+还连接到了一个额外的节点。
+
+在下面的代码中，我们有使用了一个新的词 `'A`。
+
+- `'A` 会将 `A` 这个符号放入栈中。
+- `'A` 可以用做类型变元。
+- 类型变元可以作为类型参数，比如 `'A List`。
+
+在定义 `(cons)` 和 `(append)` 时，代表类型变元的相同的符号 `'A`，出现了多次。
+这意味着在连接这些节点的接口时，这个类型变元必须匹配到相同的类型。
 
 [去 `List` 与 `(append)` 的演算场](https://inet.run/playground/dHlwZSBMaXN0IEBUeXBlIC0tIEBUeXBlIGVuZAoKbm9kZSBudWxsCiAgLS0tLS0tLS0KICAnQSBMaXN0IDp2YWx1ZSEKZW5kCgpub2RlIGNvbnMKICAnQSA6aGVhZAogICdBIExpc3QgOnRhaWwKICAtLS0tLS0tLQogICdBIExpc3QgOnZhbHVlIQplbmQKCm5vZGUgYXBwZW5kCiAgJ0EgTGlzdCA6dGFyZ2V0IQogICdBIExpc3QgOnJlc3QKICAtLS0tLS0tLQogICdBIExpc3QgOnJldHVybgplbmQKCnJ1bGUgbnVsbCBhcHBlbmQKICAoYXBwZW5kKS1yZXN0CiAgcmV0dXJuLShhcHBlbmQpCmVuZAoKcnVsZSBjb25zIGFwcGVuZAogIChhcHBlbmQpLXJlc3QgKGNvbnMpLXRhaWwgYXBwZW5kCiAgKGNvbnMpLWhlYWQgY29ucwogIHJldHVybi0oYXBwZW5kKQplbmQKCmltcG9ydCB6ZXJvIGZyb20gImh0dHBzOi8vY2RuLmluZXQucnVuL3Rlc3RzL2RhdGF0eXBlL05hdC5pIgoKbnVsbCB6ZXJvIGNvbnMgemVybyBjb25zCm51bGwgemVybyBjb25zIHplcm8gY29ucwphcHBlbmQKCm51bGwgemVybyBjb25zIHplcm8gY29ucwpudWxsIHplcm8gY29ucyB6ZXJvIGNvbnMKYXBwZW5kIEBydW4gJHJlc3VsdA)
 
@@ -887,7 +902,7 @@ with difference-lists: the idea consists in
 plugging the front of the second argument
 at the back of the first one.
 
-[去 `DiffList` 与 `(diff_append)` 的演算场](https://inet.run/playground/aW1wb3J0IExpc3QgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKdHlwZSBEaWZmTGlzdCBAVHlwZSAtLSBAVHlwZSBlbmQKCm5vZGUgZGlmZgogICdBIExpc3QgOmZyb250CiAgLS0tLS0tLQogICdBIExpc3QgOmJhY2sKICAnQSBEaWZmTGlzdCA6dmFsdWUhCmVuZAoKbm9kZSBkaWZmX2FwcGVuZAogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgRGlmZkxpc3QgOnJlc3QKICAtLS0tLS0tLQogICdBIERpZmZMaXN0IDpyZXR1cm4KZW5kCgpub2RlIGRpZmZfb3BlbgogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgTGlzdCA6bGlzdAogIC0tLS0tLS0tLS0KICAnQSBMaXN0IDpyZXR1cm4KZW5kCgpydWxlIGRpZmYgZGlmZl9hcHBlbmQKICAoZGlmZiktZnJvbnQgZGlmZiByZXR1cm4tKGRpZmZfYXBwZW5kKQogIChkaWZmX2FwcGVuZCktcmVzdCBkaWZmX29wZW4gYmFjay0oZGlmZikKZW5kCgpydWxlIGRpZmYgZGlmZl9vcGVuCiAgKGRpZmYpLWJhY2sgbGlzdC0oZGlmZl9vcGVuKQogIChkaWZmKS1mcm9udCByZXR1cm4tKGRpZmZfb3BlbikKZW5kCgppbXBvcnQgemVybyBmcm9tICJodHRwczovL2Nkbi5pbmV0LnJ1bi90ZXN0cy9kYXRhdHlwZS9OYXQuaSIKaW1wb3J0IGNvbnMgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKemVybyAoY29ucyA6dGFpbCkgemVybyBjb25zIGRpZmYgQHJvdCBAcm90IEBjb25uZWN0Cnplcm8gKGNvbnMgOnRhaWwpIHplcm8gY29ucyBkaWZmIEByb3QgQHJvdCBAY29ubmVjdApkaWZmX2FwcGVuZAoKemVybyAoY29ucyA6dGFpbCkgemVybyBjb25zIGRpZmYgQHJvdCBAcm90IEBjb25uZWN0Cnplcm8gKGNvbnMgOnRhaWwpIHplcm8gY29ucyBkaWZmIEByb3QgQHJvdCBAY29ubmVjdApkaWZmX2FwcGVuZCBAcnVuICRyZXN1bHQ)
+[去 `DiffList` 与 `(diff_append)` 的演算场](https://inet.run/playground/aW1wb3J0IExpc3QgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKdHlwZSBEaWZmTGlzdCBAVHlwZSAtLSBAVHlwZSBlbmQKCm5vZGUgZGlmZgogICdBIExpc3QgOmZyb250CiAgLS0tLS0tLQogICdBIExpc3QgOmJhY2sKICAnQSBEaWZmTGlzdCA6dmFsdWUhCmVuZAoKbm9kZSBkaWZmX2FwcGVuZAogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgRGlmZkxpc3QgOnJlc3QKICAtLS0tLS0tLQogICdBIERpZmZMaXN0IDpyZXR1cm4KZW5kCgpub2RlIGRpZmZfb3BlbgogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgTGlzdCA6bGlzdAogIC0tLS0tLS0tLS0KICAnQSBMaXN0IDpyZXR1cm4KZW5kCgpydWxlIGRpZmYgZGlmZl9hcHBlbmQKICAoZGlmZiktZnJvbnQgZGlmZiByZXR1cm4tKGRpZmZfYXBwZW5kKQogIChkaWZmX2FwcGVuZCktcmVzdCBkaWZmX29wZW4gYmFjay0oZGlmZikKZW5kCgpydWxlIGRpZmYgZGlmZl9vcGVuCiAgKGRpZmYpLWJhY2sgbGlzdC0oZGlmZl9vcGVuKQogIChkaWZmKS1mcm9udCByZXR1cm4tKGRpZmZfb3BlbikKZW5kCgppbXBvcnQgemVybyBmcm9tICJodHRwczovL2Nkbi5pbmV0LnJ1bi90ZXN0cy9kYXRhdHlwZS9OYXQuaSIKaW1wb3J0IGNvbnMgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKemVybyAoY29ucyA6dGFpbCkgemVybyBjb25zIGRpZmYgJHZhbHVlIEBjb25uZWN0IHZhbHVlCnplcm8gKGNvbnMgOnRhaWwpIHplcm8gY29ucyBkaWZmICR2YWx1ZSBAY29ubmVjdCB2YWx1ZQpkaWZmX2FwcGVuZAoKemVybyAoY29ucyA6dGFpbCkgemVybyBjb25zIGRpZmYgJHZhbHVlIEBjb25uZWN0IHZhbHVlCnplcm8gKGNvbnMgOnRhaWwpIHplcm8gY29ucyBkaWZmICR2YWx1ZSBAY29ubmVjdCB2YWx1ZQpkaWZmX2FwcGVuZCBAcnVuICRyZXN1bHQ)
 
 ```
 import List from "https://cdn.inet.run/tests/datatype/List.i"
@@ -928,12 +943,12 @@ end
 import zero from "https://cdn.inet.run/tests/datatype/Nat.i"
 import cons from "https://cdn.inet.run/tests/datatype/List.i"
 
-zero (cons :tail) zero cons diff @rot @rot @connect
-zero (cons :tail) zero cons diff @rot @rot @connect
+zero (cons :tail) zero cons diff $value @connect value
+zero (cons :tail) zero cons diff $value @connect value
 diff_append
 
-zero (cons :tail) zero cons diff @rot @rot @connect
-zero (cons :tail) zero cons diff @rot @rot @connect
+zero (cons :tail) zero cons diff $value @connect value
+zero (cons :tail) zero cons diff $value @connect value
 diff_append @run $result
 ```