如何在Idris中将函数类型声明拆分为多行？

嘿，在Idris里做类型驱动开发的时候，长到爆的类型声明确实是个头疼的问题——就像你贴的这个例子，屏幕窄点根本看不全：

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

下面给你几个实用的小技巧，能让这些长类型清爽不少：

• 合理换行对齐：直接把每个参数拆分到单独一行，保持箭头->对齐，Idris编译器完全认可这种格式，可读性瞬间提升。
• 用类型别名简化重复结构：对于像Vect rowCount (Vect columnCount element)这种重复出现的复杂类型，我们可以先定义一个类型别名：

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

  之后addMatrices的类型就能简化成这样：

  addMatrices : Matrix rowCount columnCount element 
             -> Matrix rowCount columnCount element 
             -> Matrix rowCount columnCount element
  

  是不是简洁太多了？
• 利用隐式参数减少冗余：如果rowCount、columnCount这类参数能被Idris自动推导出来，我们可以把它们改成隐式参数（用大括号{}包裹）：

  addMatrices : {rowCount, columnCount : Nat} 
             -> Matrix rowCount columnCount element 
             -> Matrix rowCount columnCount element 
             -> Matrix rowCount columnCount element
  

  这样不仅类型声明更紧凑，调用函数时还不用手动传递这些Nat参数，一举两得。

内容的提问来源于stack exchange，提问作者Alexander Novikov