Idris依赖类型的限制

Question

我一直在写Haskell一段时间,但想尝试使用Idris语言进行一些实验,并依赖打字.我玩了一下,并阅读了基本的文档,但是我想表达某种功能,并且不知道如何/是否可能.

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

first:一个函数,它接受两个自然数,但只检查第一个是否小于另一个.所以f : Nat -> Nat -> whatevernat1小于nat2.这个想法是,如果一个像f 5 10它一样的调用,但如果我调用它就像f 10 5它将无法键入检查.

第二个:一个函数,它接受一个字符串和一个字符串列表,只有当第一个字符串在字符串列表中时才进行类型检查.

在伊德里斯这样的功能是否可行？如果是这样,你会如何实现一个简单的例子？谢谢!

编辑:

在多个用户的帮助下,编写了以下解决方案功能:

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

我并不特别喜欢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)

可以安全地Fin从Nat较大的数字中定义数字的减法.我们还可以表达结果不会比输入更大的事实.

(-) : (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我在该类型中使用的是减去自然数.它截断为零的事实不需要麻烦我们,因为它的类型-确保它永远不会发生.(此功能可以Prelude在名称下找到minus.)

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

这里要学到的教训就是这个.首先,在我们的数据中构建一些正确性属性导致渐近的减速.我们可以放弃对返回值做出承诺并回到无类型版本,但实际上给类型检查器提供了更多信息,这使我们能够在没有做出牺牲的情况下获得我们的目标.