模式結果不可見

Question

我想看看如何分支到「安全類型」的代碼。例如，以下意味着僅在安全路徑上調用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-clause剛剛目睹null xs是False？

關於它的正確方法是什麼？如何從一個看起來不依賴的結果中「提取」依賴項，如Bool類型不依賴於列表xs，但在上下文中它是？

Answer 1

這就是關於inspect成語。檢查the original thread和this stackoverflow question。 The current version的inspect在標準庫中是從this線程（也有一些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) = ⊤ 

BTW2，你可以定義爲我this答案定義的類型安全pred類型安全tail。