我正在编写一些伪代码,并且想要指定具有关联数量的函数类型
Combinator
,该数量与第一个 Int
参数相同:
F :: Int -> List<Int> -> Combinator
我在想,如果我有某种方法来编写依赖类型,那么我可以编写一些像这样的伪代码:
F :: List<Int> -> (Int(a) -> Combinator<a>)
-- or even
F :: Int(a) -> List<Int> -> Combinator<a>
我该如何表达呢?是否有任何既定的符号来指定函数返回其参数的依赖类型?
在 Iris 中,拼写是
F : (arity : Int) -> List Int -> Combinator arity
https://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#dependent-types