Agda2のcodata定義

Agda2では、dataで定義したデータ型は有限で、それを利用する再帰関数も停止性が証明できないといけないけれど、codataは、停止しない再帰関数を記述することができます。

定義は、ラベルがcodataである以外、dataと同じです。以下のStream Aは、List Aと同じ構造ですが、有限である必要がないので、nil相当のコンストラクタはcodataには不要です。むしろnil相当が存在しないことで、このcodataが必ず無限であることをあらわしています。

codata Stream (A : Set) : Set where
    stream : A -> Stream A -> Stream A
{- <=>
data List (A : Set) : Set where
    nil : List A
    cons : A -> List A -> List A
-}

data同様に、普通の関数の引数や戻り値として使えます。

top : {A : Set} -> Stream A -> A
top (stream h _) = h

next : {A : Set} -> Stream A -> Stream A
next (stream _ ts) = ts

無限のcodataを扱う無限の再帰関数を記述するときは、"="のかわりに"~"で右辺を定義します。

gen : {A : Set} -> A -> Stream A
gen a ~ stream a (gen a)

map : {A B : Set} -> (A -> B) -> Stream A -> Stream B
map f (stream h ts) ~ stream (f h) (map f ts)

• gen aは、無限にaが取り出せるStreamを作る関数
• map f s は、無限Streamのsの各要素にfをかけたStreamを作る関数

こういった関数の定義に"="を使うと、data同様停止性チェックが働き、停止しないよエラーがでます。genの定義の"~"を"="に変えると以下のエラーが出ました:

[CoData.gen] does NOT termination check

逆に言うと、"~"を使う定義は、無限のデータなので戻り値の型はcodataである必要があります。

data List (A : Set) : Set where
    [] : List A
    _::_ : A -> List A -> List A

mapl : {A B : Set} -> (A -> B) -> Stream A -> List B
mapl f (stream h ts) ~ (f h) :: (mapl f ts)

戻り値がdataだと、"~"であっても非停止エラーがでます:

[CoData.mapl] does NOT termination check

前回のNatやVecも加えて、いくつか基礎的な関数を作ることができるでしょう:

data Nat : Set where
    zero : Nat
    succ : Nat -> Nat

data Vec (A : Set) : Nat -> Set where
    nil : Vec A zero
    cons : {n : Nat} -> A -> Vec A n -> Vec A (succ n)

take : {A : Set} -> (n : Nat) -> Stream A -> Vec A n
take zero _ = nil
take (succ n) (stream h ts) = cons h (take n ts)

nats : Nat -> Stream Nat
nats n ~ stream n (nats (succ n))

• take n sは、sからn個のデータをVecにして取り出す関数
• nats nは、n,n+1,n+2,...というStreamを作る関数

codataもdata同様、コンストラクタの引数には、自身が引数になる関数を、使うことはできないようです:

codata Contra : Set where
    contra : (Contra -> Nat) -> Contra

このエラー

negatively in the constructor .CoData.contra of Contra

証明では以下のように使えます。

data eq {A : Set} (x : A) : A -> Set where
    refl : eq x x

gen_eq_next_gen : {A : Set}{a : A} -> eq (gen a) (next (gen a))
gen_eq_next_gen = refl

構造比較なので、gen aも next (gen a)も同型と判定され、チェックが通ります。
式の形はターミナルでチェックできます。

Main> gen zero
gen zero
Main> next (gen zero)
gen zero
Main>

put it together

CoData.agda

module CoData where

codata Stream (A : Set) : Set where
    stream : A -> Stream A -> Stream A

top : {A : Set} -> Stream A -> A
top (stream h _) = h

next : {A : Set} -> Stream A -> Stream A
next (stream _ ts) = ts

{- codata infinite recursive definition is "~", not "="
   (no termination check)
-}
gen : {A : Set} -> A -> Stream A
gen a ~ stream a (gen a)

map : {A B : Set} -> (A -> B) -> Stream A -> Stream B
map f (stream h ts) ~ stream (f h) (map f ts)

{-
data List (A : Set) : Set where
    [] : List A
    _::_ : A -> List A -> List A

mapl : {A B : Set} -> (A -> B) -> Stream A -> List B
mapl f (stream h ts) ~ (f h) :: (mapl f ts)
-}

{- stream with nat, vec -}
data Nat : Set where
    zero : Nat
    succ : Nat -> Nat

data Vec (A : Set) : Nat -> Set where
    nil : Vec A zero
    cons : {n : Nat} -> A -> Vec A n -> Vec A (succ n)

take : {A : Set} -> (n : Nat) -> Stream A -> Vec A n
take zero _ = nil
take (succ n) (stream h ts) = cons h (take n ts)

nats : Nat -> Stream Nat
nats n ~ stream n (nats (succ n))


{- cannot create contra-variant argument data
codata Contra : Set where
    contra : (Contra -> Nat) -> Contra
-}

{- proof -}
data eq {A : Set} (x : A) : A -> Set where
    refl : eq x x

gen_eq_next_gen : {A : Set}{a : A} -> eq (gen a) (next (gen a))
gen_eq_next_gen = refl