如何用规范表示法定义返回依赖于参数的类型的函数？

你的核心需求是让函数F返回的Combinator元数与第一个Int参数的值绑定，原函数签名为：

F :: Int -> List<Int> -> Combinator

你给出的两种伪代码中，第二种写法是正确的方向：

F :: Int(a) -> List<Int> -> Combinator<a>

具体解释： #

• 第一种写法F :: List<Int> -> (Int(a) -> Combinator<a>)逻辑颠倒：它先接收列表参数，再返回一个“以指定元数的Int为输入”的函数，完全不符合你“第一个参数是元数Int”的原始设计。
• 第二种写法直接将第一个Int参数标记为值级变量a，并让返回的Combinator的元数绑定到a上，精准匹配你的需求。

依赖类型中的既定表示法 #

在Idris、Agda这类原生支持依赖类型的语言中，标准写法会直接在函数参数里声明值变量，同时将其作为类型参数使用，不需要把Int写成带参数的形式，示例如下：

F : (a : Int) -> List Int -> Combinator a

这里(a : Int)明确声明a是一个Int类型的值变量，同时它可以直接作为类型级参数传递给Combinator，清晰建立“参数值决定返回类型结构”的依赖关系。

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