Idris中如何命名函数返回值？为何参数命名语法不适用？

这个问题问得很到位！我刚接触Idris的时候也好奇过这个语法设计，咱们一步步拆解来看：

首先得搞懂Idris函数类型里参数命名的本质：那些带名字的参数声明(str : String)其实是绑定变量到类型，目的是让你在函数体或者后续的参数类型里能引用这个变量（比如在依赖类型场景下，后面的参数类型可以依赖前面的参数值）。

而函数类型的结构是一串参数绑定，最后以返回类型收尾——也就是说，->是用来分隔参数绑定和后续类型（要么是下一个参数，要么是返回值）的。当你写(str : String) -> (lengthOfStr : Nat)时，编译器会把(lengthOfStr : Nat)当成一个新的参数绑定，所以它还在等下一个->来指定返回类型，这就触发了"unexpected end of input expecting "->""的错误。简单说：返回值位置不是参数绑定的区域，语法上不支持这种命名方式。

虽然不能直接在返回类型位置命名，但有几个实用的办法能达到类似的效果：

• 用文档字符串标记：这是最常用的方案。Idris支持用|||开头的文档字符串，你可以在里面用@name来指代返回值，哪怕它没在类型里命名：

  ||| Returns the number of characters in a given string.
  ||| @str the input string to measure
  ||| @lengthOfStr the total count of characters in `str`
  length : String -> Nat
  length str = length' str 0
    where
      length' : String -> Nat -> Nat
      length' "" acc = acc
      length' (c :: cs) acc = length' cs (acc + 1)
  

  Idris的文档生成工具（比如IdrisDoc）会识别这些@标记，生成的文档里会清晰对应到返回值的含义，阅读代码的人也能一眼看明白。

• 用带命名字段的记录封装返回值：如果返回值的命名需要在代码层面被引用（而不只是文档里），可以定义一个记录类型来包裹返回值，这样字段名就是返回值的"命名"：

  ||| A record pairing a string with its character count
  record StringLengthResult where
    constructor MkStringLengthResult
    inputString : String
    calculatedLength : Nat
  
  ||| Computes the length of a string and returns it in a named record
  calculateStringLength : (str : String) -> StringLengthResult
  calculateStringLength str = MkStringLengthResult str (length str)
  

  调用这个函数后，你可以通过calculatedLength字段直接访问返回的长度，既满足了文档可读性，也让代码更具语义性。

• 在类型后加注释说明：如果只是想让代码本身更清晰，直接在返回类型后面加注释就行，简单直接：

  ||| Gets the character count of a string
  ||| @str the input string
  length : (str : String) -> Nat -- ^ calculatedLength: number of characters in `str`
  length str = ...
  

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