haskell – 可以创建以依赖类型语言返回依赖关系的功能的函数吗

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,不能应用于任何东西.