从我所了解的依赖类型,我认为它应该是可能的,但我从来没有看到一个这样的例子在一个依赖类型的语言,所以我不知道从哪里开始.
我想要的是一种形式的功能：
f : [Int] -> (Int -> Bool) f : [Int] -> (Int -> Int -> Bool) f : [Int] -> (Int -> Int -> Int -> Bool)
等等…
该函数使用n Ints列表,并返回以Ints为参数的arity n的谓词函数.这种类型的语言是否可能成为可能？如何实现这样的事情？
当创建变化的功能时,通常需要一个从值到类型的函数.在这种情况下,我们需要一个列表ℕ的函数(或简单的ℕ – 列表的长度)设置：
Predicate : ℕ → Set Predicate zero = Bool Predicate (suc n) = ℕ → Predicate n
这允许我们为每个数字创建不同的类型：
Predicate 0 = Bool Predicate 1 = ℕ → Bool Predicate 2 = ℕ → ℕ → Bool -- and so on
现在,我们如何使用谓词来表达f的类型？由于我们是依赖类型的语言,我们可以在类型中自由使用价值层次的功能.所以长度似乎是一种自然的契合：
f : (l : List ℕ) → Predicate (length l)
现在,你没有指定任何特定的f,但为了这个例子,我要实现一个.假设我们想检查相应位置的所有数字(即列表的第一个元素的函数的第一个参数等等)是否相等.
我选择了一个相当简单的功能,所以实现将非常简单.但是请注意,这些函数使用与使用类型类(在Haskell中)实现可变函数的各种不同的技巧.
当给出一个空列表时,我们将返回true：
f [] = true
对于非空列表的情况,我们创建一个函数,使用一个名为n的参数,然后将其与列表(m)的头进行比较.如果这些数字不相等,我们将快速删除f的其余部分,并返回一个忽略所有其他数字的函数,并返回false;如果这些数字相等,我们将继续列出其余的数据：
f (m ∷ ms) = λ n → case m ≟ n of λ
{ (yes _) → f ms
; (no _) → always-false
}
而助手函数always-false：
always-false : ∀ {n} → Predicate n
always-false {zero} = false
always-false {suc _} = λ _ → always-false
以下是您如何使用它：
test : Bool test = f (1 ∷ 2 ∷ 3 ∷ []) 1 2 4 -- false
作为最后的评论：当您没有任何有关您正在应用的参数的信息时,这些功能不是非常有用.例如,如果在未知长度的列表中使用f(作为另一个函数的参数给出),则甚至不能将“谓词”应用于数字.很可能列表是空的,在这种情况下,谓词是Bool,不能应用于任何东西.
