在 Idris 中多行写入函数类型答案

【问题标题】：Write function type on multiple lines in Idris在 Idris 中多行写入函数类型
【发布时间】：2020-06-29 15:14:40
【问题描述】：

如何在 Idris 中将类型声明拆分为多行？类型应该推动发展。所以它们可能会变得很长并且不适合屏幕。喜欢这个：

addMatrices : (augent : Vect rowCount (Vect columnCount element)) -> (addend: Vect rowCount (Vect columnCount element)) -> Vect rowCount (Vect columnCount element)

【问题讨论】：

Al.G.感谢您提出您的解决方案。我会尝试在 Idris 中找到更多关于别名的信息。

标签： idris

【解决方案1】：

要仅使用格式，您可以照常进行，

addMatrices : (augent : Vect rowCount (Vect columnCount element)) -> 
              (addend: Vect rowCount (Vect columnCount element)) -> 
              Vect rowCount (Vect columnCount element)

docs 说

新的声明必须以与前一个声明相同的缩进级别开始。

同样，book 仅在第 2.4.1 节中说 空白意义：布局规则，

...在任何定义和声明列表中，都必须从完全相同的列开始。

由于新行不是新声明，我认为这意味着新行可以从任何缩进级别开始，所以

addMatrices : (augent : Vect rowCount (Vect columnCount element)) -> 
       (addend: Vect rowCount (Vect columnCount element)) -> 
          Vect rowCount (Vect columnCount element)

其他变体也是有效的。

或者，根据 Al.G. 的评论，您可以使用类型别名，但如果 rowCount 和 columnCount 不在范围内，我猜它们不适合您，您将需要一个类型级函数，它是类型别名的泛化。这是一个返回类型的函数。

Matrix : Nat -> Nat -> Type -> Type
Matrix rows cols elem = Vect rows (Vect cols elem)

那么你就有了

addMatrices : (augent : Matrix rowCount columnCount element) -> 
              (addend: Matrix rowCount columnCount element) -> 
              Matrix rowCount columnCount element

这并不短。

说实话，我会考虑使用较短的名称并利用任何明显的上下文

addMatrices : (augent : Vect r (Vect c elem)) -> (addend: Vect r (Vect c elem)) -> Vect r (Vect c elem)

【讨论】：

【解决方案2】：

我在检查 Atom 中的类型时发现了这一点：

addMatrices : (augent : Vect rowCount (Vect columnCount element)) -> 
              (addend: Vect rowCount (Vect columnCount element)) -> 
              Vect rowCount (Vect columnCount element)

【讨论】：