你可以创建函数来以依赖类型语言返回一个依赖项的函数吗？ [英] Can you create functions that return functions of a dependent arity in a dependently typed language?

问题描述

从我所了解的依赖类型中，我认为它应该是可能的，但我从来没有在依赖类型语言中看到过这样的例子，所以我不确定从哪里开始。

我想要的是一个形式的函数：

pre $ f $ f [Int] - > （Int→> Bool）
f：[Int] - > （Int→> Int→> Bool）
f：[Int] - > （Int→> Int→> Int→> Bool）

p>

该函数获取n Ints 的列表，并返回一个谓词n作为参数的谓词函数。在依赖类型语言中，这种事情是可能的吗？如何实现这样的功能？

解决方案

创建不同的arity函数时，通常需要一个从值到类型的函数。在这种情况下，我们需要一个从 List （或简单地ℕ - 列表长度）到 Set ：

 谓词：ℕ→设置
谓词零= Bool 
 Predicate（suc n）=ℕ→谓词n 
  

这使我们可以创建不同的类型为每个数字：

 谓语0 = Bool 
谓语1 =ℕ→Bool 
谓语2 = ℕ→ℕ→Bool 
  - 依此类推
  

---

现在，我们如何使用 Predicate 来表达 f 的类型？由于我们处于依赖类型语言，因此我们可以自由使用类型中的值级函数。所以长度似乎是天作之合：

  f：（l ：列表ℕ）→谓词（长度为l）
  

现在，您没有指定任何特定的 f ，但是为了这个例子，我要实现一个。假设我们想检查相应位置上的所有数字（即列表中第一个元素的函数的第一个参数）是否相等。

I选择了一个相当简单的函数，所以实现将非常简单。但请注意，这些类型的函数使用的各种技巧与用于实现带有类型类的可变参数函数（在Haskell中）不同。

当给出一个空列表时，我们将只需返回 true ：

  f [] = true 
  

对于非空列表的情况，我们创建一个函数，其中一个参数名为 n ，然后将它与列表的头部进行比较（ m ）。如果这些数字不相等，我们将快捷键 f 的其余部分，并返回一个忽略所有其他数字的函数，并简单地返回 false ;如果这些数字是相同的，我们将继续列表的其余部分：

  f（m∷ms）=λ n→λ
 {（yes _）→f ms 
; （no _）→always-false 
} 
  

辅助函数 always-false ：

  always-false：∀{n}→谓词n 
 always-false {zero} = false 
 always-false {suc _} =λ_→always-false 
  

以下是您如何使用它：

  test：Bool 
 test = f （1∷2∷3∷[]）1 2 4  -  false 
  

---

作为最后的评论：当你没有任何关于你正在应用的参数的信息时，这些函数并不是很有用。例如，如果您在未知长度的列表上使用 f ，那么您甚至不能将谓词应用于数。在这种情况下谓词是 Bool 并且不能应用于任何东西的情况下，该列表很可能是空的。

From what I know about dependent types, I think that it should possible, but I've never seen an example of this before in a dependently typed language, so I'm not exactly sure where to start.

What I want is a function of the form:

f : [Int] -> (Int -> Bool)
f : [Int] -> (Int -> Int -> Bool)
f : [Int] -> (Int -> Int -> Int -> Bool)

etc...

This function takes a list of n Ints, and returns a predicate function of arity n that takes Ints as an argument. Is this sort of thing possible in a dependently typed language? How would something like this be implemented?

解决方案

When creating functions of varying arity, you generally need a function from values to types. In this case, we need a function from List ℕ (or simply ℕ - the length of the list) to Set:

Predicate : ℕ → Set
Predicate zero    = Bool
Predicate (suc n) = ℕ → Predicate n

This allows us to create different type for each number:

Predicate 0 = Bool
Predicate 1 = ℕ → Bool
Predicate 2 = ℕ → ℕ → Bool
-- and so on

---

Now, how do we use Predicate to express the type of f? Since we are in dependently typed language, we can freely use value-level functions in types. So length seems to be a natural fit:

f : (l : List ℕ) → Predicate (length l)

Now, you didn't specify any particular f, but for the sake of the example, I'm going to implement one. Let's say that we want to check if all the numbers at corresponding positions (i.e. 1st argument to the function with 1st element of the list and so on) are equal.

I picked a rather simple function, so the implementation will be quite straightforward. But note that these kinds of functions use various tricks not unlike those used for implementing variadic functions with type classes (in Haskell).

When given an empty list, we'll simply return true:

f []       = true

For the nonempty list case, we create a function taking one argument named n and then compare it to the head of the list (m). If those numbers are not equal, we'll shortcut the rest of f and return a function that ignores all other numbers and simply returns false; if those numbers are equal, we'll simply continue with the rest of the list:

f (m ∷ ms) = λ n → case m ≟ n of λ
  { (yes _) → f ms
  ; (no  _) → always-false
  }

And the helper function always-false:

always-false : ∀ {n} → Predicate n
always-false {zero}  = false
always-false {suc _} = λ _ → always-false

And here's how you'd use it:

test : Bool
test = f (1 ∷ 2 ∷ 3 ∷ []) 1 2 4  -- false

---

As a final remark: those functions are not very useful when you do not have any information about the argument you are applying it to. For example, if you use f on a list of unknown length (that was given as an argument to another function), you can't even apply the "predicate" to a number. It's quite possible that the list is empty in which case the predicate is Bool and cannot be applied to anything.

这篇关于你可以创建函数来以依赖类型语言返回一个依赖项的函数吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！