以下是我想知道的是否可以表达的几个例子：
first：一个函数,它接受两个自然数,但只检查第一个是否小于另一个.所以f：Nat – > Nat – >无论nat1小于nat2.这个想法是,如果像f 5 10那样调用它会起作用,但是如果我像f 10那样调用它,它将无法进行类型检查.
第二个：一个函数,它接受一个字符串和一个字符串列表,只有当第一个字符串在字符串列表中时才进行类型检查.
在伊德里斯这样的功能是否可行？如果是这样,你会如何实现一个简单的例子？谢谢！
编辑：
在多个用户的帮助下,编写了以下解决方案功能：
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,它需要永远(不是字面意思).我认为这是因为类型检查目前是基于搜索的.一位用户评论说,可以通过自己编写证明来提供自动提示.假设这是需要的,那么如何为这些简单案例中的任何一个编写这样的证明？
I’m not especially fond ofSo,或者确实有可避免的证明条款在程序中运行.将您的期望编织到数据本身的结构中会更令人满意.我要写下一个“小于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)
这一切都有效,但是有一个问题：通过在O(n)时间内重建其参数来减弱工作,并且我们在每次递归调用时应用它,产生用于减法的O(n ^ 2)算法.多么尴尬！弱化只是帮助进行类型检查,但它对代码的渐近时间复杂度产生了极大的影响.我们可以逃脱而不会削弱递归调用的结果吗？
好吧,我们不得不打电话削弱因为每当我们遇到一个S时,结果和界限之间的差异就会增大.我们可以通过轻轻拉下类型来满足它,而不是强行将值推到正确的类型.
(-) : (n : Nat) -> (i : Fin (S n)) -> Fin (S (n `sub` finToNat i)) n - FZ = natToFin n (S n) - (FS i) = n - i
这种类型的灵感来自于我们在加强Fin的束缚方面取得的成功. – 结果的界限完全和它需要的一样紧.
我在该类型中使用的sub是减去自然数.它截断为零的事实不需要麻烦我们,因为它的类型 – 确保它永远不会真正发生. (此功能可在减号名称的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让我们可以在没有牺牲的情况下到达我们的目的地.