Tutorial: typesfuns

[OlingCat]

• 初译
• 润色
• 初校
• 二校
• 终稿

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L276

- 这意味着它可以优化它们的表示以及像 ``plus`` 和 ``mult`` 这样的函数。
+ 这意味着 Idris 可以优化它们的表示以及像 ``plus`` 和 ``mult`` 这样的函数。

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L316

-    任何外部作用域中可见的名字，在 ``where`` 从句中也可见
-    （除非它们被重新定义过，例如这里的 ``xs``）。
+    任何外部作用域中可见，且没有被重新被定义过的名字，在 ``where`` 从句中也可见。
+    （这里的 ``xs`` 被重新定义了）

-    **形参（Parameter）**，那么仅当它在类型中出现时才会在 ``where``
+    **形参（Parameter）**，那么当它仅在类型中出现时才会在 ``where``

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L519

-（在实践中，通常在不同的模块内），像这样重载的专用名就会被 Idris 所接受。
+（在实践中，通常在不同的模块内），Idris 可以接受像这样重载的专用名。

- 混淆的构造器名称通常可根据上下文来解决。
+ 有歧义的构造器名称通常可根据上下文来解决。 

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L573

-    (++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
+    (++) (x :: xs) ys = x :: xs ++ xs -- 有误

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L717

- 元素向量。不过这里还有两个名字：``n`` 和 ``a``，它们并未显示地声明。``index``
+ 元素向量。不过这里还有两个名字：``n`` 和 ``a``，它们并未显式地声明。``index``

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L748

- 实际上，无论是隐式还是显式，任何参数都可以给定一个名称。我们可以将``index``
+ 实际上，无论是隐式还是显式，任何参数都可以给定一个名称。我们可以将 ``index``

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L788

- 例如，我们可能希望在以下定义中描述隐式参数的类型，它为向量定义了谓词（它也在
+ 例如，我们可能希望在以下定义中描述隐式参数的类型，它为向量定义了前提（它也在

https://en.wiktionary.org/wiki/predicate
此处的predicate属于（2）logic，不属于（1）grammar

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L802

同L788

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L833

- 如果相同的隐含参数被大量使用，会导致定义难以阅读。为避免此问题，可用 ``using``
+ 如果相同的隐式参数被大量使用，会导致定义难以阅读。为避免此问题，可用 ``using``

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L880

I/O -> 输入输出？

RE: 没必要吧？程序员都知道啥是 I/O

Re: Re: OK.

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L894

纯粹语言 (pure language)
副作用 (side effect)

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L906

- 我们先无视 ``IO`` 抽象的定义，尽管它有效地描述了被执行的 I/O 操作是什么，
+ 我们先给出一个 ``IO``  的抽象定义。它实质上描述了被执行的 I/O 操作是什么，

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L1070

- 余数据类型通过将递归参数标记为潜在无穷来定义无穷数据结构。对于一个余数据类型
+ 我们可以通过余数据类型，将递归参数标记为潜在无穷，来定义无穷数据结构。对于一个余数据类型

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L1105

- 要重点注意：codata 不允许创建无穷互用的递归数据结构。
+ 要重点注意：余数据类型不允许创建无穷互用的递归数据结构。

RE: 我想这里的 codata 更多指下文代码中的关键字。

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L1136

同L1105

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L1481

同L788

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L1591

- 记录以及记录中的字段可拥有依赖类型。更新允许更改字段的类型，前提是结果是良定型的。
+ 记录以及记录中的字段可拥有依赖类型。更新允许更改字段的类型，前提是结果是良类型的。

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L1684

- 使用前面的 ``class`` 记录，班级的大小可用 ``Vect`` 及通过 size
+ 使用前面的 ``class`` 记录，class 的大小可用 ``Vect`` 及通过 size

RE: 这里其实可以用班级来指代文中的 class

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L1701

同L1684

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L1822

- 我们接着析构它返回的序对， 并移除第二个字符串的第一个字符。
+ 我们接着拆开它返回的序对， 并移除第二个字符串的第一个字符。

RE: 对于序对这个数据结构，这里确实可以用析构。

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L1859

- **限制：** ``case`` 构造用于中间表达式的简单分析，一次避免编写辅助函数，
+ **限制：** ``case`` 构造用于中间表达式的简单分析，以此避免编写辅助函数，

[fangyi-zhou]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L1105

- 要重点注意：codata 不允许创建无穷互用的递归数据结构。
+ 要重点注意：余数据类型不允许创建无穷互用的递归数据结构。

RE: 我想这里的 codata 更多指下文代码中的关键字。

我还是觉得应该翻译此处的codata，如果表示关键字的话，应该是用 backticks 包起来的。

[OlingCat]

我还是觉得应该翻译此处的codata，如果表示关键字的话，应该是用 backticks 包起来的。

那就用 backticks 包起来吧，好多引用代码中函数名或参数的地方都没有 `` = =||

[fangyi-zhou]

我觉得根据上下文这里需要翻译，因为原文描述的是余数据类型的限制，而不是关键字的限制。 Best Fangyi Zhou RE: 好吧= = Issue 的回复引用机制真是恶心= =||

…

On 17 Mar 2018, at 11:11, Oling Cat ***@***.***> wrote: 我还是觉得应该翻译此处的codata，如果表示关键字的话，应该是用 backticks 包起来的。 那就用 backticks 包起来吧，好多引用代码中函数名或参数的地方都没有 `` = =|| — You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

[OlingCat]

https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L788

• 例如，我们可能希望在以下定义中描述隐式参数的类型，它为向量定义了谓词（它也在

• 例如，我们可能希望在以下定义中描述隐式参数的类型，它为向量定义了前提（它也在
  https://en.wiktionary.org/wiki/predicate
  此处的predicate属于（2）logic，不属于（1）grammar

咱又自己考虑了一下，它虽然在类型中，但语义上确实是一个谓词。

谓词，用来描述或判定客体性质、特征或者客体之间关系的词项。根据《现代汉语》的定义,汉语的体词包括名词,数词,量词；汉语的谓词包括动词和形容词。谓，在古文中与「是」等同，表示判断。

在这里，IsElem 根据构造器参数构造出一个类型Here或There来表示判断，这也是把语义编码成类型的一个例子。

[fangyi-zhou]

向量的谓词是什么呢？ 我平时阅读的中文文献不多，但这样的说法让我觉得有一点奇怪。 其他译者有什么意见么？

…

On Mon, 26 Mar 2018 at 22:41 Oling Cat ***@***.***> wrote: https://github.com/Idris-zh/Idris-dev/blame/master/docs/tutorial/typesfuns.rst#L788 - 例如，我们可能希望在以下定义中描述隐式参数的类型，它为向量定义了谓词（它也在 - 例如，我们可能希望在以下定义中描述隐式参数的类型，它为向量定义了前提（它也在 https://en.wiktionary.org/wiki/predicate 此处的predicate属于（2）logic，不属于（1）grammar 咱又自己考虑了一下，它虽然在类型中，但语义上确实是一个谓词。 谓词，用来描述或判定客体性质、特征或者客体之间关系的词项。根据《现代汉语》的定义,汉语的体词包括名词,数词,量词；汉语的谓词包括动词和形容词。谓，在古文中与「是」等同，表示判断。 在这里，IsElem 根据构造器参数构造出一个类型Here或There来表示判断，这也是把语义编码成类型的一个例子。 — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#21 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AHdBDy5nbu8A1qIokl2VM-zMOr7bc3f7ks5tiP4XgaJpZM4Stqwa> .

[OlingCat]

不是向量的谓词，而是对向量的元素定义了谓词。即 a 是向量 V 中的元素。