Idris 中有上限的计数器

Question

我正在阅读“使用 Idris 进行类型驱动开发”，所以我创建了一个相当人为的示例作为实验。这是一个在尝试减少零值时无法进行类型检查的计数器。

代码如下：

data Counter : Nat -> Type where
  Value : (n : Nat) -> Counter n

data CounterOp : Type -> (before : Nat) -> (after : Nat) -> Type where
     Incr     : CounterOp () value (S value)
     Decr     : CounterOp () (S value) value
     GetValue : CounterOp Nat value value

     Pure : ty -> CounterOp ty value value
     (>>=) : CounterOp a value1 value2 ->
             (a -> CounterOp b value2 value3) ->
             CounterOp b value1 value3

runCounterOp : (val : Counter inValue) ->
           CounterOp ty inValue outValue ->
           (ty, Counter outValue)
runCounterOp (Value value) Incr = ((), Value (S value))
runCounterOp (Value (S value)) Decr = ((), Value value)
runCounterOp (Value value) GetValue = (value, Value value)
runCounterOp value (Pure x) = (x, value)
runCounterOp value (x >>= f) =
  let (x', value') = runCounterOp value x in
  runCounterOp value' (f x')

所以不可能 运行运行CounterOp (Value 0) Decr.

现在我想改变它，让它在超过 10 时无法进行类型检查（所以 运行运行CounterOp (Value 10) Incr 是不可能的）但我不知道如何。据我所知，我应该以某种方式使用 LTE，但不明白如何使用。

有什么想法吗？

Answer 1

您可以为 Fin 10 更改 Nat 或向 Incr 添加一个参数（显式或自动解析），其中包含初始值低于 10 的证明：Incr : {auto prf : LT value 10} -> CounterOp () value (S value).

Idris 中有上限的计数器

Counter with upper limit in Idris

idris