表达非评价

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)但是由于带有表达式，我希望这个类型是⊤。我期待这一点，因为我在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

在函数参数和目标的类型中，您可以将with t视为替换任何匹配的t。但是，当您执行head l时，with不会出现在您的目标类型中 - 一旦您部分构建解决方案，其类型涉及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′

Answer 2

我找到的一个解决方案是使用检查习语。显然，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)