Computable `equivShrink`?

Stream: lean4

[Markus Schmaus]

Could docs#equivShrink be made computable? And by that I mean in the same sense as docs#Quot.mk is computable, which in my understanding doesn't change anything about the object and it's implementation, it just moves it to the other type.

I don't think it would have any implications on the soundness of Lean, as equivShrink can already be used inside proofs. Could this be done without compiler support inside a library? Or would this require changes to core?

For background, I've been looking into types which are semantically equal to existing types, but have different performance characteristics. As a small, but useful, example consider that I want to map an Array, I could use docs#Array.map, but this immediately destroys the original array or creates a full copy. But maybe, I only want to evaluate this computation for a couple of indices, in which case it would be useful to postpone computation until access. I've come up with an implementation which I quote at the end of this post.

The resulting type MappedArrayLarge is of Type 1, I can show this type 0-small, but this doesn't seem to be of much use if I want to use elements of this type in computations. I don't want to use the equivalence I used in the proof, since this would evaluate the computation eviscerating the reason why I constructed this type in the first place. The reason I want MappedArray, rather than MappedArrayImp, is that the former can be turned into a functor with all the benefits of this for reasoning about the code.

Alternatively if someone know a way to get the same performance characteristics from a Type 0, without making equivShrink computable, that would be amazing.

import Mathlib.Tactic

universe u v

def exampleArray : Array Nat := #[0, 1, 2, 3, 4, 5]

structure MappedArrayImp (α : Type) where
  β : Type
  data : Array β
  mapping : β → α

namespace MappedArrayImp

abbrev size (self : MappedArrayImp α) : Nat :=
  self.data.size

abbrev get (self : MappedArrayImp α) (i : Fin self.size) : α :=
  self.mapping (self.data.get i)

abbrev fromArray {α : Type} (data : Array α) : MappedArrayImp α :=
  { β := α, data := data, mapping := id }

instance coeArray {α : Type} : Coe (Array α) (MappedArrayImp α) := ⟨fromArray⟩

#eval (exampleArray : MappedArrayImp Nat).get ⟨2, by decide⟩ -- 2

abbrev toArray {α : Type} (a : MappedArrayImp α) : Array α :=
  Array.ofFn a.get

instance setoid (α : Type): Setoid (MappedArrayImp α) where
  r x y := x.size = y.size ∧
    ∀ i, (hx : i < x.size) → (hy : i < y.size) → x.get ⟨i, hx⟩ = y.get ⟨i, hy⟩
  iseqv := by
    constructor
    all_goals simp_all only [forall_true_left, implies_true, forall_const, and_self, and_imp]

end MappedArrayImp

abbrev MappedArrayLarge (α : Type) := Quotient (MappedArrayImp.setoid α)

#check MappedArrayLarge Nat -- Type 1

namespace MappedArrayLarge

abbrev size {α : Type} : (MappedArrayLarge α) → Nat := Quotient.lift MappedArrayImp.size <| by
  simp only [HasEquiv.Equiv, Setoid.r, and_imp]
  omega

abbrev get {α : Type} (a : MappedArrayLarge α) : (Fin a.size) → α :=
    Quotient.hrecOn a MappedArrayImp.get <| by
  simp only [HasEquiv.Equiv, Setoid.r]
  intro a b ⟨size_eq, h⟩
  exact (Fin.heq_fun_iff size_eq).mpr fun i => h (↑i) i.isLt (size_eq ▸ i.isLt)

abbrev fromArray {α : Type} (data : Array α) : MappedArrayLarge α :=
  ⟦MappedArrayImp.fromArray data⟧

instance coeArray {α : Type} : Coe (Array α) (MappedArrayLarge α) := ⟨fromArray⟩

#eval (exampleArray : MappedArrayLarge Nat).get ⟨2, by decide⟩ -- 2

abbrev toArray {α : Type} : MappedArrayLarge α → Array α :=
    Quotient.lift MappedArrayImp.toArray <| by
  simp only [HasEquiv.Equiv, Setoid.r, Array.data_length, MappedArrayImp.get, Array.get_eq_getElem,
    MappedArrayImp.toArray, and_imp]
  intro a b size_eq h
  apply Array.ext
  · simp_all only [Array.size_ofFn]
  · aesop

def arrayEquiv {α : Type} : MappedArrayLarge α ≃ Array α where
  toFun := toArray
  invFun := fromArray
  left_inv := by
    intro a
    have ⟨a', a_def⟩ := Quotient.exists_rep a
    subst a_def
    simp only [fromArray, MappedArrayImp.fromArray, toArray, Quotient.lift_mk,
      MappedArrayImp.toArray, Array.data_length, Quotient.eq, HasEquiv.Equiv, Setoid.r,
      Array.size_ofFn, MappedArrayImp.get, Array.get_eq_getElem, Array.getElem_ofFn, id_eq,
      implies_true, forall_const, and_self]
  right_inv := by
    intro a
    apply Array.ext
    · simp only [toArray, fromArray, MappedArrayImp.fromArray, Quotient.lift_mk,
        MappedArrayImp.toArray, Array.data_length, Array.size_ofFn]
    · simp only [toArray, fromArray, MappedArrayImp.fromArray, Quotient.lift_mk,
        MappedArrayImp.toArray, Array.data_length, Array.size_ofFn, Array.getElem_ofFn,
        MappedArrayImp.get, Array.get_eq_getElem, id_eq, implies_true, forall_const]

instance small (α : Type) : Small.{0} (MappedArrayLarge α) where
  equiv_small := by
    use Array α
    constructor
    exact arrayEquiv

end MappedArrayLarge

def MappedArray (α : Type) := Shrink (MappedArrayLarge α)

#check MappedArray Nat -- Type 0

[Mario Carneiro]

What are you trying to accomplish with this MappedArray?

[Mario Carneiro]

You can probably do most of what you want (that is, the #xy problem, not equivShrink itself) by exposing β as a parameter of MappedArray

[Markus Schmaus]

The question is how far down the xy problem do you want to go? My ultimate goal is that I want to be able to quickly write reliable code with good enough performance to solve my practical needs.

I find that lawful monads are a good way to reason about code and show that it does what it is supposed to do, I've done so informally in the past, and I am excited that this can be done formally with Lean. Lean's List monad provides the semantics I want, but I know from prior experience (mostly with other programming languages), that the performance of linked lists isn't good enough for the kind of programs I want to write. The solution I've used in the past was to use arrays at the bottom, with delayed computation stacked on top, which get evaluated and cached at the appropriate times. Semantically that's equivalent to List, just like Array is semantically equivalent to List, and therefore it's a lawful monad. I can implement this in Lean (at least I am making good progress). I can even tell Lean about the monad semantics, by creating a LawfulMonad instance, which I can use to formally reason about my code. The only downside is that so far this monad is Type u → Type u + 1.

I'm eager to talk about all the xs and ys of this project I'm working on, with anybody who's interested, but many of my ideas are still pretty intuitive, and I'm still in the process of formalizing this in Lean code, So in order to keep this question somewhat manageable I'm asking if it's possible to make quivShrink computable?

[Junyan Xu]

I've thought about making Small a data-carrying class (or making a data-carrying version of Small), and I am in favor of it if it doesn't lead to serious diamonds. The reason is that in category theory etc. most use cases are saying something like ULift.{u} X is Small.{v} if X : Type v, in which case we have the canonical equivalence docs#Equiv.ulift and it would be preferable to use it rather than an arbitrarily chosen one.

[Junyan Xu]

There is indeed some diamond issue though; both of the following rfl fail.

import Mathlib
universe u v w
example (α : Type u) : ULift.{v} (ULift.{w} α) = ULift.{max v w} α := rfl /- fails -/
example (α : Type u) : ULift.{v} (ULift.{w} α) = ULift.{w} (ULift.{v} α) := rfl /- fails -/

[Markus Schmaus]

I believe you mean a data-carrying Shrink, as Small can already carry data, if I provide a computable equiv_small into a data-carrying type. I think the diamonds you are worried about would only occur if there is a Small instance for Shrink, but this could already be defined to day, so I don't see how making Shrink data-carrying changes this. Even if Shrink is data-carrying I don't think it would ever be a good choice for the canonical model in a Small instance, as it wouldn't be useful to reason about the type in the higher universe, the model from the Small which is used for the Shrink would even be useful to reason about the Shrink type.

[Floris van Doorn]

class Small (α : Type v) : Prop
It would have to be : Type _ instead of Prop to carry data.

[Floris van Doorn]

But making it data-carrying might cause diamonds (though Junyan's example is not an example of diamonds, I think, since the fact that the types are different, it means that there is not a risk of that being a diamond).

If all instances of Small are type-directed (e.g., F X Y is small whenever X and Y are small), then I don't think there is a risk of diamonds.

[James Gallicchio]

@Markus Schmaus you might be interested in some stuff I've been doing here. Maybe relevant things:

• experimental interface for indexed types like array
• foldable Views into data that allow for inlining data pipelines
• Slices into indexed types

[James Gallicchio]

the terminology used in this library is very unintuitive and derived from many sources, and there's very little documentation, but I am happy to help if this library will be useful to you

[James Gallicchio]

(also, the library's whole goal is to be more amenable to proof, but that is very much work-in-progress...)

[Markus Schmaus]

@James Gallicchio I had a look at your library and it looks interesting.

[Markus Schmaus]

I totally misremembered the definition of Small, but that also means, that making it carry data wouldn't help my use case, as this wouldn't help with making equivShrink computable.

[Junyan Xu]

What's wrong with

import Mathlib

universe w v u
variable (α : Type v)

@[pp_with_univ] class Small' where
  Shrink : Type w
  equivShrink : α ≃ Shrink

#check Small'.equivShrink
/- Small'.equivShrink.{w, v} {α : Type v} [self : Small' α] : α ≃ Small'.Shrink α -/

This Small'.equivShrink is computable. I'm simply replacing the existential with essentially a Sigma type.

Floris van Doorn said:

But making it data-carrying might cause diamonds (though Junyan's example is not an example of diamonds, I think, since the fact that the types are different, it means that there is not a risk of that being a diamond).

If all instances of Small are type-directed (e.g., F X Y is small whenever X and Y are small), then I don't think there is a risk of diamonds.

Yeah sorry I was confused, and I misremembered what my concern was. There won't be non-defeq synthesized Small.{v} (ULift X) instances for X : Type v, but the actual use case isn't this, instead it's about using Small to define UnivLE, and the actual diamond is the following (continued from above):

instance : Small'.{v} α := ⟨α, .refl α⟩

instance : Small'.{v} (ULift.{w} α) := ⟨α, .ulift⟩

@[pp_with_univ] abbrev UnivLE' := ∀ α : Type w, Small'.{v} α

example : UnivLE'.{w, w} := inferInstance

-- Analog of `univLE_of_max`, key instance for UnivLE to work
-- priority := low so that `#synth UnivLE'.{w,w}` gets the `.refl` instance
instance (priority := low) univLE'OfMax [UnivLE'.{max w v, w}] : UnivLE'.{v, w} :=
  fun α ↦ ⟨Small'.Shrink (ULift.{w} α), .trans (.symm .ulift) Small'.equivShrink⟩

#synth UnivLE'.{w, w} /- fun α => instSmall' α -/
#synth UnivLE'.{w, max w v} -- succeeds
example [UnivLE'.{max w v, w}] : UnivLE'.{v, w} := inferInstance -- succeeds

def Small'.trans_univLE' (α : Type u) [Small'.{w} α] [UnivLE'.{w, v}] : Small'.{v} α :=
  ⟨Small'.Shrink (Small'.Shrink α), Small'.equivShrink.{w}.trans Small'.equivShrink⟩

def univLE'Trans [UnivLE'.{w, v}] [UnivLE'.{v, u}] : UnivLE'.{w, u} :=
  fun α ↦ Small'.trans_univLE' α

example : univLE'Trans.{w, max w v, max w v u} = by infer_instance := rfl -- fails

This means that even though UnivLE' enjoys transitivity, it's undesirable to use univLE'trans to construct instances.

[Mario Carneiro]

Making Small data carrying won't solve @Markus Schmaus 's problem at all, because it will just end up being a convoluted way of defining def MappedArray (α : Type) := Array α. There is also the question of how you expect to have any operations on this type - the only method provided to you by the Shrink infrastructure is to use the equiv you are given, but this amounts to eagerly computing the map result, which defeats the point.