agda - 带表达式非求值

Question

我正在尝试定义一个没有延迟构造函数的 CoList。我遇到了一个问题，我使用了 with 表达式，但 agda 没有细化子案例的类型。

module Failing where

open import Data.Unit
open import Data.Empty
open import Data.Maybe
open import Data.Nat
open import Data.Vec hiding (head ; tail ; map ; take)

record CoList (A : Set) : Set where
  coinductive
  field
    head : Maybe A
    tail : maybe (λ _ → ⊤) ⊥ head -> CoList A
open CoList

nil : ∀ {A} -> CoList A
head nil = nothing
tail nil ()

cons : ∀ {A} -> A -> CoList A -> CoList A
head (cons x xs) = just x
tail (cons x xs) tt = xs

take : ∀ {A} -> CoList A -> (n : ℕ) -> Maybe (Vec A n)
take l zero = just []
take l (suc n) with head l
...                 | nothing = nothing
...                 | just x = map (λ xs → x ∷ xs) (take (tail l {!!}) n)

那个洞的类型可能是 (λ _ → ⊤) ⊥ (head l) 但由于 with 表达式，我希望类型是 ⊤。我期望这是因为我在 head l 上使用了 withed，在那种情况下 head l = just x。如果我尝试用 tt 填充整个 agda 模式会给我以下错误:

⊤ !=< (maybe (λ _ → ⊤) ⊥ (head l)) of type Set
when checking that the expression tt has type
(maybe (λ _ → ⊤) ⊥ (head l))

我回答了下面的问题，所以现在我很好奇是否有更好的方法在没有延迟构造函数的情况下对这个列表进行编码？

Answer 1

您可以将 with t 视为在函数参数和目标的类型中用您匹配的任何内容替换 t。但是，当您执行 with 时，head l 不会出现在您的目标类型中 — 类型涉及 head l 的目标只会在稍后出现，一次您已经部分构建了解决方案。这就是您最初的尝试不起作用的原因。

如您的回答所示，inspect 习惯用法确实是此类问题的常用解决方案。

对于具有“多个构造函数”的余归类型的编码，我知道有两种(密切相关的)方法:

1. 互感/互感类型:

   data   CoList′ (A : Set) : Set
   record CoList  (A : Set) : Set
   
   data CoList′ A where
     [] : CoList′ A
     _∷_ : A → CoList A → CoList′ A
   
   record CoList A where
     coinductive
     field
       unfold : CoList′ A
   
   open CoList
   
   repeat : ∀ {A} → A → CoList A
   repeat x .unfold = x ∷ repeat x
   
   take : ∀ {A} → ℕ → CoList A → List A
   take zero    _ = []
   take (suc n) xs with unfold xs
   ... | [] = []
   ... | x ∷ xs′ = x ∷ take n xs′
   

2. 显式地取 cofixpoint:

   data CoList′ (A : Set) (CoList : Set) : Set where
     [] : CoList′ A CoList
     _∷_ : A → CoList → CoList′ A CoList
   
   record CoList (A : Set) : Set where
     coinductive
     field
       unfold : CoList′ A (CoList A)
   
   open CoList
   
   repeat : ∀ {A} → A → CoList A
   repeat x .unfold = x ∷ repeat x
   
   take : ∀ {A} → ℕ → CoList A → List A
   take zero    _ = []
   take (suc n) xs with unfold xs
   ... | [] = []
   ... | x ∷ xs′ = x ∷ take n xs′