haskell - Idris 中依赖类型的限制

Question

我编写 Haskell 一段时间了，但想尝试使用 Idris 语言和依赖类型进行一些实验。我玩了一下，并阅读了基本文档，但是我想表达某种风格的功能，并且不知道如何/是否可能。

以下是我想知道是否可以表达的几个例子:

first:一个函数，它接受两个自然数，但仅类型检查第一个是否小于另一个。所以f : Nat -> Nat ->whatever 其中 nat1 小于 nat2。这个想法是，如果像 f 5 10 这样调用它就可以工作，但如果我像 f 10 5 那样调用它，它将无法进行类型检查。

第二个:一个函数，它接受一个字符串和一个字符串列表，仅检查第一个字符串是否在字符串列表中。

Idris 中可以实现这样的功能吗？如果是这样，您将如何实现上述简单示例之一？谢谢!

编辑:

在几位用户的帮助下，编写了以下解决方案函数:

module Main

import Data.So

f : (n : Nat) -> (m : Nat) -> {auto isLT : So (n < m)} -> Int
f _ _ = 50

g : (x : String) -> (xs : List String) -> {auto inIt : So (elem x xs)} -> Int
g x xs = 52

main : IO ()
main = putStrLn $ show $ g "hai" ["test", "yo", "ban", "hai", "dog"]

这些当前解决方案不适用于大型案例。例如，如果您运行 f 的数字超过几千，则需要很长时间(不是字面上的意思)。我认为这是因为类型检查目前是基于搜索的。一位用户评论说，可以通过自己编写证明来为 auto 提供提示。假设这就是所需要的，如何为这些简单情况中的任何一个编写这样的证明？

Answer 1

I'm not especially fond of So ，或者实际上是在程序中存在可避免的证明项。将您的期望融入数据本身的结构中会更令人满意。我将写下“小于 n 的自然数”的类型。

data Fin : Nat -> Set where
  FZ : Fin (S n)
  FS : Fin n -> Fin (S n)

Fin 是一种类似数字的数据类型 - 将 FS (FS FZ) 的形状与自然数 S (S Z) 的形状进行比较code> - 但有一些额外的类型级结构。为什么叫Fin？ Fin n 类型恰好有 n 个唯一成员；因此，Fin 是有限集家族。

我的意思是:Fin确实是一种数字。

natToFin : (n : Nat) -> Fin (S n)
natToFin Z = FZ
natToFin (S k) = FS (natToFin k)

finToNat : Fin n -> Nat
finToNat FZ = Z
finToNat (FS i) = S (finToNat i)

重点是:Fin n 值必须小于其 n。

two : Fin 3
two = FS (FS FZ)
two' : Fin 4
two' = FS (FS FZ)
badTwo : Fin 2
badTwo = FS (FS FZ)  -- Type mismatch between Fin (S n) (Type of FZ) and Fin 0 (Expected type)

当我们这样做时，没有任何数字小于零。也就是说，基数为0的集合Fin Z是一个空集。

Uninhabited (Fin Z) where
  uninhabited FZ impossible
  uninhabited (FS _) impossible

如果你有一个小于n的数字，那么它肯定小于S n。因此，我们有一种方法可以放松 Fin 的上限:

weaken : Fin n -> Fin (S n)
weaken FZ = FZ
weaken (FS x) = FS (weaken x)

我们还可以采用另一种方式，使用类型检查器自动查找给定 Fin 上可能的最紧边界。

strengthen : (i : Fin n) -> Fin (S (finToNat i))
strengthen FZ = FZ
strengthen (FS x) = FS (strengthen x)

可以安全地定义从较大的 Nat 数字中减去 Fin 数字。我们还可以表达这样一个事实:结果不会比输入大。

(-) : (n : Nat) -> Fin (S n) -> Fin (S n)
n - FZ = natToFin n
(S n) - (FS m) = weaken (n - m)

<小时/>

这一切都有效，但有一个问题:weaken 的工作原理是在 O(n) 时间内重建其参数，并且我们将其应用于 - 的每次递归调用>，产生 O(n^2) 减法算法。多么尴尬! weaken 只是真正帮助类型检查，但它对代码的渐近时间复杂度有巨大的影响。我们可以在不削弱递归调用结果的情况下逃脱吗？

好吧，我们必须调用 weaken 因为每次遇到 S 时，结果和界限之间的差异就会增大。我们可以通过轻轻地向下拉类型以满足它来缩小差距，而不是强行将值拉到正确的类型。

(-) : (n : Nat) -> (i : Fin (S n)) -> Fin (S (n `sub` finToNat i))
n - FZ = natToFin n
(S n) - (FS i) = n - i

这种类型的灵感来自于我们成功地通过strengthen收紧了Fin的束缚。 - 结果的界限完全符合其需要的严格程度。

我在类型中使用的

sub是自然数的减法。它在零处截断的事实不必困扰我们，因为 - 的类型确保它永远不会真正发生。 (此函数可以在 Prelude 中的 minus 名称下找到。)

sub : Nat -> Nat -> Nat
sub n Z = n
sub Z m = Z
sub (S n) (S m) = sub n m

这里要吸取的教训是这样的。起初，在我们的数据中构建一些正确性属性会导致渐近减速。我们本可以放弃对返回值做出 promise 并返回到无类型版本，但事实上giving the type checker more information让我们能够在不做出牺牲的情况下到达目的地。