## Stream: general

### Topic: seq and coinduction

#### Kenny Lau (Mar 27 2018 at 18:23):

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 (Mar 27 2018 at 19:16):

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 (Mar 27 2018 at 19:16):

except possibly the computation rules

#### Kenny Lau (Mar 27 2018 at 19:19):

and what is the name of the fixed point function?

#### Mario Carneiro (Mar 27 2018 at 19:20):

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

#### Kenny Lau (Mar 27 2018 at 19:22):

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

#### Mario Carneiro (Mar 27 2018 at 19:23):

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 (Mar 27 2018 at 19:24):

and then doing what?

#### Mario Carneiro (Mar 27 2018 at 20:17):

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 (Mar 27 2018 at 20:18):

no cycle [1,2,3]?

#### Mario Carneiro (Mar 27 2018 at 20:22):

You could, but then what is cycle []?

#### Mario Carneiro (Mar 27 2018 at 20:23):

this way that's syntactically impossible to give as input

#### Kevin Buzzard (Mar 27 2018 at 20:23):

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

#### Kevin Buzzard (Mar 27 2018 at 20:23):

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

I see

#### Mario Carneiro (Mar 27 2018 at 20:25):

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

Last updated: May 16 2021 at 05:21 UTC