Making Shrink computable

Stream: general

[William Sørensen]

I am unsure if this is the right place to post but I'm quite stuck. I'm trying to add a computable version of Shrink, to do this i am trying to use the FFI feature of lean. I have been trying for the past few days to get this to work but either I segfault when I use external_class, or I get unexpected results when i use anything else.

In redefining Shrink i try to do it like this:

private opaque ShrinkImpl (a : Type b) [inst : Small.{b, s} a] : Type s

/- @[pp_with_univ] -/
@[implemented_by ShrinkImpl]
def Shrink (a : Type b) [inst : Small.{b, s} a] : Type s :=
  Classical.choose inst.equiv_small

@[extern "shrink_mk"]
private opaque mkImpl {α} [Inhabited α] [Small.{b, s} α] : α → Shrink α

@[extern "shrink_dest"]
private opaque destImpl {α} [Inhabited α] [Small.{b, s} α] : Shrink α → α

@[implemented_by mkImpl]
def mk [Inhabited α] [Small.{b, s} α] : α → Shrink α :=
  (equivShrink α).toFun

@[implemented_by destImpl]
def dest [Inhabited α] [Small.{b, s} α] : Shrink α → α :=
  (equivShrink α).invFun

and the simplest C++ that doesnt lead to a segfault is just returning the object like this:

extern "C" lean_object *shrink_mk(lean_object *inhabited, lean_object *small,
                                  lean_object *obj) {
  return obj;
}
extern "C" lean_object *shrink_dest(lean_object *inhabited, lean_object *small,
                                    lean_object *shrink) {
  return shrink;
}

This leads to very strange behaviour:

def main : IO Unit := do
  let obj : Shrink Nat := Shrink.mk 999

  IO.println obj.dest -- Prints 0?

If this is the wrong place to post please feel free to point me where to go.

[Robin Arnez]

export is overkill, just:

private unsafe def equivShrinkImpl.{w, v} (α : Type v) [Small.{w, v} α] : α ≃ Shrink.{w, v} α := ⟨unsafeCast, unsafeCast, lcProof, lcProof⟩
@[csimp] private unsafe def equivShrink_eq_equivShrinkImpl : @equivShrink = @equivShrinkImpl := lcProof

and then you can define the rest without implemented_by or anything (also why the indirection of extern + implemented_by? you can just do extern on the def. not sure what's wrong with the extern thing)

[Eric Wieser]

I suspect you're in trouble here because docs#Shrink is in Prop and so erased at compile-time?

[Aaron Liu]

It's not???

[Eric Wieser]

Ah sorry, I was confusing it with docs#Small

[Eric Wieser]

Presumably we could also use

class Small (α : Type v) where
  equiv_small : Squash <| (S : Type w) × (α ≃ S)

to get some form of computability for free

[Edward van de Meent]

the only computability you'd get for free is data which is (provably) the same up to choice of permutation, which is probably not a lot...

[Paul Reichert]

I agree this would be useful, I've also naturally wished for that while working on the iterator library. Unfortunately, it seems to me that one currently needs to choose two of (a) get computable Shrink, (b) keep Small in Prop` and (c) do not use unsafe...

[Eric Wieser]

Why does the iterator library need Small?

[Paul Reichert]

The iterators return a value of type m (IterStep α β), where α is the internal state type and β is the type of the emitted values. If α and β live in distinct universes, then IterStep α β lives in their max, so the monad needs to live in max. This made the API quite fragile to use. Shrink would allow us to compress the state as needed.

Therefore, α and β are currently forced to live in the same universe. But there are some situations where it's desirable to have them live in different ones (the existing Stream data type is also universe-heterogeneous, but it isn't monadic, so it avoids most of the problems).

[William Sørensen]

Robin Arnez said:

export is overkill, just:

private unsafe def equivShrinkImpl.{w, v} (α : Type v) [Small.{w, v} α] : α ≃ Shrink.{w, v} α := ⟨unsafeCast, unsafeCast, lcProof, lcProof⟩
@[csimp] private unsafe def equivShrink_eq_equivShrinkImpl : @equivShrink = @equivShrinkImpl := lcProof

and then you can define the rest without implemented_by or anything (also why the indirection of extern + implemented_by? you can just do extern on the def. not sure what's wrong with the extern thing)

Wouldn’t I need to mark mk and dest both as noncomputable? Wouldn’t this carry up?

[William Sørensen]

Ok I’ll try these things tomorrow at least but we’ll see

[Robin Arnez]

William Sørensen schrieb:

Wouldn’t I need to mark mk and dest both as noncomputable?

No, we already provided an implementation of equivShrink so it will use that then.

[Robin Arnez]

Oh and it would probably be reasonable to mark equivShrinkImpl as @[inline]

[William Sørensen]

@Robin Arnez thanks for the help here, yeah your answer is perfect.

[Tristan Figueroa-Reid]

Is the code for equivShrinkImpl somewhere accessible?

[Violeta Hernández]

If we're actually going to do this, can we keep the prop-valued Small? There would be very major breakage in e.g. the entirety of the combinatorial game library otherwise, since we'd have to deal with such annoying stuff such as showing that two different witnesses of Small construct the same game.

[Violeta Hernández]

Eric Wieser said:

Presumably we could also use

class Small (α : Type v) where
  equiv_small : Squash <| (S : Type w) × (α ≃ S)

to get some form of computability for free

This would still be a bit annoying since x y : Squash α are propeq and not defeq. Otherwise I agree this is the best solution.

[William Sørensen]

I found that @Robin Arnez's idea of just making the equiv unsafe worked wonders, I just need to check if it is correct

[William Sørensen]

Making small reside in type goes against the point as then it must reside in a high universe

[Violeta Hernández]

What's the problem with that? Small would have a "high" universe but the equivalent type would still have the correct one.

[Violeta Hernández]

I think another solution might be to make a separate Small' (name pending) typeclass for the data-valued version, and prove Small' implies Small.

[Eric Wieser]

Violeta Hernández said:

This would still be a bit annoying since x y : Squash α are propeq and not defeq. Otherwise I agree this is the best solution.

Isn't this the same story as Fintype and Decidable?

[Violeta Hernández]

Well, with Fintype, we eventually ended up making Finite.

[Violeta Hernández]

Decidable can also be basically ignored if you're doing proofs and assuming choice

[Eric Wieser]

Yes, your Small' message came in as I was typing :)

[Aaron Liu]

Eric Wieser said:

Isn't this the same story as Fintype and Decidable?

yes but also no

[Eric Wieser]

Having reread the thread I now understand that the unsafe idea is reasonable here

[William Sørensen]

Violeta Hernández said:

What's the problem with that? Small would have a "high" universe but the equivalent type would still have the correct one.

I can try to have a look into if this is fine but i think i found i needed it to be small to work with the fixed point system i was using, i am unsure though

[William Sørensen]

Eric Wieser said:

Having reread the thread I now understand that the unsafe idea is reasonable here

Yeah it really worked wonders for me, was super useful and I belive it is sound, I dont know how to reason that it is though...

[Eric Wieser]

With your example above, I don't understand why you need the Inhabited vs using

@[extern "shrink_mk"]
def mk [Small.{s} α] : α → Shrink α :=
  (equivShrink α).toFun

[Eric Wieser]

Nevermind, I guess Robin's suggestion replaces this. Can you share your working version?

[William Sørensen]

Heres a link to the repo i made with it https://github.com/Equilibris/Shrink/blob/main/Shrink/Basic.lean

[William Sørensen]

This worked fine

[Aaron Liu]

you probably want equivShrinkImpl to be always inline or something

[William Sørensen]

I've made a pr for this now. If people want to add some comments to it before I post it in #PR reviews then feel free. Maybe especially you at @Robin Arnez as it's your implementation and I included you in the comment if you want to be there or not. Additionally I ended up using implemented_by over your csimp approach, I dont quite know whats best there