From 1e7a0525d7ff65f808f24cbf353adbbdf0e62c28 Mon Sep 17 00:00:00 2001 From: Xie Yuheng Date: Tue, 5 Sep 2023 11:58:50 +0800 Subject: [PATCH] =?UTF-8?q?[docs]=20=E5=8F=8D=E5=BA=94=E7=BD=91=E7=BC=96?= =?UTF-8?q?=E7=A8=8B=20--=20=E5=AE=8C=E6=88=90=20`List`=20=E7=9A=84?= =?UTF-8?q?=E8=AE=B2=E8=A7=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- TODO.md | 1 - ...24\347\275\221\347\274\226\347\250\213.md" | 33 ++++++++++++++----- 2 files changed, 24 insertions(+), 10 deletions(-) diff --git a/TODO.md b/TODO.md index a2f106b3..da40390e 100644 --- a/TODO.md +++ b/TODO.md @@ -1,6 +1,5 @@ # articles -[docs] 反应网编程 -- 完成 `List` 的讲解 [docs] 反应网编程 -- 完成 `DiffList` 的讲解 [docs] 反应网编程 -- 总结 diff --git "a/docs/articles/\345\217\215\345\272\224\347\275\221\347\274\226\347\250\213.md" "b/docs/articles/\345\217\215\345\272\224\347\275\221\347\274\226\347\250\213.md" index b186300a..21978975 100644 --- "a/docs/articles/\345\217\215\345\272\224\347\275\221\347\274\226\347\250\213.md" +++ "b/docs/articles/\345\217\215\345\272\224\347\275\221\347\274\226\347\250\213.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 ```