idris - 使用 Idris 实现 isLast

Question

查看来自 Idris 的类型驱动开发的练习 9.2:

data Last : List a -> a -> Type where
  LastOne : Last [value] value
  LastCons : (prf : Last xs value) -> Last (x :: xs) value

Uninhabited (Last [] value) where
  uninhabited LastOne impossible
  uninhabited (LastCons _) impossible

notLast : Not (x = value) -> Last [x] value -> Void
notLast prf LastOne      impossible
notLast prf (LastCons _) impossible

isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast []      value = No absurd
isLast (x::[]) value = case decEq x value of
                         Yes Refl  => Yes LastOne
                         No contra => No (notLast contra)
isLast (x::y::ys) value = ?rhs

我在 notLast prf LastOne 上遇到编译时错误案件:

*section1> :r
Type checking ./section1.idr
section1.idr:20:9:notLast prf LastOne is a valid case
Holes: Main.rhs, Main.notLast

为什么编译器认为它是一个有效的案例？

Answer 1

idris 不太能看出 Not (value = value)同构于 Void所以你需要通过解释问题是什么来帮助它:

notLast : Not (x = value) -> Last [x] value -> Void
notLast prf LastOne      = absurd (prf Refl)
notLast prf (LastCons _) impossible