式が評価されない

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

あなたが関数の引数と目標の両方のタイプで、照合どんなことでtを置き換えるようwith tと考えることができます。ただし、を実行するとhead lのゴールタイプには表示されません。head lを含むタイプのゴールは、ソリューションを部分的に構成した後に表示されます。これがあなたの最初の試みがうまくいかない理由です。

あなたの答えに示されているように、inspectのイディオムは実際にこの種の問題の通常の解決策です。 「複数のコンストラクタ」とcoinductive種類のエンコーディングについては

、2は（密接に関連）があります私の知ることをアプローチ：

1. 相互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′ 
   

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

私が見つけた1つの解決策は、検査のイディオムを使用することです。明らかに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)