带表达式非求值

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)

那个洞的类型是 maybe (λ _ → ⊤) ⊥ (head l) 但由于 with 表达式，我希望类型是 ⊤。我希望这是因为我在 head l 上停了下来，在那种情况下 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

我找到的一个解决方案是使用 inspect 习惯用法。显然，agda 中的抽象不会传播平等。 inspect 惯用法使相等性显而易见。

data Uncons (A : Set) : Set where
  Nil : Uncons A
  Cons : A -> CoList A -> Uncons A

uncons : ∀ {A} -> CoList A -> Uncons A
uncons l with head l | inspect head l
uncons l | nothing   | _ = Nil
uncons l | just x    | [ p ] = Cons x (tail l (subst (maybe (λ _ -> ⊤) ⊥) (sym p) tt))

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

Answer 2

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

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

至于 'more than one constructor' 的余归类型编码，我知道有两种（密切相关的）方法：

相互inductive/coinductive类型：

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′

显式取 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′

带表达式非求值

With expression non evaluation

agda

dependent-type