Agda 中的 coinductive data type

Agda 中的 coinductive data type

來自專欄千里冰封被吊打的日常14 人贊了文章

---

最近和 @16 聊了一些關於 Coq 的話題，16 給我講了很多 Coq 對 coinductive

數據類型的處理方式，讓我一臉懵逼。

由於 Agda 中（似乎？）沒有像 Coq 那樣區分 coinductive 和 inductive（而是作為幾個 postulate，下面會說），所以我從來還沒想過這些問題。

然後就研究了一下，感覺是之前不會的東西，就寫篇博客聊聊。

本文命名僅僅是比較正常，請 Haskell 程序員不要模仿。

名稱解釋

比較面向小學生的說法是，coinductive 就是在歸納的時候上升的，而 inductive 是在歸納的時候下降的。

比較面向工業界編程的說法是，coinductive 的數據類型是無窮的，inductive 是有窮的。

比如 java.util.Collection 就是 inductive 的， java.util.Iterable 就是 coinductive 的。

For experts

我知道 Agda 現在有 coinductive record + copattern 這種更推薦的方式來使用 coinductive，

但本文講的是它的 "old-way" coinductive。

從字元串說起

Agda 的內置字元串類型（ Agda.Builtin.String）是作為 postulate 定義的：

module Agda.Builtin.Stringpostulate String : Set{-# BUILTIN STRING String #-}

然後又 postulate 了一堆函數：

postulate primStringToList : String → List Charpostulate primStringFromList : List Char → Stringpostulate primStringAppend : String → String → Stringpostulate primStringEquality : String → String → Boolpostulate primShowString : String → String

很明顯這些函數是直接映射到目標語言的原生函數的。

但是這就直接導致這些函數以及 String 類型自己的性質無法被用於形式驗證了（因為實現對 checker 是不可見的），

所以十分雞肋（只能說可以運行時用用吧，但 Agda 基本都是不運行的）。

如果是需要 Haskell 的那種

type String = List Char

的 String 的話，又需要用 primStringToList 轉來轉去，十分 ~~鍵山雛~~ 麻煩。

之所以要研究這個，是因為我想試試在 Agda 里調用 putStrLn, whose 參數類型是 String。

然後我看向了標準庫（而不是內置庫）的 IO.Primitive.putStrLn 的實現：

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

看到 Costring 就應該知道這個應該是在外面被調用的，真正被使用的是 IO.putStrLn（就是所謂的『外面』），

所以我們可以看看 IO 里對 putStrLn 的實現：

import IO.Primitive as Priminfixl 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)

順帶一提，Unit 就是 ?，Agda.Builtin.IO（內置庫）和 IO（標準庫）是不一樣的，

所以標準庫把這個重寫了而不是單純地擴展內置庫。

這個時候如果你只看過我之前的博客（而不是早就知道這些東西），

你肯定充滿了疑問，那個 ∞ 是啥？ ? 是啥？ Costring 又是啥？

所以就引入了本文的正題， coinductive data type。

無窮的數據類型

假設你已經知道 Haskell 里的無窮序列的定義，如果不知道，你看了這個就知道了：

data Colist a = a :> Colist a

然後我們可以給它定義 cozipWith, cohead 和 cotail：

cozipWith :: (a -> b -> c) -> Colist a -> Colist b -> Colist ccozipWith f (a :> as) (b :> bs) = f a b :> cozipWith f as bscohead :: Colist a -> acohead (x :> _) = xcotail :: Colist a -> Colist acotail (_ :> xs) = xs

這個就是絕對 coinductive 的 List，它絕對不會是 inductive 的

（反觀 List 就可以是 inductive 的，因為它可以被 [1, 2, 3, 4] 這樣有限地構造。

即使它經常被當成 coinductive 地使用，因為 Haskell 語言層面就支持惰性數據結構）。

舉兩個應用的例子：

-- n 的無限序列repeat :: a -> Colist arepeat n = n :> repeat n-- 斐波那契數列的無限序列fib :: Integral n => Colist nfib = 0 :> 1 :> cozipWith (+) fib (cotail fib)

舉個 Colist 無法實現的 List 的使用例子：

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

如果你覺得剛掌握這個概念，對它還不太熟悉，想練習一下，那麼可以試試

這個 CodeWars Kata。

Agda 中的表示

看起來你已經懂了什麼是 coinductive data type 了，那麼在 Agda 中這玩意是怎麼表示的呢？

我們來看看 Agda 是怎麼定義 Colist 的：

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... 居然提供了 [] 這個構造器。。。

考慮到這裡可能是為了編譯到 Haskell 的 List 時更好地一一對應，就不吐槽了。

但這個玩意和 List 很明顯還是不一樣的，我們看到 _∷_ 這個構造器的第二個參數就知道事情並不簡單。

∞ 是什麼鬼，∞ (Colist A) 和 Colist A 有什麼區別，怎麼構造一個 ∞ (Colist A) 呢？

真相

事實上因為 Agda 和 Haskell 一樣沒有嚴格區分 GADT 的 coinductive 與否，

所以它引入了下面這三個音樂符號，一個作為 coinductive 的標記，兩個作為互相轉換的運算符：

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 Arepeat a = a ∷ repeat a

還可以藉助 ?_ 來假裝一個序列是無限序列，比如：

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

以及我們可以更方便地使用 inductive 版本的函數來輔助我們對 coinductive 版本的數據類型的使用：

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

而上文提到的 Costring 就是 Colist Char 而已。

拓展閱讀

• 更推薦的 coinductive 方式

推薦閱讀：