Idris 中依赖类型的限制
Limits of dependent typing in Idris
我写 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 提供 提示 。假设这是所需要的，那么如何为这些简单的情况编写这样的证明呢？
，或者实际上在程序中有可避免的证明项 运行。将您的期望编织到数据本身的结构中会更令人满意。我要写下 "natural numbers smaller than 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
这种类型的灵感来自于我们成功地用 strengthen 收紧了 Fin 的约束。 - 结果的界限完全符合需要。
sub，我在type里面用的，就是自然数的减法。它在零处截断的事实不必困扰我们，因为 - 的类型确保它永远不会真正发生。 （这个函数可以在minus名字下的Prelude中找到。）
sub : Nat -> Nat -> Nat
sub n Z = n
sub Z m = Z
sub (S n) (S m) = sub n m
这里要吸取的教训是这样的。起初，在我们的数据中构建一些正确性属性会导致渐近减速。我们本可以放弃对 return 值做出承诺并返回到无类型版本，但实际上 giving the type checker more information 允许我们在不做出牺牲的情况下到达我们要去的地方。
So 是一个非常通用的东西，它允许您 "lift" 类型级别的任何布尔条件。不过，这种普遍性是有代价的，即这样的证明（至少以我的经验）更难构建且计算成本更高。
相反，通常最好为自己创建一个专门的证明类型，它允许您仅表达某种类型的条件，但以更简单的方式产生更清晰、更易于构造的证明。 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 的证明（请注意，它仅适用于 Nat，因为它依赖于该类型的内部结构）。 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 for all rights.
LTESucc : LTE left right -> LTE (S left) (S right)表示一个蕴涵：如果left小于等于right则S left小于等于S right.
这是Curry-Howard同构的全貌。
我写 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 提供 提示 。假设这是所需要的，那么如何为这些简单的情况编写这样的证明呢？
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
这种类型的灵感来自于我们成功地用 strengthen 收紧了 Fin 的约束。 - 结果的界限完全符合需要。
sub，我在type里面用的，就是自然数的减法。它在零处截断的事实不必困扰我们，因为 - 的类型确保它永远不会真正发生。 （这个函数可以在minus名字下的Prelude中找到。）
sub : Nat -> Nat -> Nat
sub n Z = n
sub Z m = Z
sub (S n) (S m) = sub n m
这里要吸取的教训是这样的。起初，在我们的数据中构建一些正确性属性会导致渐近减速。我们本可以放弃对 return 值做出承诺并返回到无类型版本，但实际上 giving the type checker more information 允许我们在不做出牺牲的情况下到达我们要去的地方。
So 是一个非常通用的东西，它允许您 "lift" 类型级别的任何布尔条件。不过，这种普遍性是有代价的，即这样的证明（至少以我的经验）更难构建且计算成本更高。
相反，通常最好为自己创建一个专门的证明类型，它允许您仅表达某种类型的条件，但以更简单的方式产生更清晰、更易于构造的证明。 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 的证明（请注意，它仅适用于 Nat，因为它依赖于该类型的内部结构）。 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 for all rights.
LTESucc : LTE left right -> LTE (S left) (S right)表示一个蕴涵：如果left小于等于right则S left小于等于S right.
这是Curry-Howard同构的全貌。