Skip to content

Commit

Permalink
doc(example): extract code for lambda
Browse files Browse the repository at this point in the history
  • Loading branch information
@peter-jerry-ye
peter-jerry-ye committed Dec 4, 2024
1 parent 5d8ee28 commit 83d8006
Show file tree
Hide file tree
Showing 8 changed files with 453 additions and 183 deletions.
136 changes: 66 additions & 70 deletions next/locales/zh_CN/LC_MESSAGES/tutorial.po
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ msgid ""
msgstr ""
"Project-Id-Version: MoonBit Document \n"
"Report-Msgid-Bugs-To: \n"
"POT-Creation-Date: 2024-12-03 16:21+0800\n"
"POT-Creation-Date: 2024-12-04 11:18+0800\n"
"PO-Revision-Date: YEAR-MO-DA HO:MI+ZONE\n"
"Last-Translator: FULL NAME <EMAIL@ADDRESS>\n"
"Language: zh_CN\n"
Expand Down Expand Up @@ -2614,18 +2614,18 @@ msgid ""
"}\n"
msgstr ""

#: ../../tutorial/example/lambda/index.md:27
#: ../../tutorial/example/lambda/index.md:25
msgid ""
"Concepts encountered in daily programming such as boolean values, if "
"expressions, natural number arithmetic, and even recursion can all be "
"implemented using Lambda expressions. However, this is not the focus of "
"this article. Interested readers can refer to:"
"this article."
msgstr ""

#: ../../tutorial/example/lambda/index.md:29
#: ../../tutorial/example/lambda/index.md:28
msgid ""
"Programming with Nothing：[https://tomstu.art/programming-with-"
"nothing](https://tomstu.art/programming-with-nothing)"
"Interested readers can refer to: [Programming with "
"Nothing](https://tomstu.art/programming-with-nothing)"
msgstr ""

#: ../../tutorial/example/lambda/index.md:31
Expand Down Expand Up @@ -2711,7 +2711,7 @@ msgid ""
"variables:"
msgstr ""

#: ../../tutorial/example/lambda/index.md:67
#: ../../tutorial/example/lambda/index.md:69
msgid ""
"// (λx.E) T => E.subst(x, T)\n"
"fn subst(self : Term, var : String, term : Term) -> Term {\n"
Expand All @@ -2731,31 +2731,31 @@ msgid ""
"}\n"
msgstr ""

#: ../../tutorial/example/lambda/index.md:86
#: ../../tutorial/example/lambda/index.md:88
msgid ""
"Next, I'll introduce a less popular but somewhat convenient method: de "
"Bruijn index."
msgstr ""

#: ../../tutorial/example/lambda/index.md:88
#: ../../tutorial/example/lambda/index.md:90
msgid "De Bruijn Index"
msgstr ""

#: ../../tutorial/example/lambda/index.md:90
#: ../../tutorial/example/lambda/index.md:92
msgid ""
"De Bruijn index is a technique for representing variables in Lambda terms"
" using integers. Specifically, it replaces specific variables with "
"Lambdas between the variable and its original imported position."
msgstr ""

#: ../../tutorial/example/lambda/index.md:92
#: ../../tutorial/example/lambda/index.md:94
msgid ""
"λx.(λy.x (λz.z z))\n"
"\n"
"λ.(λ.1 (λ.0 0))\n"
msgstr ""

#: ../../tutorial/example/lambda/index.md:98
#: ../../tutorial/example/lambda/index.md:100
msgid ""
"In the example above, there is one Lambda `λy` between the variable `x` "
"and its introduction position `λx`, so `x` is replaced with `1`. For "
Expand All @@ -2766,19 +2766,19 @@ msgid ""
" by the number of nested Lambdas."
msgstr ""

#: ../../tutorial/example/lambda/index.md:100
#: ../../tutorial/example/lambda/index.md:102
msgid ""
"The same variable may be replaced with different integers in different "
"positions."
msgstr ""

#: ../../tutorial/example/lambda/index.md:102
#: ../../tutorial/example/lambda/index.md:104
msgid ""
"We define a new type `TermDBI` to represent Lambda terms using de Bruijn "
"indices:"
msgstr ""

#: ../../tutorial/example/lambda/index.md:104
#: ../../tutorial/example/lambda/index.md:106
msgid ""
"enum TermDBI {\n"
" Var(String, Int)\n"
Expand All @@ -2793,22 +2793,22 @@ msgid ""
"form is painful, so we need to write a function `bruijn()` to convert "
"`Term` to `TermDBI`. This is also why there is still a `String` in the "
"definition of the `TermDBI` type, so that the original variable name can "
"be used for its `to_string` method, making it easy to print and view the "
"evaluation results with `println`."
"be used for its `Show` implementation, making it easy to print and view "
"the evaluation results with `println`."
msgstr ""

#: ../../tutorial/example/lambda/index.md:114
msgid ""
"fn to_string(self : TermDBI) -> String {\n"
"impl Show for TermDBI with output(self : TermDBI, logger) -> Unit {\n"
" match self {\n"
" Var(name, _) => name\n"
" Abs(name, body) => \"(\\\\\\{name}.\\{body})\"\n"
" App(t1, t2) => \"\\{t1} \\{t2}\"\n"
" Var(name, _) => logger.write_string(name)\n"
" Abs(name, body) => logger.write_string(\"(\\\\\\{name}.\\{body})\")\n"
" App(t1, t2) => logger.write_string(\"\\{t1} \\{t2}\")\n"
" }\n"
"}\n"
msgstr ""

#: ../../tutorial/example/lambda/index.md:124
#: ../../tutorial/example/lambda/index.md:121
msgid ""
"To simplify implementation, if the input `Term` contains free variables, "
"the `bruijn()` function will report an error directly. MoonBit provides a"
Expand All @@ -2817,77 +2817,77 @@ msgid ""
"respectively."
msgstr ""

#: ../../tutorial/example/lambda/index.md:126
#: ../../tutorial/example/lambda/index.md:123
msgid "Readers familiar with Rust should find this familiar."
msgstr ""

#: ../../tutorial/example/lambda/index.md:128
#: ../../tutorial/example/lambda/index.md:126
msgid "fn bruijn(self : Term) -> Result[TermDBI, String]\n"
msgstr ""

#: ../../tutorial/example/lambda/index.md:132
#: ../../tutorial/example/lambda/index.md:130
msgid ""
"We take a clumsy approach to save variable names and their associated "
"nesting depth. First, we define the `Index` type:"
msgstr ""

#: ../../tutorial/example/lambda/index.md:134
#: ../../tutorial/example/lambda/index.md:132
msgid ""
"struct Index {\n"
" name : String\n"
" depth : Int\n"
"}\n"
msgstr ""

#: ../../tutorial/example/lambda/index.md:141
#: ../../tutorial/example/lambda/index.md:138
msgid ""
"Then we write a helper function to find the corresponding `depth` based "
"on a specific `name` from `List[Index]`:"
msgstr ""

#: ../../tutorial/example/lambda/index.md:143
#: ../../tutorial/example/lambda/index.md:140
msgid ""
"// Find the first depth corresponding to varname in the environment\n"
"// Find the depth corresponding to the first varname in the environment\n"
"fn find(map : @immut/list.T[Index], varname : String) -> Result[Int, "
"String] {\n"
" match map {\n"
" Nil => Err(varname) // abort(\"variable '(varname)' not found\")\n"
" Cons(i, rest) => {\n"
" Nil => Err(varname)\n"
" Cons(i, rest) =>\n"
" if i.name == varname {\n"
" Ok(i.depth)\n"
" } else {\n"
" find(rest, varname)\n"
" }\n"
" }\n"
" }\n"
"}\n"
"\n"
msgstr ""

#: ../../tutorial/example/lambda/index.md:159
#: ../../tutorial/example/lambda/index.md:147
msgid "Now we can complete the `bruijn()` function."
msgstr ""

#: ../../tutorial/example/lambda/index.md:161
#: ../../tutorial/example/lambda/index.md:149
msgid ""
"Handling `Var` is the simplest, just look up the table to find the "
"corresponding `depth`."
msgstr ""

#: ../../tutorial/example/lambda/index.md:162
#: ../../tutorial/example/lambda/index.md:150
msgid ""
"`Abs` is a bit more complicated. First, add one to the `depth` of all "
"`index` in the list (because the Lambda nesting depth has increased by "
"one), and then add `{ name : varname, depth : 0 }` to the beginning of "
"the list."
msgstr ""

#: ../../tutorial/example/lambda/index.md:163
#: ../../tutorial/example/lambda/index.md:151
msgid ""
"`App` succeeds when both sub-items can be converted; otherwise, it "
"returns an `Err`."
msgstr ""

#: ../../tutorial/example/lambda/index.md:165
#: ../../tutorial/example/lambda/index.md:153
msgid ""
"fn go(m : @immut/list.T[Index], t : Term) -> Result[TermDBI, String] {\n"
" match t {\n"
Expand All @@ -2899,103 +2899,99 @@ msgid ""
" }\n"
" }\n"
" Abs(varname, body) => {\n"
" let m = m.map(fn (index){\n"
" { name : index.name, depth : index.depth + 1 }\n"
" }).cons({ name : varname, depth : 0 })\n"
" let m = @immut/list.Cons(\n"
" { name: varname, depth: 0 },\n"
" m.map(fn(index) { { name: index.name, depth: index.depth + 1 } "
"}),\n"
" )\n"
" let res = go(m, body)\n"
" match res {\n"
" Err(name) => Err(name)\n"
" Ok(term) => Ok(Abs(varname, term))\n"
" }\n"
" }\n"
" App(e1, e2) => {\n"
" App(e1, e2) =>\n"
" match (go(m, e1), go(m, e2)) {\n"
" (Ok(e1), Ok(e2)) => Ok(App(e1, e2))\n"
" (Err(name), _) => Err(name)\n"
" (_, Err(name)) => Err(name)\n"
" }\n"
" }\n"
" }\n"
"}\n"
"\n"
"go(Nil, self)\n"
msgstr ""

#: ../../tutorial/example/lambda/index.md:197
#: ../../tutorial/example/lambda/index.md:160
msgid "Reduce on TermDBI"
msgstr ""

#: ../../tutorial/example/lambda/index.md:199
#: ../../tutorial/example/lambda/index.md:162
msgid "Reduction mainly deals with App, i.e., calls:"
msgstr ""

#: ../../tutorial/example/lambda/index.md:201
#: ../../tutorial/example/lambda/index.md:164
msgid ""
"fn eval(self : TermDBI) -> TermDBI {\n"
" match self {\n"
" App(t1, t2) => {\n"
" App(t1, t2) =>\n"
" match (eval(t1), eval(t2)) {\n"
" (Abs(_, t1), t2) => eval(subst(t1, t2))\n"
" (t1, t2) => App(t1, t2)\n"
" }\n"
" }\n"
" Abs(_) => self\n"
" otherwise => abort(\"eval(): \\{otherwise} \")\n"
" // eval should not encounter free variables\n"
" // Eval should not encounter any free variables\n"
" _ => panic()\n"
" }\n"
"}\n"
"\n"
msgstr ""

#: ../../tutorial/example/lambda/index.md:217
#: ../../tutorial/example/lambda/index.md:170
msgid ""
"First, attempt reduction on both sub-items, then see if `eval(t1)` "
"results in a Lambda. If so, perform one step of variable substitution "
"(via the subst function) and then continue simplifying. For Lambdas "
"(`Abs`), simply return them as they are."
msgstr ""

#: ../../tutorial/example/lambda/index.md:219
#: ../../tutorial/example/lambda/index.md:172
msgid ""
"The implementation of the subst function becomes much simpler when we "
"don't need to consider free variables. We just need to keep track of the "
"current depth recursively and compare it with the encountered variables. "
"If they match, it's the variable to be replaced."
msgstr ""

#: ../../tutorial/example/lambda/index.md:221
#: ../../tutorial/example/lambda/index.md:174
msgid ""
"fn subst(t1 : TermDBI, t2 : TermDBI) -> TermDBI {\n"
" fn go(t1 : TermDBI, t2 : TermDBI, depth : Int) -> TermDBI {\n"
" match t1 {\n"
" Var(name, d) => {\n"
" if d == depth {\n"
" t2\n"
" } else {\n"
" t1\n"
" }\n"
" }\n"
" Abs(name, t) => {\n"
" Abs(name, go(t, t2, depth + 1))\n"
" }\n"
" App(tl, tr) => {\n"
" App(go(tl, t2, depth), go(tr, t2, depth))\n"
" }\n"
" Var(_, d) => if d == depth { t2 } else { t1 }\n"
" Abs(name, t) => Abs(name, go(t, t2, depth + 1))\n"
" App(tl, tr) => App(go(tl, t2, depth), go(tr, t2, depth))\n"
" }\n"
" }\n"
"\n"
" go(t1, t2, 0)\n"
"}\n"
"\n"
msgstr ""

#: ../../tutorial/example/lambda/index.md:244
#: ../../tutorial/example/lambda/index.md:180
msgid ""
"The full code: "
"[try.moonbitlang.com/#b52b528b](https://try.moonbitlang.com/#b52b528b)"
"The full code: [GitHub repository](https://github.com/moonbitlang"
"/moonbit-docs/tree/main/next/sources/lambda-expression/src/top.mbt)"
msgstr ""
"完整代码请查看 [GitHub 代码仓库](https://github.com/moonbitlang/moonbit-"
"docs/tree/main/next/sources/lambda-expression/src/top.mbt)。"

#: ../../tutorial/example/lambda/index.md:246
#: ../../tutorial/example/lambda/index.md:182
msgid "Improvement"
msgstr ""

#: ../../tutorial/example/lambda/index.md:248
#: ../../tutorial/example/lambda/index.md:184
msgid ""
"When mapping variable names to indices, we used the "
"`@immut/list.T[Index]` type and updated the entire list every time we "
Expand Down
2 changes: 2 additions & 0 deletions next/sources/lambda-expression/.gitignore
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
target/
.mooncakes/
Loading

0 comments on commit 83d8006

Please sign in to comment.