haskell – 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"]

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)

这一切都有效,但是有一个问题：通过在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让我们可以在没有牺牲的情况下到达我们的目的地.