#idris
#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 (значение 0) Decr.
Теперь я хочу изменить его, чтобы он не выполнял проверку типа, когда он превышает 10 (поэтому запустить runCounterOp (значение 10) Incr невозможно), но я не знаю как. Насколько я понимаю, я должен как-то использовать LTE, но не понимаю, как.
Есть идеи?
Комментарии:
1. Может
Fin
быть, было бы полезно
Ответ №1:
Вы можете либо изменить Nat
Fin 10
, либо добавить к Incr
параметру (явному или автоматически разрешаемому), который содержит доказательство того, что начальное значение меньше 10: Incr : {auto prf : LT value 10} -> CounterOp () value (S value)
.