Idris 中依赖类型的限制

Question

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

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

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

second：一个函数，它接受一个字符串和一个字符串列表，它只检查第一个字符串是否在字符串列表中。

在 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 的数字超过几千，则需要永远（不是字面意思）。我认为这是因为类型检查当前是基于搜索的。一位用户评论说，可以通过自己编写证明来为自动提供提示。假设这是所需要的，如何为这些简单案例中的任何一个编写这样的证明？

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) 的形状进行比较 - 但有一些额外的类型级结构。为什么叫Fin？恰好有n 类型为Fin 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)

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

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

这种类型的灵感来自于我们成功收紧了Fin 与strengthen 的绑定。 - 的结果的界限与它需要的一样紧。

sub，我在类型中使用的，是自然数的减法。它在零处截断的事实不必给我们带来麻烦，因为- 的类型确保它永远不会真正发生。 （这个功能可以在minus名称下的Prelude中找到。）

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

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

Answer 2

So 是一个非常通用的东西，它允许您将任何布尔条件“提升”到类型级别。不过，这种普遍性是有代价的，即此类证明（至少在我的经验中）更难构建且计算成本更高。

相反，通常最好为自己创建一个专门的证明类型，它只允许您表达某种类型的条件，但以一种更简单的方式，产生更清晰、更容易构建的证明。 Idris 标准库充满了这种专门的证明类型（或者更确切地说是类型族）。果然，这里已经包含了你关心的那些。

||| Proofs that `n` is less than or equal to `m`
||| @ n the smaller number
||| @ m the larger number
data LTE  : (n, m : Nat) -> Type where
  ||| Zero is the smallest Nat
  LTEZero : LTE Z    right
  ||| If n <= m, then n + 1 <= m + 1
  LTESucc : LTE left right -> LTE (S left) (S right)

（来自Prelude.Nat）

LTE x y 类型的术语表示x 不大于y 的证明（请注意，它仅适用于Nats，因为它依赖于该类型的内部结构）。 LTEZero 不需要任何参数，因为Z 永远不会大于任何Nat（包括Z 本身）。你可以随意构建这样的证明。对于其他数字，您可以通过归纳证明LTE 关系（假设LTE x y 暗示LTE (S x) (S y) 的规则）。通过解构你的论点，你最终会到达其中一个是Z 的时刻。如果它是左边的，那么你通过声明Z 小于或等于任何东西来完成，如果它是正确的，对不起，你的假设是错误的，因此你将无法构建你的证明。

maybeLTE : (n, m : Nat) -> Maybe (LTE n m)
maybeLTE Z _ = Just LTEZero
maybeLTE _ Z = Nothing
maybeLTE (S n) (S m) = map LTESucc $ maybeLTE n m

请注意，此构造如何不依赖任何外部排序概念。相反，这种类型定义Nat 小于或等于另一个Nat 意味着什么。这两个构造函数（连同类型 Nat 本身）可以被认为是一个理论的公理，您可以从中得出您的证明。我们再来看看这些构造函数的类型：

LTEZero : LTE Z right 声明 Z 小于或等于 right 对于所有 rights。

LTESucc : LTE left right -> LTE (S left) (S right) 表示暗示：如果left 小于或等于right，则S left 小于或等于S right。

这是完全荣耀的库里-霍华德同构。