使用证明对象定义列表的头部

Question

我想为列表定义一个 head 函数。为了避免尝试计算空列表的头部可以使用长度大于 1 的向量（即 Vec (suc n)）或使用 Lists，但将列表非空的证明传递给 head。（这就是“工作中的依赖类型”所说的 internal vs external 编程逻辑，我相信。）我对后一种方法感兴趣。请注意，有一个可以解决这个问题，但我想要一个最小的方法。（例如，我宁愿不使用 Instance Arguments 除非他们被要求。）下面是我的尝试，但我不完全明白发生了什么。例如：

不清楚为什么我能够跳过 head [] 案例。显然它与我传递的“证明”有关，但我本以为我需要某种带有 () 的案例。
当我输入 check (C-c C-l) 时，我似乎得到了两个目标作为输出。
我希望看到 tmp2 类型检查失败。

非常欢迎任何见解。特别是，做我想做的事情的“正确”方法是什么？

data List (A : Set) : Set where
    [] : List A
    _::_ : A → List A → List A

{-
head1 : {A : Set} → (as : List A) → A
-- As expected, complains about missing case `head1 []`.
head1 (a :: aa) = a
-}

data ⊤ : Set where
    tt : ⊤

data ⊥ : Set where

isNonEmpty : {A : Set} → List A → Set
isNonEmpty [] = ⊥
isNonEmpty (_ :: _) = ⊤

head : {A : Set} → (as : List A) → {isNonEmpty as} → A
head (a :: _) = a

-- Define just enough to do some examples

data Nat : Set where
    zero : Nat
    suc : Nat → Nat

{-# BUILTIN NATURAL Nat #-}

len1 : List Nat
len1 = 17 :: []

tmp : Nat
tmp = head len1

tmp1 : Nat
tmp1 = head len1 { tt }

len0 : List Nat
len0 = []

tmp2 : Nat
tmp2 = head len0

Answer 1

coverage checking in Agda 上的用户手册解释说，在某些情况下，荒谬的条款可以完全省略：

In many common cases, absurd clauses may be omitted as long as the remaining clauses reveal sufficient information to indicate what arguments to case split on. [...] Absurd clauses may be omitted if removing the corresponding internal nodes from the case tree does not result in other internal nodes becoming childless.

请注意，如果您愿意，您仍然可以手动编写荒谬的子句，Agda 会接受它。

你得到的不是两个未解决的漏洞，而是两个未解决的元变量。这些元变量是由 Agda 创建的，用于分别在 tmp 和 tmp2 的定义中填充 head 的隐式参数，而 Agda 的约束求解器无法求解它们。对于 tmp 中的元变量，这是因为你将 ⊤ 定义为数据类型而不是记录类型，而 Agda 只对记录类型应用 eta-equality。对于tmp2中的元变量，类型是⊥所以Agda没希望在这里找到解决方案。
使用 Agda 时，您应该将未解决的元变量视为“类型检查失败”的特定情况。它们不是 hard 类型错误，因为那会阻止您继续使用 Agda 的交互式编辑，并且在许多情况下进一步填补漏洞实际上会解决元变量。但是，它们表示“此程序未完成”，就像实际类型错误一样。

使用证明对象定义列表的头部

Defining the head of a list with a proof object

agda