The Coq mailing list

[Dan Doel <dan.doel AT gmail.com>]

On Sunday 25 October 2009 11:00:03 am Jeffrey Harris wrote:
> Thank you for your detailed reply.

There's actually an even simpler implementation of plain coinductive types 
than Yves mentioned (although, not simpler than Nat -> A for Stream A). It's 
similar to a Church encoding of an inductive type; one encodes a coinductive 
type by the information needed to unfold it. So if your type is "ν X. F X", F 
being the shape functor (specifying the destructors), then the encoding is:

  νF = ∃ (S : Type). S × (S → F S)

  unfold step seed = (seed, step)
  observe (seed, step) = map (λ seed'. (seed', step)) (step seed)

I left the mucking with the existential quantification out of the above, but 
hopefully it's still comprehensible. This encoding might bump things up a 
universe level* (unless you use Set with impredicativity), but it actually 
mimics the underlying foundation of coinductive types pretty well. For 
instance, since Church encodings have weaker eliminators than their 
corresponding inductive type, you might expect the above encoding to be 
weaker 
in some way (I did), but equality proofs on coinductives (for instance) are 
extensional anyway, and the observation produces (presumably) a type with 
actual constructors, so perhaps things are covered. In fact, the dual of 
stronger eliminators might be stronger introduction rules for coinductives, 
but I couldn't come up with any such thing thinking about it for a while.

One significant difference with the coinductives in Coq is that this doesn't 
have issues with subject reduction. Values of νF are opaque, and all you can 
do is call "observe" on them, and use the result. They are not treated as 
actually being *made* out of the constructors of F, and subject to evaluation 
by case analysis. This means that there are things you can't prove about them 
that you could prove about Coq coinductives (for instance, way back I think 
someone showed how to prove intensional equality via bisimulation), but 
arguably, you shouldn't be able to prove them in Coq either.

The other issue is how well this extends to indexed types and families, 
which, 
I suspect it doesn't very nicely. But it does indicate that plain coinductive 
types aren't likely to give you increased computational power.

Cheers,

-- Dan

* I noticed while trying to do this in Agda that the universe bump makes this 
encoding extra painful, because "F νF" is not a valid construction. F has 
type 
Set -> Set, while νF has type Set1, so observe isn't well typed. 
Impredicativity solves this, of course, since νF : Set is allowed, but I 
think 
it might not actually be a problem in Coq even with Type, due to universe 
polymorphism. However, my Coq-fu is too weak to test this hypothesis, so it's 
an exercise left to the reader. :) I have got it working with Agda's 
experimental universe polymorphism:

data ℕ-Shape {i : Level} (X : Set i) : Set i where
  z : ℕ-Shape X
  s : X → ℕ-Shape X

map-ℕ : ∀{i j} {X : Set i} {Y : Set j} → (X → Y) → ℕ-Shape X → ℕ-Shape Y
map-ℕ f z     = z
map-ℕ f (s x) = s (f x)

data ∃ {i : Level} (T : Set i → Set i) : Set (suc i) where
  _,_ : (S : Set i) (t : T S) → ∃ T

Coℕ : Set₁
Coℕ = ∃ λ S → S × (S → ℕ-Shape S)

obs-Coℕ : Coℕ → ℕ-Shape Coℕ
obs-Coℕ (S , (seed , step)) =
  map-ℕ (λ seed' -> (S , (seed' , step))) (step seed)