Agda 中的 coinductive data type

by

从字符串说起

Agda 的内置字符串类型（ Agda.Builtin.String）是作为 postulate 定义的：

module Agda.Builtin.String

postulate String : Set
{-# BUILTIN STRING String #-}


postulate primStringToList   : String → List Char
postulate primStringFromList : List Char → String
postulate primStringAppend   : String → String → String
postulate primStringEquality : String → String → Bool
postulate primShowString     : String → String


type String = List Char


String 的话，又需要用 primStringToList 转来转去，十分 键山雏 麻烦。

postulate IO : Set → Set
{-# BUILTIN IO IO #-}

postulate putStrLn : Costring → IO Unit
{-# COMPILE GHC putStrLn = putStrLn #-}


import IO.Primitive as Prim

infixl 1 _>>=_ _>>_

data IO {a} (A : Set a) : Set (suc a) where
lift   : (m : Prim.IO A) → IO A
return : (x : A) → IO A
_>>=_  : {B : Set a} (m : ∞ (IO B)) (f : (x : B) → ∞ (IO A)) → IO A
_>>_   : {B : Set a} (m₁ : ∞ (IO B)) (m₂ : ∞ (IO A)) → IO A

{-# NON_TERMINATING #-}

putStrLn∞ : Costring → IO ⊤
putStrLn∞ s =
♯ lift (Prim.putStrLn s) >>
♯ return _

putStrLn : String → IO ⊤
putStrLn s = putStrLn∞ (toCostring s)


无穷的数据类型

data Colist a = a :> Colist a


cozipWith :: (a -> b -> c) -> Colist a -> Colist b -> Colist c
cozipWith f (a :> as) (b :> bs)  = f a b :> cozipWith f as bs

cohead :: Colist a -> a
cohead (x :> _) = x

cotail :: Colist a -> Colist a
cotail (_ :> xs) = xs


-- n 的无限序列
repeat :: a -> Colist a
repeat n = n :> repeat n

-- 斐波那契数列的无限序列
fib :: Integral n => Colist n
fib = 0 :> 1 :> cozipWith (+) fib (cotail fib)


-- 取列表的最后一项
last :: List a -> a
last [] = error "empty list"
last [a] = a
last (_ : as) = last as


Agda 中的表示

infixr 5 _∷_

data Colist {a} (A : Set a) : Set a where
[]  : Colist A
_∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A

{-# FOREIGN GHC type AgdaColist a b = [b] #-}
{-# COMPILE GHC Colist = data MAlonzo.Code.Data.Colist.AgdaColist ([] | (:)) #-}


emmmm… 居然提供了 [] 这个构造器。。。

∞ 是什么鬼，∞ (Colist A)Colist A 有什么区别，怎么构造一个 ∞ (Colist A) 呢？

真相

postulate
-- 标记
∞  : ∀ {a} (A : Set a) → Set a
-- 互相转换的运算符
♯_ : ∀ {a} {A : Set a} → A → ∞ A
♭  : ∀ {a} {A : Set a} → ∞ A → A
{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}


repeat : ∀ {a} {A : Set a} → A → Colist A
repeat a = a ∷ repeat a


[_] : ∀ {a} {A : Set a} → A → Colist A
[ x ] = x ∷ ♯ []


map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Colist A → Colist B
map f []       = []
map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)


拓展阅读

Tweet this
Top

Create an issue to apply for commentary