native support of coinductive types / codata

Stream: new members

[Serhii Khoma (srghma)]

Could lean support

/-- Infinite lists -/
coinductive Stream α
  | cons : α → Stream α → Stream α

(as https://github.com/alexkeizer/QpfTypes does it) in a lean natively?

Does it make sense?

[Floris van Doorn]

Could? Potentially. But it's more likely that it will be implemented on top of the kernel instead of a kernel extension. Take a look at previous discussions, e.g. #lean4 > Coinduction? and the QPF paper.

[Serhii Khoma (srghma)]

So, special optimizations for types generated by Qpf. Would be good too

[Niels Voss]

You might be interested in this thread, which describes why the current representation of conductive types is inefficient, and how it might be improved: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Divergence.20monad

[Serhii Khoma (srghma)]

Niels Voss

Tnx, here is a summary

I have a question. Why not use church encoding everywhere for coinductive datatypes instead of QPF? Like I use for FreeMonad and Proxy

[Robin Arnez]

Church encoding doesn't allow for coinductive data types?

/-
coinductive CoStream (α : Type u) where
  | cons (x : α) (l : CoStream α) : CoStream α
-/
def CoStream (α : Type u) :=
  ∀ β : Type u,
    (α → β → β) → -- cons
    β

theorem costream_empty (x : CoStream α) : False :=
  (x PEmpty (fun _ x => x.elim)).elim

[Notification Bot]

3 messages were moved from this topic to #new members > power_in_kernel_of_finite_image by Matt Diamond.

[Aaron Liu]

Robin Arnez said:

Church encoding doesn't allow for coinductive data types?

/-
coinductive CoStream (α : Type u) where
  | cons (x : α) (l : CoStream α) : CoStream α
-/
def CoStream (α : Type u) :=
  ∀ β : Type u,
    (α → β → β) → -- cons
    β

theorem costream_empty (x : CoStream α) : False :=
  (x PEmpty (fun _ x => x.elim)).elim

I think you have to reverse it

[Serhii Khoma (srghma)]

def CoStream (α : Type u) :=
∀ β, (α → β → β) → β
That’s inductive: it consumes αs by folding them into β.

def CoStream (α : Type u) :=
∀ β, (Unit → α × β) → β
we now produce αs on demand, not consume them.

[Aaron Liu]

Serhii Khoma (srghma) said:

def CoStream (α : Type u) :=
∀ β, (Unit → α × β) → β
we now produce αs on demand, not consume them.

This also doesn't seem quite right, since it would mean that CoStream Empty is inhabited

[Robin Arnez]

Well, let's just say in general: The church encoding isn't really an option because:

1. You have universe bump (I mean inductive also exists to avoid a universe bump! (among other things))
2. You have lots of invalid values (e.g. values that depend on the types given)
3. You have to decide which universe to eliminate into (you can only choose one per type!)