with-pattern 结果不可见

Question

我正在尝试查看如何分支到 "safely-typed" 代码。例如，下面的意思是仅在安全路径上调用 tail - 即如果输入列表不为空。当然，有一个简单的方法，就是对列表进行模式匹配，但这个想法是协调函数 (null) 的结果及其在右侧的使用：

data Void : Set where

data _==_ {A : Set} (x : A) : A -> Set where
  refl : x == x

data Bool : Set where
  True : Bool
  False : Bool

data List (A : Set) : Set where
  nil  : List A
  _::_ : A -> List A -> List A

null : forall {A} -> List A -> Bool
null nil         = True
null (x :: xs)   = False

non-null : forall {A} -> List A -> Set
non-null nil = Void
non-null (x :: xs) = (x :: xs) == (x :: xs)

tail : forall {A} -> (xs : List A) -> {p : non-null xs} -> List A
tail (_ :: xs) = xs
tail nil      {p = ()}

prove-non-null : forall {A} -> (xs : List A) -> (null xs == False) -> non-null xs
prove-non-null nil         ()
prove-non-null (x :: xs)   refl = refl

compileme : forall {A} -> List A -> List A
compileme xs with null xs
...             | True    = xs
...             | False   = tail xs {prove-non-null xs refl}

在最后一行，agda 抱怨说 refl 不能被证明是 null xs == False 类型。为什么看不到with子句刚刚见证了null xs是False？

正确的做法是什么？如何从一个看似不依赖的"extract"依赖结果，像Bool类型不依赖列表xs，但在上下文中却是？

Answer 1

这就是 inspect 成语。检查 the original thread and this Whosebug question. The current version of inspect in the standard library is from this thread (there are also some explanations).

如果删除_==_的定义，那么可以将compileme定义为

open import Relation.Binary.PropositionalEquality renaming (_≡_ to _==_)

...

compileme : forall {A} -> List A -> List A
compileme xs with null xs | inspect null xs
...             | True    | [ _ ] = xs
...             | False   | [ p ] = tail xs {prove-non-null xs p}

顺便说一句，(x :: xs) == (x :: xs) 是什么意思？只是

open import Data.Unit
...
non-null (x :: xs) = ⊤

顺便说一句，你可以定义类型安全 tail 就像我在 this 答案中定义类型安全 pred 一样。

with-pattern 结果不可见

with-pattern result not visible

agda