String.getOp

Stream: lean4

[Arthur Paulino]

I saw this:

#check String.getOp -- String.getOp : String → String.Pos → Char

So I wonder, is this expected?

#eval ""[0] -- 'A'

[Sebastian Ullrich]

What is the question? Whether getOp should panic in that case?

[Arthur Paulino]

Hm, I would expect getOp to have type String → String.Pos → Option Char instead

[Sebastian Ullrich]

That would be inconsistent with all other getOp implementations

[Arthur Paulino]

Why doesn't getOp return Option x? I fear the current API risks making programmers not seeing errors in their code in some situations

[Arthur Paulino]

Like, if they assume some list/array/etc is not empty but in fact it is. And they don't see errors because getOp is returning something regardless

[Leonardo de Moura]

We have discussed this issue in the past. One of the proposals was:

• a[i]! panics if index out of bounds
• a[i]? returns Option
• a[i] uses proof and i is a Fin.

but, we never implemented this proposal. It is a good time to revisit this issue and decide what to do here before the first official release.

[Arthur Paulino]

(for some reason I imagined a cavalry of Python programmers spamming a[i]! all over their code - I am a Python programmer)

[Arthur Paulino]

• a[i]! panics if index out of bounds
• a[i]? returns Option
• a[i] uses proof and i is a Fin.

That makes total sense to me

[Leonardo de Moura]

Related issue https://github.com/leanprover/lean4/issues/406. @Andrew Kent suggested that all APIs that may panic should have a ! suffix.

[Leonardo de Moura]

Arthur Paulino said:

• a[i]! panics if index out of bounds
• a[i]? returns Option
• a[i] uses proof and i is a Fin.

That makes total sense to me

Great. It would be great to have more feedback from the community since this is a very disruptive change.

a[i]! all over their code - I am a Python programmer)

I suspect you are not the only one that will have a[i]! all over the place.

[Henrik Böving]

Leonardo de Moura said:

Arthur Paulino said:

• a[i]! panics if index out of bounds
• a[i]? returns Option
• a[i] uses proof and i is a Fin.

That makes total sense to me

Great. It would be great to have more feedback from the community since this is a very disruptive change.

a[i]! all over their code - I am a Python programmer)

I suspect you are not the only one that will have a[i]! all over the place.

If we end up doing this it could be worth to add a linter that tells you to maybe add ! to your function name if it could panic.

If this lint works recursively (that is if your function calls a function that could panic) it might end up being a little oppressive though since you could of course in theory be sure that you are not violating its invariants and it will never panic but the compiler keeps yelling at you (an option could be used to address this but people might end up being annoyed if there is too many "most likely false positives" they have to option away)

If it does not work recursively (so only check if you directly call to panic!) it could be a little too loose as well though so I'm not 100% sure whether it's worth to go through with it, we'll likely end up with something that either annoys people too much or doesn't annoy them enough :D

Just an idea^^

[Kyle Miller]

Sort of related to this, in a loop such as for i in [0:37] do ... I wonder if there could be some interface where [0:37] could provide some sort of membership proof if you were to write something like for h : i in [0:37] do .... I would imagine in this case the proof would be of 0 <= i /\ i < 37. This would help with any sort of proposal where a[i] uses i : Fin _.

There are other solutions to this, but this sort of feature might still be useful.

[Leonardo de Moura]

Kyle Miller said:

Sort of related to this, in a loop such as for i in [0:37] do ... I wonder if there could be some interface where [0:37] could provide some sort of membership proof if you were to write something like for h : i in [0:37] do .... I would imagine in this case the proof would be of 0 <= i /\ i < 37. This would help with any sort of proposal where a[i] uses i : Fin _.

There are other solutions to this, but this sort of feature might still be useful.

We already have the for h : i in [0:37] feature :)
See https://github.com/leanprover/lean4/blob/master/RELEASES.md for an example.

[Leonardo de Moura]

If we end up doing this it could be worth to add a linter that tells you to maybe add ! to your function name if it could panic.

That would be great :)

[Gabriel Ebner]

If we end up doing this it could be worth to add a linter that tells you to maybe add ! to your function name if it could panic.

To play the devil's advocate, how would you even prove that a function never calls panic? We have a wonderful proof language, but it cannot say anything about panics.

[Kyle Miller]

Maybe the panic checker could be like the Lean 3 noncomputability checker, where it makes a best-effort attempt to determine whether or not a function might panic, but it's not a proof per se. This is more subtle, though, since you'd want to record a predicate on a function's inputs that, when true, guarantee the function will not panic.

[Leonardo de Moura]

Kyle Miller said:

Maybe the panic checker could be like the Lean 3 noncomputability checker, where it makes a best-effort attempt to determine whether or not a function might panic, but it's not a proof per se. This is more subtle, though, since you'd want to record a predicate on a function's inputs that, when true, guarantee the function will not panic.

I was assuming the same kind of best-effort attempt, but it seems Gabriel's point is that we will have to add ! to a bunch of functions that depend on panic, but panic is not actually reachable.

[Leonardo de Moura]

It might still be useful to have this kind of linter if we add some kind of annotation for marking functions that should be viewed as "panic free" even if they depend on it.

[Kyle Miller]

Maybe this panic checker is like the termination checker, where if you can add hypotheses locally to try to automatically prove that the no-panic predicate for a given function application is true?

[Gabriel Ebner]

Nontermination is actually a good comparison because it's not syntactically evident and cannot be proven in Lean.

[Gabriel Ebner]

It's certainly vexing that you can prove your program correct, but then it panics or runs into an infinite loop when you run it and there's nothing you can do to rule it out.

[Gabriel Ebner]

Kyle Miller said:

This is more subtle, though, since you'd want to record a predicate on a function's inputs that, when true, guarantee the function will not panic.

Two more applications of this definedness predicate come to mind:

1. If the predicate is satisfied for the inputs of a partial def, then we should have a theorem that the partial def is equal to its body.
2. (Very speculatively) The predicate could also record whether all integrals, derivatives, etc., are well-defined.

[Gabriel Ebner]

Leonardo de Moura said:

I was assuming the same kind of best-effort attempt, but it seems Gabriel's point is that we will have to add ! to a bunch of functions that depend on panic, but panic is not actually reachable.

More pointedly, I think we would need to add ! to most definitions since lots of low-level functions use panic.

[Sebastian Ullrich]

Yes, most functions calling ! functions are supposed to never panic, so an opt-out lint might be a bit bothersome; just think of all the functions indexing into arrays without conclusively proving they're doing the right thing. Instead there could be a @[no_panic] opt-in annotation for people that really want to make sure.

[Sebastian Ullrich]

For conditionally panicking functions as well as their ?D variants, I still wonder if they should be captured by returning a common Option subtype a la { x : Option A // i < as.size -> x.isSome }. Then all the variants can be expressed as operations on this type. But it would require unboxed unions to avoid (most of) the Option overhead.

[Henrik Böving]

Yeah the false positives part is exactly the thing I was worrying about above as well, it might end up just being bothersome to the user.

[Kyle Miller]

Sebastian Ullrich said:

Yes, most functions calling ! functions are supposed to never panic, so an opt-out lint might be a bit bothersome; just think of all the functions indexing into arrays without conclusively proving they're doing the right thing. Instead there could be a @[no_panic] opt-in annotation for people that really want to make sure.

Maybe a concrete version of what I was proposing is that you might have an annotation like

@[no_panic idx < self.size]
def Array.getOp {α : Type u} [Inhabited α] (self : Array α) (idx : Nat) : α :=
  self.get! idx

and then the panic checker could try to prove that condition automatically wherever the function is used. In simple cases the panic checker could try to synthesize this condition for functions that call conditionally-panicking functions.

[Jannis Limperg]

If you can automatically prove this, then you can also provide the Fin needed for Array.get. I think serious software verification will always require that the code is syntactically panic-free (and implementedBy-free).

[Sebastian Ullrich]

Sebastian Ullrich said:

But it would require unboxed unions to avoid (most of) the Option overhead.

I completely forgot that I already had a solution for that... that I never wrote down until now

def Conditional (α : Type _) (cond : Prop) := cond → α

namespace Conditional
variable {cond : Prop}

@[inline] protected def get (c : Conditional α cond) (h : cond) : α := c h
@[inline] protected def get! [Decidable cond] [Inhabited α] (c : Conditional α cond) : α :=
  if h : cond then c.get h else panic! "in the disco"
@[inline] protected def get? [Decidable cond] (c : Conditional α cond) : Option α :=
  if h : cond then c.get h else none
@[inline] protected def getD [Decidable cond] (c : Conditional α cond) (default : α) : α :=
  if h : cond then c.get h else default

end Conditional

def Array.get' (as : Array α) (i : Nat) : Conditional α (i < as.size) :=
  fun h => as.get ⟨i, h⟩

-- test code generation
set_option trace.compiler.ir.result true
def Array.get!' [Inhabited α] (as : Array α) i := as.get' i |>.get!
def Array.getD' (as : Array α) i := as.get' i |>.getD
def Array.get?' (as : Array α) i := as.get' i |>.get?

As far as I can see, the generated code is optimal thanks to eta expansion

[Mac]

Gabriel Ebner said:

To play the devil's advocate, how would you even prove that a function never calls panic? We have a wonderful proof language, but it cannot say anything about panics.

I don't understand what you mean by this? If a definition has branch where it panics and a branch where it doesn't, it can be perfectly possible to prove that it does not panic for certain inputs (i.e., that the result is equal to that of the non-panicking branch). For example:

opaque does_not_panic : Nat
def panic_if_true! (b : Bool) : Nat :=
  if b then panic! "was true" else does_not_panic

theorem false_does_not_panic : panic_if_true! false = does_not_panic := by
  unfold panic_if_true!; simp

[Mac]

Leonardo de Moura said:

We have discussed this issue in the past. One of the proposals was:

• a[i]! panics if index out of bounds
• a[i]? returns Option
• a[i] uses proof and i is a Fin.

Sebastian Ullrich said:

I completely forgot that I already had a solution for that... that I never wrote down until now

def Conditional (α : Type _) (cond : Prop) := cond → α
-- [...]

I personally really like both of these approaches. The Conditional solution is much more general and flexible whereas the bracket macro solution is conveniently terse (but still clear).

It might even be possible to mix the two. For example, to ease the transition, getOp could return a Conditional and Coditional could have a Coe (Conditional a) a := (.get!) instance. This would make most current uses cases still work (due to the coercion). The []? and []! macros could be defined on top of this as shorthand for Conditional.get?/getD. Then, once users have shifted to the new approach, the Conditional coercion could be removed, and the [] could be change to Fin version if desired.

[Tomas Skrivan]

I'm also in favour of the notation: a[i]! a[i]? a[i]

Personally, on my own data types I already use the Fin version of a[i]. However instead of a[i]!, I have defined a macro !x that expands to ⟨x, sorry⟩, so I can write a[!i] where i is Nat.

[Tomas Skrivan]

With this change to the meaning of a[i], I would also point out that it might be worth to change the type of the index i in for i in [0:n] from Nat to Fin n. Or something along those lines, like notation for i in [n] to produce the Fin n index.

[Gabriel Ebner]

If a definition has branch where it panics and a branch where it doesn't, it can be perfectly possible to prove that it does not panic for certain inputs (i.e., that the result is equal to that of the non-panicking branch).

This is of course not nearly sufficient for panic-freeness:

def a : Nat :=
  let x := panic! "every time"
  x - x

#eval a  -- beautiful stacktrace

theorem a_does_not_panic?!? : a = 0 := by
  simp [a]

[Evgeniy Kuznetsov]

Why panic! doesn't require the unsafe attribute on a definition?

def List.get!' [Inhabited α] : List α → Nat → α
  | a::_,  0   => a
  | _::as, n+1 => get!' as n
  | _,     _   => panic! "invalid index"
termination_by _ l => sizeOf l
decreasing_by decreasing_tactic

Depending on lean_set_exit_on_panic and lean_set_panic_messages flags this pure function with explicit proof of termination performs I/O and throws a runtime exception. And when these flags aren't enabled (default behavior when building a binary executable) it could silently introduce a logical bug that is ten times worse.

With lean_set_panic_messages(true) Lean is lying about the type of this definition ([Inhabited α] → List α → Nat → IO α).
With lean_set_exit_on_panic(true) Lean is lying about termination of this function.
And without these flags enabled you won't know that something is going wrong.

Doesn't this compromise all static guarantees that Lean could provide?

[Sebastian Ullrich]

unsafe has a very precise definition: it can undermine memory safety. panic! can't.

[Sebastian Ullrich]

And as discussed above, it is quite hard to make a non-trivial Lean program panic-free, so it definitely should not require a viral annotation

[Gabriel Ebner]

unsafe has a very precise definition: it can undermine memory safety.

unsafe also has a second effect: it compromises logical soundness (to clarify: inside unsafe, that is). panic! is even true constructively.

[Evgeniy Kuznetsov]

I don't insist on this exact keyword, it can be anything else if you consider unsafe unsuitable.
Sebastian Ullrich said:

And as discussed above, it is quite hard to make a non-trivial Lean program panic-free, so it definitely should not require a viral annotation

Even implementedBy trick doesn't allow to effectively use such a viral annotation when writing a non-trivial program?

[Mac]

Gabriel Ebner said:

This is of course not nearly sufficient for panic-freeness.

Admittedly, sure, this is true in the context of adversarial examples as you point out. However, it still reasonable to do so in places where panic! is used in a conventional manner (for unproved invariant violations) and the goal is just to prove that the relevant invariant actually does hold and avoids the panic in a specific case. On the other hand, if the goal is oblivious zero trust panic safety, though, then no, it is not sufficient.

[Leonardo de Moura]

Pushed the proposal:

• a[i]! panics if index out of bounds
• a[i]? returns Option
• a[i] uses proof and i is a Fin.

It is quite disruptive, but it is better now than after the first official release at the end of the summer.
The Array type implements the three notations.
The String type currently only implements the a[i]?, and String.get still returns a default value for invalid positions.
We also have the notation a[i, h] as sugar for a[⟨i, h⟩]

[Mac]

Leonardo de Moura said:

We also have the notation a[i, h] as sugar for a[⟨i, h⟩]

Design question: Would it be possible/reasonable to have a[i, h] expand to yet another getOp version that takes the index and hypothesis as separate parameters (e.g., Array.uget)? This could avoid the potential boxing/unboxing overhead that comes with Fin and remove the need for other types which have an index condition and use the syntax to have a Subtype-like structure (or directly use Subtype)? Just a thought, not sure how reasonable/worthwhile of an idea it is.

[Tomas Skrivan]

I'm not sure about the notation a[i, h]. What about multi dimensional arrays, I would like to have a notation a[i, j] for matrices. Wouldn't be there a clash?

[Tomas Skrivan]

Also at some point I would like to experiment with notation a[:, j] for slices i.e. j-th column of a matrix . It would be nice if the notation would not clash with that either. (Not saying it does right now but it would be nice to keep this in mind when doing further changes)

[Tomas Skrivan]

One thing I do not understand, is why is the notation a[i] done with getOp which has special requirements on argument names etc. Why it is not a simple macro/notation for a.get i ? My guess, is it related to Lean's bootstrapping?

[Xubai Wang]

Is it possible to have a GetOp typeclass to reuse this syntax for different index types (like Nat, Range, Nat × Nat , Fin and Nat × Prop) at the same time?

[Xubai Wang]

For example：

class GetOp (α : Sort u) (β : α → Sort v) (γ : outParam (Sort w)) where
  getOp : (a : α) → β a → γ

class GetOp? (α : Sort u) (β : Sort v) (γ : outParam (Sort w)) where
  getOp? : α → β → γ

/-!
For Lists
-/

-- as[⟨n, h⟩]
instance : GetOp (List α) (Fin ∘ List.length) α where
  getOp as n := as.get n

-- as[n, h]
instance : GetOp (List α) (λ as => (n : Nat) ×' n < as.length) α where
  getOp as x := as.get ⟨x.fst, x.snd⟩

-- as[n]?
instance : GetOp? (List α) Nat (Option α) where
  getOp? as n := as.get? n

-- as[[m:n]]
instance : GetOp (List α) Range (List α) where
  getOp as r := sorry

/-!
Matrix m[i, j]
-/
instance : GetOp? (Matrix α) (Nat × Nat) := sorry

[Tomas Skrivan]

I'm a bit unsure if a[i, j] should be a shorthand for a[i][j] or a[(i, j)].

Effectively, do you understand matrix as Fin n -> Fin m -> Float or as Prod (Fin n) (Fin m) -> Float.

The second one might be boxing those indices unnecessarily.

[Xubai Wang]

The detailed decision is up for who implements it. Also I think boxing (dereferencing) may not be a big overhead in the future, since we will have stack allocated value "soon"?

[Leonardo de Moura]

Thanks for the feedback. I will remove the a[i, h] for now. The issue raised by @Tomas Skrivan was also exposed by one of our tests, and I used priorities to override the notation.
https://github.com/leanprover/lean4/commit/a0fdc2d05049ecbaf21f57e9cc4a997e0c6bed91
I will post other messages discussing how the notation works and other suggestions.

[Leonardo de Moura]

We often have to decide whether we should use "dot-notation" (aka namespace-oriented) or "type classes". I am coping here a thread we had in the dev channel last year. It describes the "pros" and "cons" of each approach, and examples.

type classes pros

• Chaining. That is, given an instance ToString A, we can create an instance ToString (List A)
• We can write polymorphic methods

def f [ToString a] (x : a) :=
   ">> " ++ toString a

type classes cons

• Depends heavily on unification. Moreover, it becomes quite unreliable when higher-order unification has to be used. This is often an issue when we want to make a polymorphic method as general as possible. More about this later.
• Universe constraints. It is part of the unification problem described in the previous item, but it is often overlooked since the universes are often implicit.
• We don't want type class resolution to assign metavariables occurring in input parameters. So, TC often fails in scenarios we don't have sufficient information. The new defaultInstance feature minimizes this problem.

dot-notation pros

• Low tech and predictable. Given x : C as, x.foo is notation for C.foo x. The parameters as may contain metavariables.
• Allow non-uniform signatures. That is, C.foo and D.foo may have completely different types.

dot-notation cons

• No support for chaining
• No support for writing polymorphic functions. That is, we can't write

def f {A : Type} (a : A) :=
  a.toString

An Example: the x[i] notation

In the master branch, x[i] is a notation based on the dot-notation. That is, given x : C as, it is a notation for x.getOp i.
This is flexible since the type of i may or may not depend on x, the result type may or may not depend on x and/or i, and the only information the elaborator needs is the head symbol C, and as may contain a bunch of metavariables.

Now, suppose we have used a type class GetElem for implementing the notation x[i]. The first try would be:

class GetElem (ρ : Type u) (ι : outParam $ Type v) (α : outParam $ Type w) where
  getElem : ρ → ι → α

The problem here is that there isn't support for dependencies. For example, we can't implement getElem using

def Array.get {α : Type u} (a : Array α) (i : Fin a.size) : α :=
...

since the index i depends on a.
Then, we may try to define a more general GetElem

class GetElem (ρ : Type u) (ι : outParam (ρ → Type v)) (α : outParam ((c : ρ) → ι c → Type w)) where
  getElem : (c : ρ) → (i : ι c) → α c i

Then, we can add instances such as

instance : GetElem (Array α) (fun a => Fin a.size) (fun _ _ => α) where
  getElem a i := a.get i

instance (lt : α → α → Bool) (β : α → Type v) : GetElem (RBMapDep α β lt) (fun _ => α) (fun _ i => Option (β i)) where
  getElem a i := a.find? i

Everything looks great until we try to use getElem. The problem is that it generates nontrivial higher-order unification problems.
Note that the type of i at t[i] is of the form ?m t. Suppose we have t : Array Nat, after we resolve the TC problem, we have to solve the unification problem ?m t =?= Fin t.size. Even a simple version where t is just a variable and we don't take into account reduction, we have two solutions

?m := fun x => Fin x.size
?m := fun _ => Fin t.size

In this particular case, the first solution is the right one, but, in general, there is no way to decide. In Lean 2, we have tried to transform elaboration into a constraint solving problem, but the performance was bad, and error messages that are very hard to understand.
So, I don't see how to have classes that rely on higher-order unification and are reliable in practice.

[Leonardo de Moura]

Mac said:

Leonardo de Moura said:

We also have the notation a[i, h] as sugar for a[⟨i, h⟩]

Design question: Would it be possible/reasonable to have a[i, h] expand to yet another getOp version that takes the index and hypothesis as separate parameters (e.g., Array.uget)? This could avoid the potential boxing/unboxing overhead that comes with Fin and remove the need for other types which have an index condition and use the syntax to have a Subtype-like structure (or directly use Subtype)? Just a thought, not sure how reasonable/worthwhile of an idea it is.

This is an interesting suggestion, but the "function selection process" would have to depend on the type of the index too. The current dispatch is based only on the type of a. Note that, given a : Array Int when we type a[_], the hole has type Fin a.size.
If we move to type-classes, then we have the problems described in the previous comment.

[Leonardo de Moura]

Tomas Skrivan said:

One thing I do not understand, is why is the notation a[i] done with getOp which has special requirements on argument names etc. Why it is not a simple macro/notation for a.get i ? My guess, is it related to Lean's bootstrapping?

The notation uses the "dot notation" (aka namespace-based) approach described above.

[Mac]

Leonardo de Moura said:

[T]he "function selection process" would have to depend on the type of the index too. [..] If we move to type-classes, then we have the problems described in the previous comment.

What if we combined the two? That is, what if we used type class synthesis for the "function selection process" and once found, expanded it via a macro. For example:

import Lean
open Lean Elab Meta Term

class GetOp (ρ : Type u) where
  op : Name

instance : GetOp (Array α) := ⟨``Array.getOp⟩

unsafe def unsafeEvalExpr (α) [ToExpr α] (e : Expr) : TermElabM α :=
  Meta.evalExpr α (toTypeExpr α) e

@[implementedBy unsafeEvalExpr]
opaque evalExpr (α) [ToExpr α] (e : Expr) : TermElabM α

elab a:term noWs "[" i:term "]'" : term => do
  let e ← elabTerm a none
  synthesizeSyntheticMVarsNoPostponing
  let α ← inferType e
  let u ← getDecLevel α
  let inst := mkApp (mkConst ``GetOp [u]) α
  let instVal ← synthInstance inst
  let ope ← instantiateMVars (mkAppN (mkConst ``GetOp.op [u]) #[α, instVal])
  let op ← evalExpr Name ope
  let stx ← `($(mkCIdent op) $a $i)
  withMacroExpansion (← getRef) stx <| elabTerm stx none

#eval #[0, 1, 2][1]' -- 1

This would enable the chain benefits of type classes, while avoiding the unification problem.

[Arthur Paulino]

My two cents: I was expecting the proof in a[i] to go after the brackets, as in a[i] h, as if it were replacing the ! or ?

[Sebastian Ullrich]

Coincidentally that's exactly what you'd have to/could do if a[i] returned Conditional

[Leonardo de Moura]

@Mac

What if we combined the two? That is, what if we used type class synthesis for the "function selection process" and once found, expanded it via a macro. For example:

One nice feature of your approach is that we can use scoped instances and instance priorities to select which function is used to implement a[i]. For example, we could have

namespace Array.unsafeReads
scoped instance : GetOp (Array α) := ⟨``Array.get!⟩
end Array.unsafeReads

#eval #[0, 1, 2][⟨1, by decide⟩]'  -- index is a Fin
open Array.unsafeReads
#eval #[0, 1, 2][1]'  -- index is a Nat

This is good. On the other hand, it feels like an abuse of the type class resolution feature. We would be using it to implement a mapping from type to function name. Let's see what others have to say about this.

[Sebastian Ullrich]

A typeclass solution that is not parameterized over the index type (like in Rust, for prior work) to me just feels... disappointing. It's neither here nor there.

[Leonardo de Moura]

Sebastian Ullrich said:

A typeclass solution that is not parameterized over the index type (like in Rust, for prior work) to me just feels... disappointing

Yes, it is disappointing, but Rust does not have dependent types. So, they can avoid the higher-order unification problems introduced by a type class such as:

class GetElem (ρ : Type u) (ι : ρ → Type v) (α : outParam ((c : ρ) → ι c → Type w)) where
  getElem : (c : ρ) → (i : ι c) → α c i

Because they can simply use

class GetElem (ρ : Type u) (ι : Type v) (α : outParam (Type w)) where
  getElem : ρ →  ι  → α

[Leonardo de Moura]

Sebastian Ullrich said:

Coincidentally that's exactly what you'd have to/could do if a[i] returned Conditional

The Conditional proposal streamlines the definition of get?, get!, etc. This is good, but I have two concerns.

• If i : Fin a.size, we would have to write a[i.val] i.isLt
• It may impact the compilation times. The code generator is creating/eliminating joint-points as it inlines these definitions to eliminate the overhead.

[Sebastian Ullrich]

Would this be a defensible use case for [macroInline]? I haven't checked the resulting IR yet, or whether it avoids the join points.

[Sebastian Ullrich]

Leonardo de Moura said:

• If i : Fin a.size, we would have to write a[i.val] i.isLt

Yes. We can keep it as taking Fin and use Conditional.get in its implementation.

[Leonardo de Moura]

Sebastian Ullrich said:

Would this be a defensible use case for [macroInline]? I haven't checked the resulting IR yet, or whether it avoids the join points.

Not sure it would work. The code generator would still find the nested if-then-else.

[Leonardo de Moura]

Sebastian Ullrich said:

Leonardo de Moura said:

• If i : Fin a.size, we would have to write a[i.val] i.isLt

Yes. We can keep it as taking Fin and use Conditional.get in its implementation.

Not sure whether it is worth the trouble.

[Leonardo de Moura]

I can see a substantial improvement if we can solve the higher-order unification problems generated by a type-class like

class GetElem (ρ : Type u) (ι : ρ → Type v) (α : outParam ((c : ρ) → ι c → Type w)) where
  getElem : (c : ρ) → (i : ι c) → α c i

We could try to write a custom elaboration function for getElem applications. We have implemented similar custom elaborators before (e.g., ▸ for Eq.subst). It is hard to tell how well it would work.
If we succeed, we would be able to write

instance [Inhabited α] : GetElem (Array α) (fun _ => Nat) (fun _ _ => α) where
  getElem a i := a.get! i

instance : GetElem (Array α) (fun a => Fin a.size) (fun _ _ => α) where
  getElem a i := a.get i

instance : GetElem (Array α) (fun _ => USize) (fun (a : Array α) (i : USize) => i.toNat < a.size → α) where
  getElem a i := a.uget i

We would still need a[i]? for the Option case, or use a scoped instance for it.

[Sebastian Ullrich]

I was thinking along similar lines, that I would love to tell the elaborator not to bother creating the HO problem regarding i : ?m c, but that i : ?m' is enough for now until TC resolution is done. It seems like typeclasses like this will be a reoccurring issue.

[Leonardo de Moura]

Sebastian Ullrich said:

I was thinking along similar lines, that I would love to tell the elaborator not to bother creating the HO problem regarding i : ?m c, but that i : ?m' is enough for now until TC resolution is done. It seems like typeclasses like this will be a reoccurring issue.

It is not clear to me how your proposal would work. When using the GetElem type class above, we have to infer ρ and ι before we invoke the TC resolution procedure. To infer ι, we need higher-order unification.

[Leonardo de Moura]

It seems like typeclasses like this will be a reoccurring issue.

I agree. If we solve it for GetElem, we can try to generalize the solution.

[Sebastian Ullrich]

Oh, I falsely assumed ι was an outParam. I don't know if it should be one, but that would be the closer modelling compared to the current design I think.

[Leonardo de Moura]

If ι is an outParam, I don't see a big motivation for moving to type classes. We would be able to use scoped instances to select different implementations like in @Mac's proposal. Note that @Mac's proposal completely avoids all ho-unification issues.

[Sebastian Ullrich]

ι not being an outParam would be the strongest point in favor for type classes to me, to enable overloading of the index type. But I don't see how to reconcile that with the HO issues, yeah.

[Henrik Böving]

I have a slightly more general question regarding this, my knowledge of ho-unification is that:

• it is not decidable
• is related to dependent types
• and apparently a pretty big issue

But i never really understood what it is, could someone explain to me what the issue arising with this type class would be?

[Leonardo de Moura]

@Henrik Böving In the higher-order case, the metavariables can be functions. Even the simply-typed case is already a mess. Consider the following unification problem.

?m a =?= f a a

Here are some possible solutions

?m := fun _ => f a a
?m := fun x => f x a
?m := fun x => f a x
?m := fun x => f x x

[Henrik Böving]

ah and thus solving the alpha parameter doesn't work out nicely, yes?

[Leonardo de Moura]

Given a : Array Int, i : Nat, If a[i] is a notation for GetElem.getElem a i, then before invoking TC, we would have to solve the constraints

?ρ =?= Array Int -- Easy case
?ι a =?= Nat -- nasty case

The "right" solution for the example above is

?ρ := Array Int
?ι  := fun _ => Nat

We have to solve unification problems such as ?ι ?ρ =?= Nat in other parts of the system (e.g., computing the motive for induction).
However, in each one of these cases we do not use the general isDefEq, but a custom heuristic that is usually based on "waiting" for information, and using the kabstract function.

[Sebastian Ullrich]

And in this case, waiting would only make sense if ι is an outParam. Correct?

[Henrik Böving]

Waiting in the same sense as postponing execution in term elaboration I guess?

[Leonardo de Moura]

Sebastian Ullrich said:

And in this case, waiting would only make sense if ι is an outParam. Correct?

Sorry, I was vague. I was referring to the case that it is not an outParam. The idea is to wait for a and the type of i to be fully "available" (i.e., they do not contain nested metavariables). Then, we compute ι by using kabstract <type-of-i> <a>.

[Sebastian Ullrich]

I see! Ideally i : Fin ?m would be sufficient to trigger TC resolution, but your idea would already be quite good.

[Gabriel Ebner]

We could also put the domain as an extra argument to the type class, avoiding dependencies:

class GetElem (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) (Dom : outParam (Cont → Idx → Prop)) where
  getElem (xs : Cont) (i : Idx) (h : Dom xs i) : Elem

export GetElem (getElem)

def getElem! [GetElem Cont Idx Elem Dom] [Inhabited Elem] (xs : Cont) (i : Idx) [Decidable (Dom xs i)] : Elem :=
  if h : _ then getElem xs i h else unreachable!

def getElem? [GetElem Cont Idx Elem Dom] (xs : Cont) (i : Idx) [Decidable (Dom xs i)] : Option Elem :=
  if h : _ then some (getElem xs i h) else none

macro "linarith" : tactic => `(first| trivial | decide | assumption) -- TODO
macro (priority := high) x:term noWs "[" i:term "]" : term => `(getElem $x $i (by linarith))
macro (priority := high) x:term noWs "[" i:term "]?" : term => `(getElem? $x $i)
macro (priority := high) x:term noWs "[" i:term "]!" : term => `(getElem! $x $i)

instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
  getElem xs i h := xs.get ⟨i, h⟩

instance : GetElem (Array α) Std.Range (Array α) fun _ _ => True where
  getElem xs i _ := xs.extract i.start i.stop

#eval #[1,2,3][2]
#eval #[1,2,3][[1:3]]

[Leonardo de Moura]

@Gabriel Ebner I think this proposal is cleaner than the Conditional one. Perhaps, we should just accept the fact that the Idx cannot depend on the collection. That is, we can't write instance : GetElem (Array α) (Fin ??) .... Perhaps this is acceptable. We can still write instance : GetElem (Vector α n) (Fin n) ...

[Mac]

Here is a version of my proposal that allows the operation to be dependent on the index:

import Lean
open Lean Elab Meta Term

class GetOp (ρ : Type u) (r : ρ) (ι : Type v) where
  op : Name

instance : GetOp (Array α) as Nat := ⟨``Array.getOp⟩
instance : GetOp (Array α) as USize := ⟨``Array.uget⟩
instance : GetOp (Array α) as (Fin as.size) := ⟨``Array.get⟩

unsafe def unsafeEvalExpr (α) [ToExpr α] (e : Expr) : TermElabM α :=
  Meta.evalExpr α (toTypeExpr α) e

@[implementedBy unsafeEvalExpr]
opaque evalExpr (α) [ToExpr α] (e : Expr) : TermElabM α

elab:max a:term noWs "[" i:term "]'" : term => do
  let ax ← elabTerm a none
  let ix ← elabTerm i none
  synthesizeSyntheticMVarsNoPostponing
  let ρ ← inferType ax
  let ι ← inferType ix
  let u ← getDecLevel ρ
  let v ← getDecLevel ι
  let inst := mkAppN (mkConst ``GetOp [u, v]) #[ρ, ax, ι]
  let instVal ← synthInstance inst
  let opApp := mkAppN (mkConst ``GetOp.op [u, v]) #[ρ, ax, ι, instVal]
  let opVal ← instantiateMVars opApp
  let op ← evalExpr Name opVal
  let stx ← `($(mkCIdent op) $a $i)
  withMacroExpansion (← getRef) stx <| elabTerm stx none

#eval #[0, 1, 2][1]' -- 1
#eval #[0, 1, 2][(1 : USize)]' (by native_decide) -- 1
#eval #[0, 1, 2][Fin.mk 1 (show 1 < #[0, 1, 2].size from by decide)]' -- 1

[Mac]

What do you think @Leonardo de Moura / @Sebastian Ullrich / @Gabriel Ebner ?

[Tomas Skrivan]

For me personally, finding out a class GetOp that asks for Name instead of the expected function would be a huge wtf moment. Might not be an issue if this becomes a common pattern or the user side interface is a bit more sane.

[Leonardo de Moura]

@Mac I agree with Tomas, the hack is getting too complicated, and the code above does not have support for postponing elaboration yet. Another problem is that mechanisms such as [defaultInstances] will not work with your approach.

[Sebastian Ullrich]

A nice benefit of having _[_] default to a tactic search is that we can give a very clear error message if it fails, even explaining Lean's indexing approach to newcomers that invariably try to apply the standard indexing notation.

[Gabriel Ebner]

We can also make the search tactic do the right thing for Fins out of the box. Then nobody will notice that _[_] doesn't support Fin:

instance [GetElem Cont Nat Elem Dom] : GetElem Cont (Fin n) Elem fun xs i => Dom xs i where
  getElem xs i h := getElem xs i.1 h

theorem foo (h : a < b) : Fin.mk a h < b := h
macro_rules | `(tactic| linarith) => `(tactic| · apply foo)

#check fun (xs : Array Nat) (i : Fin xs.size) =>  xs[i]

[Tomas Skrivan]

Can't the Mac's approach be done with an attribute? I.e. tagging functions that follow certain pattern instead of using an odd type class.

[Tomas Skrivan]

A bit tangentially related, would it be possible to get a[i] displayed in the goal view as a[i] and not as Array.getOp a i?

mwe:

def a := #[0,1,2]
def i : Fin a.size := ⟨0, by decide⟩

example : a[i] = 0 := by
  trace_state
  simp
  done

Displays Array.getOp a i = 0 instead of a[i] = 0. It makes lots of stuff I work with quite unreadable.

[Henrik Böving]

Specifically for Array.getOp it's possible with an appUnexpander:

import Lean
open Lean PrettyPrinter

@[appUnexpander Array.getOp]
def unexpandGet : Unexpander
  | `(Array.getOp $array $index) => `($array[$index])
  | _ => throw ()

def a := #[0,1,2]
def i : Fin a.size := ⟨0, by decide⟩

example : a[i] = 0 := by
  trace_state
  simp
  done

Traces

⊢ a[i] = 0

But generalizing this to all getOps (as they are currently implemented) might require some manual work or magic in the compiler to treat getOp applications to any type specially.

Depending on the implementation suggestions from above it would also be doable with varying degrees of complexity, if we end up with a pure type class it should be trivial because there is only one unexpander required, if we do it with the attribute the thing that handles the attribute would have to generate an unexpander specifically etc.

[Tomas Skrivan]

Ohh I see, this solution is good enough for me for now. I just add this bit of code to every place where I provide getOp.

[Leonardo de Moura]

@Gabriel Ebner's proposal above is now on master. Please update your projects, and thanks for your patience with these changes before the first official release. The proposal seems to be working well after a few improvements to our elaborator.

[Leonardo de Moura]

Please see release notes for additional details: https://github.com/leanprover/lean4/blob/49951b87b953c7cf74f415c1dc1488ae26921cf2/RELEASES.md

[Mac]

@Leonardo de Moura Very cool! :heart: One suggestion, though: instead of a[i]'h for index-with-proof-syntax, how about just a[i](h)? Most of the examples that use a[i]'h already end up doing a[i]'(h) so this would be shorter and, in my view, cleaner and clearer.

[Tomas Skrivan]

I'm also not sure about the a[i]'h notation. What about a[i|h] or a[i;h]?

[Tomas Skrivan]

Cool works nicely! A quick test to find out if notation like ∑ i, b[i] works correctly:

def sum (f : α → β) : β := sorry

macro "∑" xs:Lean.explicitBinders ", " b:term : term => Lean.expandExplicitBinders `sum xs b

def NArray (α : Type) (n : Nat) := {a : Array α // n = a.size}

@[defaultInstance]
instance : GetElem (NArray α n) (Fin n) α (λ _ _ => True) where
  getElem xs i _ := xs.1.get (xs.2 ▸ i)

variable (b : NArray Nat 10) (i : Fin 10)

#check b[i]
#check ∑ i, b[i]   --- works as expected!

[Tomas Skrivan]

However I'm unable to get the unexpander working. This does not work:

@[appUnexpander GetElem.getElem]
def unexpandGet : Unexpander
  | `(GetElem.getElem $array $index _) => `($array[$index])
  | _ => throw ()

However, there is a bit ambiguity how to unexpand it, do you want a[i] ora[i]'h. I would like to apply the above unexpander only if Dom = (λ _ _ => True).

[Henrik Böving]

For the unexpander there are two mistakes on your side, both related to how syntax works:

1. GetElem.getElem is syntactically not equivalent to getElem which is what the macro uses so every occurence of the macro won't match this here already
2. _ is interpreted as a literal syntactic _ here, you want an antiquotation $_

And then we get:

import Lean
open Lean PrettyPrinter

@[appUnexpander GetElem.getElem]
def unexpandGet : Unexpander
  | `(getElem $array $index $_) => `($array[$index])
  | _ => throw ()

def a := #[0,1,2]
def i : Fin a.size := ⟨0, by decide⟩

example : a[i] = 0 := by
  trace_state
  simp
  done

which traces

⊢ a[i] = 0

[Tomas Skrivan]

Ahh thanks! I was slowly uncovering 1 but had no clue about 2.

[Tomas Skrivan]

Should it be @[appUnexpander GetElem.getElem] or @[appUnexpander getElem]? ... both work.

[Henrik Böving]

I guess I'd use the 2nd since it is what the unexpander in question actually cares about? But I don't know whether it makes a difference.

I'm also not quite sure how to adapt the unexpander to correctly make a difference between the cases where a 'h and none was used, for example

def foo1 (a : Array Int) (i : Nat) (h : i < a.size) : Int :=
  a[i] -- Ok

with

@[appUnexpander GetElem.getElem]
def unexpandGet : Unexpander
  | `(getElem $array $index $h) => `($array[$index]'$h)
  | _ => throw ()

turns into

fun a i h => a[i]'h

so there is virtually no difference between a[i]'h and a[i] with the h inferred via tactic on a syntactic level at this point.

[Tomas Skrivan]

Yeah, I'm not sure what to do about that. That is why I wanted to do the unexpander only for Dom = (λ _ _ => True) i.e. when the domain proof is trivial. Maybe, in all other cases unexpand to a[i]'h ?

[Leonardo de Moura]

Tomas Skrivan said:

I'm also not sure about the a[i]'h notation. What about a[i|h] or a[i;h]?

The a[i]' h notation is based on the following suggestion from @Arthur Paulino

My two cents: I was expecting the proof in a[i] to go after the brackets, as in a[i] h, as if it were replacing the ! or ?

The only difference is the '.
It would be great to have a consensus here. I don't have a strong preference here, but I found this variant useful when fixing the Lean 4 repo.

[Leonardo de Moura]

@Henrik Böving Thanks for the feedback. I will add an abbreviation for a[i] ' h. Thus, we can use it in the unexpander.

[Leonardo de Moura]

Pushed https://github.com/leanprover/lean4/commit/35018dbea24dd92d5f75b02a9faa8bbf57a5496d

[Sebastian Ullrich]

Since there doesn't seem to be an immediately natural syntax for a[i]'h, I think it's worth discussing whether we need one at all. Especially if we assume that most short proofs will eventually be automated by e.g. linarith anyway, and for everything longer than one line any such notation seems problematic. Still, sometimes you might not want to type out the proposition for a separate have (though auto-generating that skeleton from a Code Action would be cool). Since we already have other such "implicitly proof-consuming" syntax with well-founded recursion, I'm wondering whether we should have a general syntax for discharging remaining proof obligations from terms on the command level, like with Coq's Program/Obligation.

example (a : Array Int) (h : a.size = 2) : Int :=
  a[0]
where
  case «a[0]» =>  -- should also accept a default like `case _`
    rw [h]; decide

[Sebastian Ullrich]

For further motivation, imagine repeating the same syntax discussion for a proof-consuming division operator :) ...

[Henrik Böving]

I think having a user extensible framework for proof consuming operators is a great idea :thumbs_up:

[James Gallicchio]

my only concern would be that the connection between the written code and the underlying terms might get a bit further separated -- like, to me, the termination_by is a magic wand that I do not understand, but it's okay because I never have to really interact with the underlying rec definition, just with the equational lemmas...

[James Gallicchio]

whereas I fully expect users to have to interact with getElem and its corresponding proof terms

[Sebastian Ullrich]

When would you interact with its proof terms?

[James Gallicchio]

If you're doing any proof with a term that uses getElem you'd see the version with the proof term in it, if that makes sense. Lean wouldn't hide the underlying proof terms from you as it does with well-founded recursion

[James Gallicchio]

I guess in the case of well-founded recursion you _can_ still end up seeing the underlying representation, but my impression is that something is wrong if you're seeing it

[Sebastian Ullrich]

We do in fact hide the proof in the getElem unexpander. And even if you disable pp.notation, you'll still only see _ for the proof because of pp.proofs. But at that level the output will be the same regardless of which syntactic approach we choose anyway.

[Mario Carneiro]

Would it be possible / too magic to have a[i] look for an assumption in the context possibly supplied by have and otherwise fall back on the normal getOp? That would make for some really slick code for stuff like if h : x < a.size then a[i] else 37

[Mario Carneiro]

The choice of ' as separator is not particularly consonant with other syntax in lean, but I don't have any better suggestions

[Gabriel Ebner]

Not sure if you've been following this thread, but that's exactly what it does now (except for the falling back part).

[Henrik Böving]

It uses this custom extensible tactic which among others calls to assumption so it can do this

[Mario Carneiro]

oops, I guess the new one is a[i]! now

[Mario Carneiro]

what's the current state of the fin version?

[Tomas Skrivan]

It is done through a typeclass, so you can write a[i] for i : Nat and fetch proof from context but you can also write a[i] for i : Fin a.size.

[Mario Carneiro]

Ah, just read the release notes which clarify the situation somewhat. The get_elem_tactic tactic doesn't seem to have any access to information about what array or index is being proved?

[Tomas Skrivan]

Oh a[i] for i : Fin a.size works because of coercion of Fin a.size to Nat instead of specialized instance of GetElem.

[Henrik Böving]

Mario Carneiro said:

Ah, just read the release notes which clarify the situation somewhat. The get_elem_tactic tactic doesn't seem to have any access to information about what array or index is being proved?

I guess you could extend it with a type aware tactic that fails per default if there isn't the types it expects around though right?

[Mario Carneiro]

I mean, you can implement it as assumption which is presumably the intent, but I don't see what kind of extra smarts you could give it

[Tomas Skrivan]

Do we also want to unify notation a[i] := x and a[i] += x?

Following identical pattern I have defined two classes SetElem and ModifyElem

import Lean

class SetElem (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) (Dom : outParam (Cont → Idx → Prop)) where
  setElem (xs : Cont) (i : Idx) (x : Elem) (h : Dom xs i) : Cont

export SetElem (setElem)

class ModifyElem (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) (Dom : outParam (Cont → Idx → Prop)) where
  modifyElem (xs : Cont) (i : Idx) (f : Elem → Elem) (h : Dom xs i) : Cont

export ModifyElem (modifyElem)

syntax (priority := high) atomic(Lean.Parser.Term.ident) noWs "[" term "]" " := " term : doElem
syntax atomic(Lean.Parser.Term.ident) noWs "[" term "]" " += " term : doElem

macro_rules
| `(doElem| $x:ident[ $i:term ] := $xi) => `(doElem| $x:ident := setElem $x $i $xi (by get_elem_tactic))
macro_rules
| `(doElem| $x:ident[ $i:term ] += $xi) => `(doElem| $x:ident := modifyElem $x $i (λ val => val + $xi) (by get_elem_tactic))

instance : SetElem (Array α) Nat α (λ xs i => i < xs.size) where
  setElem xs i x h := xs.set ⟨i,h⟩ x

instance : ModifyElem (Array α) Nat α (λ xs i => i < xs.size) where
  modifyElem xs i f _ := xs.modify i f

#eval Id.run do
  let mut a := List.toArray [5,10]
  a[0] := 42
  a[1] += 6
  a -- returns #[42, 16]

[Mario Carneiro]

Didn't @Gabriel Ebner have some implementation of general lvalues? How hard is it to incorporate arrays in that?

[Gabriel Ebner]

https://github.com/leanprover/lean4/issues/905#issuecomment-1165768170 And it supports array updates (at least with the syntax from yesterday).

[Tomas Skrivan]

That looks really nice!

[Leonardo de Moura]

Gabriel Ebner said:

Not sure if you've been following this thread, but that's exactly what it does now (except for the falling back part).

I expanded the release notes https://github.com/leanprover/lean4/commit/351fc6ea04ea5aa5763d2981826acafa2ec2a617

[Leonardo de Moura]

Mario Carneiro said:

what's the current state of the fin version?

I covered the Fin case in the commit above.

[Mario Carneiro]

typo: get_tactic_tactic in the release notes

[Joe Hendrix]

I really like @Sebastian Ullrich's proposal of having a syntax to define well-formed checks after the rest of the definition. ACL2 and PVS both allow one to defer side condition checks like this and that might be partly born out of necessity, but I think it avoids having proofs of these sort of safety side-conditions clutter up the program.