PR #1107 help needed with Satisfies

Stream: batteries

[Shreyas Srinivas]

Hello all, I need some help with working around this SatisfiesM predicate in batteries#1107

This PR is about adding some missing monadic defs for vectors (see the discussion in batteries#925). I am trying to extract the size guarantee of Array.size_modifyM (which uses Satisfies) to give me a proof that the size of the modified vector remains unchanged (around line 31). Conceptually I understand where my "proof" is going wrong. But I am not sure I know how to work around it.

[Shreyas Srinivas]

Update

On discord, we discussed using an [implemented_by] unsafe def ... with an unsafe cast on Array.modifyM to get a vector, and writing the safe version without using Array` defs. User Rob_23oba (who is not on Zulip) suggested something as follows:

@[inline]
unsafe def modifyMUnsafe [Monad m] (v : Vector α n) (i : Nat) (f : α → m α) : m (Vector α n) :=
  -- Array and Vector have the same internal representation, so this cast is valid
  unsafeCast (Array.modifyM v.toArray i f)

/--
`modifyM v i f` applies a monadic transformation `f` to `v[i]`
-/
@[implemented_by modifyMUnsafe]
def modifyM [Monad m] (v : Vector α n) (i : Nat) (f : α → m α) : m (Vector α n) := do
  if h : i < n then
    let x   := v[i]
    let x ← f x
    pure <| v.set i x
  else
    pure v

[Shreyas Srinivas]

The disadvantage is that of course one is always using the unsafe version for computations in practice.

[Shreyas Srinivas]

The advantage is that one doesn't need extra typeclass instances like LawfulMonad, LawfulFunctor and MonadSatisfying to use satisfying

[Shreyas Srinivas]

What is the community's opinion on this? CC : @Kim Morrison

[Kim Morrison]

No unsafe definitions here please, unless there are significant performance gains which are otherwise in inaccessible. In particular, not for the sake of proofs.

[Kim Morrison]

Why do you want the implemented_by here in the first place?

[Kim Morrison]

Note that for Array/Vector I'll soon be changing the signature, so modify takes an in-bounds proof and modifyIfInBounds preserves the current behaviour parallel to List.

[Shreyas Srinivas]

It was an idea to get around the challenge I described above. I need to show that the size of the vector after modifyM is n and I have very little experience with SatisfiesM

[Shreyas Srinivas]

So to use the satisfying function to extract the proof from Array.size_modifyM, I had to add a bunch of instances and the proof is still wrong. I can see why it is wrong, but not the fix.

[Kim Morrison]

What's wrong with the safe definition above? Just remove the implemented by.

[Shreyas Srinivas]

It might not be efficient. Last time I wrote my own defs for Vector I was told that it must use the array functions.

[Shreyas Srinivas]

To make sure the functions use FBIP