types - 依赖类型可以对 n-arg 函数进行抽象吗？

Question

在动态类型语言中，我可以创建一个将函数作为参数并返回一个函数的函数。

例如 memoize Clojure 中的函数。

(def memoized-fn 
  (memoize any-function))

在本例中， memoize不在乎什么功能 any-function指或它接受多少个参数*。

* 实际上，它并不关心传入什么， (memoize 10) Clojure 是有效的，但是尝试使用返回的值只会引发异常。

在以前的生活中，我想用静态类型语言创建类似的东西，就我而言，我使用的是 Scala，而 Scala 有很多 FunctionN类型(我相信 1 个 arg 到 23 个)，但是如果函数之间没有任何关系，似乎无法利用它们的功能性并创建单个通用函数。

最后我有这样的事情 *

def m(fn: Function1[A,Z]) : Function1[A,Z]
def m(fn: Function2[A,B,Z]) : Function2[A,B,Z]
....
def m(fn: Function23[A,B,....,Z]) : (fn: Function23[A,B,....,Z])

(实际上，我在 Fn 4 或 5 附近停了下来，因为虽然我很高兴 Function23 的存在，但我从来不想真正使用它。)

* 这也可能是伪 Scala 代码，我已经有一段时间没有写了。

回到现在:我知道使用依赖类型我可以创建一个函数，该函数接受一个参数化的参数。一个很好的例子似乎是一个函数，它接受一个任何类型和大小为 n 的列表，并返回一个相同大小为 n 的列表。

我可以用同构列表(大小为 n 的 A 类列表)来理解这一点，但我不知道异构列表是否有可能。

由此我假设我可以创建一个函数，该函数采用相同类型的 n 个参数。类似的东西:

def m(fn: Function[n,A]): Function[n,A]

我想我的实际问题是:依赖值能否以异构方式影响类型的数量？

另请注意:请将上面使用的备忘录示例和语言仅作为我想法的示例，我不是在问如何在静态类型语言中进行备忘录，而是以备忘录代码为例提出更高级别的问题。

* 请原谅我在这个问题上缺乏更好的词汇，我仍在学习很多。也欢迎提出编辑/改进建议。

Answer 1

依赖类型(pis)基本上是函数空间(箭头)的“增强”形式。

如果你看到:

Pi x : T. T(x)

然后它的类型基本上是在说“给我一个类型为 T 的 x，我会给你类型为 T(x) 的东西”

在退化情况下 T没有任何 x 的实例在它的主体中，这相当于 T1 -> T2在其他语言中(用 T1 代替上面 x 中的东西)。对您的问题的简单回答是，不，您通常不能增加类型中的“箭头数量”，但是如果您有这个，您可以做一些基本上就是这样的事情。

Pi x : nat. listoflength(x)

哪里 listoflength是生成长度 x 的列表(某种类型，可能是另一个参数)的东西.例如，您可以使用 sigma 类型(例如，列表的长度作为 Prop 参数 ala this technique )来实现它。问题在于参数必须是同构类型。另一种方法是创建一个函数，给定一个参数，返回一个元组 n事物，每个事物都有某种类型。

基本问题是，如果你给出一个具体的 n ，那么您需要能够说，“我接受 n 参数，这里是它们的类型”，以使所有类型算术运算都能完成。

因此，虽然您不能创建任意数量的箭头，但您可以创建一些东西来生成一个将元组作为其输入的函数(我想如果您知道 n ，您可以在它被使用的地方取消它) .

在实际依赖类型的编程中，我不知道这会有多有用(我没有证据说它没有用)但我可以看到采用特定大小列表的函数的情况，其中大小必须有一些静态计算来证明它们“匹配”。在您想要接受异构输入类型的情况下，在实践中对此进行推理可能会很复杂，我通常会尽量避免这种情况作为编码实践的问题。在可以拥有可变数量参数的动态语言中，用例似乎可能让您在道德上轻松“重载”函数，但在依赖类型的语言中，您从中获得的任何符号便利似乎都将丢失因为您必须证明您正确使用了实例。