seq and coinduction

Stream: general

[Kenny Lau]

I see this comment in data.seq.seq:

/-
coinductive seq (α : Type u) : Type u
| nil : seq α
| cons : α → seq α → seq α
-/
 ```
Does this mean that `seq` is intended to be coinductive? Does that mean we can have co-fixed points?

[Mario Carneiro]

seq is intended to be coinductive, and it has co-fixed points. It has all the same properties you would expect of such a coinductive def, if it existed

[Mario Carneiro]

except possibly the computation rules

[Kenny Lau]

and what is the name of the fixed point function?

[Mario Carneiro]

corec I think, depending on what you mean by co-fixed point

[Kenny Lau]

I mean the sequence (1,2,1,2,...) being defined as X := 1,2,X

[Mario Carneiro]

We would need a better compiler to implement such a thing, but you can do it manually with a list storing the cycle

[Kenny Lau]

and then doing what?

[Mario Carneiro]

Here's an implementation of cycle for stream: cycle 1 [2, 3] = [1, 2, 3, 1, 2, 3, ...]

def  cycle {α} (a : α) (l : list α) : stream α :=
stream.corec' (λ al, match al with
| (b, []) := (b, a, l)
| (b, c::l') := (b, c, l')
end) (a, l)

[Kenny Lau]

no cycle [1,2,3]?

[Mario Carneiro]

You could, but then what is cycle []?

[Mario Carneiro]

this way that's syntactically impossible to give as input

[Kevin Buzzard]

if you did it in meta you wouldn't have to worry about this sort of thing, right?

[Kevin Buzzard]

and then you could just promise not to put [] in

[Kenny Lau]

I see

[Mario Carneiro]

You can promise not to put [] in in cycle as well: you could have an assumption l != [] which would be no fun to work with, or you could have A be inhabited so that it returns [default, default, ...] in that case, or you could return a seq so that this produces an empty seq