# 无限大的大小与余归纳数据结构

{-# OPTIONS --no-unicode  #-}
{-# OPTIONS --without-K   #-}
{-# OPTIONS --copattern   #-}
{-# OPTIONS --sized-types #-}

module MuGenHackingToTheGate where

open import lib.Basics

variable i : ULevel


## 停机性的重要性

module PleaseGoDieIfNotTerminate where
open import lib.types.Nat


  {-# NON_TERMINATING #-}
test2 : 1 + 1 == 3
test2 rewrite test2 = idp


1. 保证我们的函数停机
2. 说服编译器，让它认为我们的函数停机

## 传统定义

data Nat = O | S Nat deriving (Eq, Show)

mugen :: Nat
mugen = S mugen

minus :: Nat -> Nat -> Nat
minus O _ = O
minus a O = a
minus (S a) (S b) = minus a b

lessThan :: Nat -> Nat -> Bool
lessThan _ O = False
lessThan O _ = True
lessThan (S a) (S b) = lessThan a b

• lessThan a mugen 返回 True
• lessThan mugen a 返回 False
• minus mugen a 返回的东西还是 mugen
• minus a mugen 返回 O

Agda 是一个编译期 call-by-name，运行时 call-by-need 的语言，所以我们很明显可以定义出无限大的自然数。

module TranditionalNatMuGen where
{-# NON_TERMINATING #-}
mugen : Nat
mugen = S mugen


Termination checking failed for the following functions:
TranditionalNatMuGen.mugen
Problematic calls:
mugen

  testNeq : mugen ≠ 0
testNeq ()

Failed to solve the following constraints:
Is empty: mugen == FromNat.read ℕ-reader 0

Agda 有个旧方法可以实现 Coindutive 数据类型，HoTT-Agda 还封装了它：

import lib.Coinduction as OldWayCoinduction using ()


## 次时代余归纳数据结构

module NextGenerationCoinductiveDataTypes where


  Maybe : (A : Type i) -> Type i
Maybe A = Coprod Unit A


  module InductiveConat where
record Conat' : Type0 where
inductive
constructor nat
field
succ : Maybe Conat'
open Conat'


    toNat' : Conat' -> Nat
toNat' (nat (inl unit)) = O
toNat' (nat (inr x)) = S (toNat' x)

fromNat' : Nat -> Conat'
fromNat' O = nat (inl unit)
fromNat' (S n) = nat (inr (fromNat' n))


    -- 除以二
_/2 : Conat' -> Conat'
nat (inl unit) /2 = nat (inl unit)
nat (inr (nat (inl unit))) /2 = nat (inl unit)
nat (inr (nat (inr x))) /2 = nat (inr (x /2))


    _ = idp :> (toNat' (fromNat' 10 /2) == 5)
_ = idp :> (toNat' (fromNat' 11 /2) == 5)
_ = idp :> (toNat' (fromNat' 9 /2) == 4)
_ = idp :> (toNat' (fromNat' 0 /2) == 0)
_ = idp :> (toNat' (fromNat' 1 /2) == 0)
_ = idp :> (toNat' (fromNat' 2 /2) == 1)
_ = idp :> (toNat' (fromNat' 3 /2) == 1)


    proofNat' : forall n -> toNat' (fromNat' n) == n
proofNat' O = idp
proofNat' (S n) = ap S (proofNat' n)

proofNat'' : forall n -> fromNat' (toNat' n) == n
proofNat'' (nat (inl unit)) = idp
proofNat'' (nat (inr x)) = ap (nat ∘ inr) (proofNat'' x)


    conat-is-nat : Conat' == Nat
conat-is-nat = ua \$
equiv toNat' fromNat' proofNat' proofNat''


  record Conat : Type0 where
coinductive
constructor nat
field
succ : Maybe Conat
open Conat


  fromNat : Nat -> Conat
fromNat O = nat (inl unit)
fromNat (S n) = nat (inr (fromNat n))

-- toNat 暂时定义不了


  {-# NON_TERMINATING #-}


  _ = fromNat 233 :> Conat


• 写代码，构造出这个数据结构（如何构造，这是我们关心的重点
• 写代码，使用这个构造出来的数据结构

• 写代码，构造出这个数据结构，由于惰性求值，我们可以构造无限的数据结构
• 写代码，对它无限的东西进行有限地解构并使用（如何解构，这是我们关心的重点

• 通过 succ mugen 解构 mugen
• 返回的还是一个 mugen

  mugen : Conat
succ mugen = inr mugen


## 余归纳列表

data Stream a = a :>: Stream a

ones :: Stream Int
ones = 1 :>: ones

zipWith :: (a -> b -> c) -> Stream a -> Stream b -> Stream c
zipWith f (a :>: as) (b :>: bs) = f a b :>: zipWith f as bs

head :: Stream a -> a
head (a :>: _) = a

tail :: Stream a -> Stream a
tail (_ :>: as) = as

take :: Int -> Stream a -> [a]
take 0 _ = []
take n (a :>: as) = a : take (n-1) as

λ> take 5 ones
[1, 1, 1, 1, 1]

fib = 0 : 1 : zipWith (+) fib (tail fib)

### 普通的余归纳列表

  module SimpleCoinductiveList where
open import lib.types.List


    record Colist {i} (A : Type i) : Type i where
coinductive
constructor _:>:_
field
cotail : Colist A
open Colist


    ones : Colist Nat
cotail ones = ones


    cotake : {A : Type i} -> Nat -> Colist A -> List A
cotake O as = nil
cotake (S n) as = cohead as :: cotake n (cotail as)


    _ = idp :> (cotake 1 ones == 1 :: nil)
_ = idp :> (cotake 2 ones == 1 :: 1 :: nil)
_ = idp :> (cotake 3 ones == 1 :: 1 :: 1 :: nil)
_ = idp :> (cotake 4 ones == 1 :: 1 :: 1 :: 1 :: nil)
_ = idp :> (cotake 5 ones == 1 :: 1 :: 1 :: 1 :: 1 :: nil)
_ = idp :> (cotake 6 ones == 1 :: 1 :: 1 :: 1 :: 1 :: 1 :: nil)
_ = idp :> (cotake 7 ones == 1 :: 1 :: 1 :: 1 :: 1 :: 1 :: 1 :: nil)


    cozipWith : {A B C : Type i} -> (A -> B -> C)
-> Colist A -> Colist B -> Colist C
cotail (cozipWith f a b) = cozipWith f (cotail a) (cotail b)


    open import lib.types.Nat using (_+_)
{-# TERMINATING #-}
cofib : Colist Nat
cotail (cotail cofib) = cozipWith _+_ cofib (cotail cofib)


Ayayayayaya! 我们遇到了停机问题！ 编译器不知道 cozipWith 返回的 Colist 和传入的 Colist 的关系 （函数范围内的停机信息不会保留，这也是开头说的停机性判定迷的地方）， 导致了报错！

Termination checking failed for the following functions:
cofib
Problematic calls:
cofib

### 无限大的大小

open import Agda.Builtin.Size


• 不能被模式匹配
• 它的类型是 Size，这个类型独立于 Set 的类型体系
• 考虑到 Girard Paradox，我们给定 Size 本身的类型是 SizeU
• SizeU 也独立于 Set 的类型体系
• SizeU 需要 --type-in-type 这个 pragma
• 它的构造类似自然数，不过一般的用法不一样

• 函数拿一个隐式参数 s，类型是 Size
• 我们可以把这个 s 填进其他参数的类型参数里
• 返回值如果和参数大小相同
• 就给他们配上同一个 s
• 否则可以使用 Size<↑ 等函数创造新的 Size 并描述和 s 的关系
• Size 的默认值是无限大

open import lib.types.Nat

record Colist {i} (s : Size) (A : Type i) : Type i where
coinductive
constructor _:>:_


  field


    cotail : {ss : Size< s} -> Colist ss A


open Colist
variable s : Size


ones 的定义将不受影响：

ones : Colist s Nat
cotail ones = ones


cotake 由于处理的对象的长度是无所谓的，所以我们不需要使用 Size，就直接使用无限大这个 Size

open import lib.types.List
cotake : {A : Type i} -> Nat -> Colist ∞ A -> List A
cotake O as = nil
cotake (S n) as = cohead as :: cotake n (cotail as)


_ = idp :> (cotake 1 ones == 1 :: nil)
_ = idp :> (cotake 4 ones == 1 :: 1 :: 1 :: 1 :: nil)
_ = idp :> (cotake 7 ones == 1 :: 1 :: 1 :: 1 :: 1 :: 1 :: 1 :: nil)


cozipWith 可以使用一个 Size 来保留『返回的 Colist 长度和参数一致』这一细节，通过手动指定他们的 Size 都是同一个变量：

cozipWith : {A B C : Type i} -> (A -> B -> C)
-> Colist s A -> Colist s B -> Colist s C
cotail (cozipWith f a b) = cozipWith f (cotail a) (cotail b)


cofib : Colist s Nat
cotail (cotail cofib) = cozipWith _+_ cofib (cotail cofib)


_ = idp :> ((cotake 1 cofib) == O :: nil)
_ = idp :> ((cotake 5 cofib) == O :: 1 :: 1 :: 2 :: 3 :: nil)


_ = idp :> ((cotake 15 cofib) == O :: 1 :: 1 :: 2 ::
3 :: 5 :: 8 :: 13 :: 21 :: 34 :: 55 :: 89 ::
144 :: 233 :: 377 :: nil)


_ = idp :> ((cotake 28 cofib) == O :: 1 :: 1 :: 2 ::
3 :: 5 :: 8 :: 13 :: 21 :: 34 :: 55 :: 89 ::
144 :: 233 :: 377 :: 610 :: 987 :: 1597 :: 2584 ::
4181 :: 6765 :: 10946 :: 17711 :: 28657 :: 46368 ::
75025 :: 121393 :: 196418 :: nil)