Fin ForIn

Stream: lean4

[Patrick Massot]

Is there a ForIn instance on Fin n somewhere? Or are we meant not to need it?

[Patrick Massot]

Are we meant to rather use docs4#Std.Range.forIn or something like this?

[Mario Carneiro]

It's a bit weird to have an instance directly on numbers, what does it mean to say for x in (2 : Fin 5) do ...?

[Patrick Massot]

I meant for x in Fin 5 do ... of course.

[Patrick Massot]

So I guess I meant "a ForIn instance on Fin" not "on Fin n".

[Mario Carneiro]

It is a bit unfortunate that the current version of ForIn depends on a type rather than a value, since it means you can't have an instance for types directly to support for x in Fin 5 do .... One way to work around this is to have a wrapper type

structure AsType (a : A)

but then you still have to write for x in AsType.mk (Fin 5) do .... The most ergonomic version of the syntax under the current constraints that I can think of is:

class Elems (α : Type _) (σ : outParam (Type _)) where
  elems : σ
open Elems (elems)

structure FinStream (n : Nat) where
  pos : Nat

instance : Stream (FinStream n) (Fin n) where
  next? | ⟨i⟩ => if h : i < n then some (⟨i, h⟩, ⟨i + 1⟩) else none

instance : Elems (Fin n) (FinStream n) where
  elems := ⟨0⟩

#eval show Id (Array (Fin 5)) from do
  let mut j := #[]
  for i in elems (Fin 5) do
    j := j.push i
  pure j
-- #[0, 1, 2, 3, 4]

[Patrick Massot]

Thanks. Do you know whether such a solution would compile to something much slows than using Std.range?

[Mario Carneiro]

It is approximately the same as the Std.Range implementation, probably faster since it doesn't need a step size, except that this one uses the stream version instead of the direct ForIn impl.

[Patrick Massot]

Ok, nice.

[Mario Carneiro]

Here's an version which uses a direct implementation of ForIn. It is annoying that there are two ways to make forIn impls...

@[specialize] protected def FinStream.forIn {β : Type u} {m : Type u → Type v} [Monad m]
    (f : Fin n → β → m (ForInStep β)) (i : Nat) (b : β) : m β :=
  if h : i < n then do
    match (← f ⟨i, h⟩ b) with
    | ForInStep.done b  => pure b
    | ForInStep.yield b => FinStream.forIn f (i + 1) b
  else
    pure b
termination_by _ i _ => n - i

instance : ForIn m (FinStream n) (Fin n) where
  forIn i b f := FinStream.forIn f i.1 b

#reduce show Id (Array (Fin 5)) from do
  let mut j := #[]
  for i in elems (Fin 5) do
    j := j.push i
  pure j

[Mario Carneiro]

you can tell it is working because the #reduce at the end doesn't get stuck, unlike the previous example

[Mario Carneiro]

The stream version gets stuck in #reduce because it is using a partial function to implement the iteration. Making it work without partial requires std4#127

[Eric Wieser]

Can we hook into docs4#FinEnum here?

[Mario Carneiro]

yeah, the idea is similar to that, except not as antagonistic to producing fast code

[Mario Carneiro]

it wouldn't be hard to layer a LawfulElems typeclass over top which basically asserts that it produces all the elements, or alternatively it is given a FinEnum and asserts that it produces the same elements in the same order

[Patrick Massot]

Do you mean such a layer would allow to prove stuff about programs using your ForIn?

[Mario Carneiro]

well I should hope so

[Mario Carneiro]

any approach that doesn't use partial (either well founded streams or forIn instances) can in principle be proved to have some behavior, and you probably want to have LawfulElems if you actually need to know it exhausts the type

[Jesse Slater]

This is very nice!
I don't know the guidelines for what gets included in mathlib, but if Fin i -> alpha is the recommended tuple type, should these definitions be added to Mathlib.Data.Fin.Tuple.Reflection?

[Scott Morrison]

This sort of stuff is definitely desirable in Mathlib or Std. I think there is quite a bit of design work to do it, however: in the examples above Mario introduces Elems and FinStream which would both require API and integration with the library.

[Mario Carneiro]

I think it could be better handled by changing the desugaring of for ... in so that you can pass a type there