- 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 Σ, Π, 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 :: Churchzero f = idsucc :: Church -> Churchsucc 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) -> bnone :: Option anone tup = tup.fstsome :: a -> Option anone 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 ngives 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.