§ Simulating Inductives Via Coinductives (And Vice Versa)

• Given inductive types, it's fairly standard to simulate coinductives by writing them as an inverse limit of inductive types. For this, we need function spaces to write down the inverse limit sequence.

• What about the other way round? Given a language with $\Sigma$, $\Pi$, and coinductive, how do we simulate inductive?

§ Simulating List from Stream

• Step 1: define Stream a where head :: a; tail :: Stream a.
• Step 2: define church numerals:

type Church = (a -> a) -> (a -> a)

zero :: Church
zero f = id

succ :: Church -> Church
succ n f = (n f) . f

• We need one more ingredient, which is Option a.

type Tuple a b where
  fst :: a
  snd :: b

-- Final encoding of option.
type Option a = {b : Type} -> Tuple b (a -> b) -> b

none :: Option a
none tup = tup.fst

some :: a -> Option a
none a tup = tup.snd a

• We will define lists via the final encoding, and show that this type contains inhabitants.

-- List, final encoding.
type List a = (b : Type) -> (hnil : b) -> (hcons : b -> a -> b)

• We will inhabit it as a coinductive stream of Options, which are eventually none.

• First, a coinductive predicate that the stream has only nones.

coinductive OnlyNone (s : Stream (Option a)) : Prop where
  hdNone :: (hd s) = none
  tailNone :: OnlyNone (tail s)

• Next, a predicate that the stream is eventually only nones. For this, we say that there is a number $n$ such that applying $n$gives us a stream with OnlyNone.

type EventuallyNone (s : Stream (Option a)) : Prop := 
  ∃ (n : Church), OnlyNone ((n Stream.tail) s)

• Now, one can see that a List a is an EventuallyNone (Stream a).
• See that one ca also define Option a as a { s : Stream a // OnlyNone s \/ OnlyNone (tail s) }.
• In toto, this lets us simulate inductive types inside coinductive types, by building the large object, and then "cutting away" the subobject we want!
• See that we need function spaces to get ourselves an e.g. Option. In general, with just products, we can't get sums :)
• In some sense, we're using functions to build the "categorical" objects (inverse limits, sums) to get to the data type.