函数类型的类型列表

Question

我想创建一个给定函数类型（例如String -> Nat -> Bool）的函数，它将返回与该函数类型相对应的类型列表（例如[String, Nat, Bool]）。据推测，这样一个函数的签名将是Type -> List Type，但我正在努力确定如何实现它。

Answer 1

我不相信它可以一般地完成，因为你不能在功能上进行模式匹配。你也不能检查功能的类型。这不是什么依赖类型。就像在Haskell或OCaml中一样，你可以用函数实际做的唯一事情是将它应用于某个参数。但是，我设计了一些可能会做的技巧：

myFun : {a, b : Type} -> (a -> b) -> List Type
myFun {a} {b} _ = [a, b]

现在的问题是a -> b是唯一可以匹配任意函数的签名。但是，当然，对于arity高于1的函数，它的行为方式并不像你想要的那样：

> myFun (+)
[Integer, Integer -> Integer] : List Type

因此，需要对自身进行某种递归调用以提取更多参数类型：

myFun : {a, b : Type} -> (a -> b) -> List Type
myFun {a} {b} _ = a :: myFun b

这里的问题是b是一个任意类型，不一定是函数类型，我无法想出动态检查它是否是一个函数，所以我想这与Idris一样多。

但是，动态检查类型（至少在我看来）并不是静态类型语言所需要的功能。毕竟静态类型的所有要点是预先指定函数可以处理什么类型的参数，并防止在编译时使用无效参数调用函数。所以基本上你可能根本不需要它。如果您指定了更宏伟的目标，那么有人可能会向您展示正确的方法。