Блог

Сейчас я читаю «Разработку на основе типов с помощью 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, но не понимаю, как.

Есть идеи?

Вы можете либо изменить Nat Fin 10 , либо добавить к Incr параметру (явному или автоматически разрешаемому), который содержит доказательство того, что начальное значение меньше 10: Incr : {auto prf : LT value 10} -> CounterOp () value (S value) .