时间戳

首页 > 解决方案 > 伊德里斯中带上限的计数器

idris - 伊德里斯中带上限的计数器

问题描述

我现在正在阅读“使用 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')

所以不可能运行 runCounterOp (Value 0) Decr。

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

有任何想法吗？

标签： idris

解决方案

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

推荐阅读