日々の流転

λ. ストリームの表現

ストリームの直観的な表現はsigを使った次のような表現だが、この定義はtermination checkerに怒られる。

Stream :: Set -> Set
Stream A = sig
             head :: A
             tail :: Stream A

別の定義として以下のようなものが考えられるが、今度はストリームを生成する関数がtermination checkerに怒られることになる。

data Stream (X::Set) = SCons (x::X) (xs::Stream X)

from :: Nat -> Stream Nat
from n = SCons n (from (succ n))

実のところ、agdaにはcodataを扱う機能がないので、ストリームのようなcodataを直接扱うことは出来ない。そこでストリームと同型でかつagdaで表現可能なデータ型を考える。ストリームの直観的な意味は無限個の直積 A^ω なので Nat -> A という関数型として表現することが考えられる。基本的な演算も同時に定義すると以下のようになる。

Stream :: Set -> Set
Stream A = Nat -> A

head (|A::Set) :: Stream A -> A
head s = s zero

tail (|A::Set) :: Stream A -> Stream A
tail s = \n -> s (succ n)

unfold (|A,|X::Set) :: (X -> A × X) -> (X -> Stream A)
unfold phi x n =
    case phi x of
    (a,x)->
        case n of
        (zer  )-> a
        (suc m)-> unfold phi x m

この表現で一つ嫌な点は外延性が成り立たない点。つまり Ext = (A::Set) -> (s1,s2::Stream A) -> ((n::Nat) -> Id (s1 n) (s2 n)) -> Id s1 s2 は要素を持たないし、双模倣(bisimulation)の関係にあるストリームが等しいことも一般には証明できない。内包的(intentional)な型理論の世界で作業している以上仕方がないところではあるが、これはやっぱし嫌な感じだし、ある程度の外延性を持った型理論がいいなぁ……

ところで、このストリームの表現は Representations of First order function types as terminal coalgebras. の対応を逆に使ったものなので、他のcodataにも同様の方法で表現できるものがある。しかし、νX. 1+A×X のように直和が入ってくるとこの方法では表現できないと思うし、やはり組み込みのcodata対応は欲しいところか。OTT(Observational Type Theory) と Observational Epigram (Codata参照) に期待。それから、IsabelleやCoqではcodataの扱いはどうなってるんだろう。Coqはcodataをサポートしているらしいが…

【2007-09-11追記】 直和が入ってくるような場合でも、20070905#p01のようにすれば表現可能。