Implication of adding typeclass bounds on structures

Stream: general

[cmlsharp]

What are the implications of writing instance bounds on structures e.g.

structure BinaryHeap (α: Type w) where
  arr : Array α

structure BinaryHeap (α: Type w) [Ord α] where
  arr : Array α

From my Rust background, my default is to opt for the former as it seems strictly more flexible, and it allows you to write some methods (such as empty) without supplying an instance at all. However, I notice that e.g. in the standard library HashTable has class bounds for BEq and Hashable in the structure definition. Is there a reason to prefer the latter over the former?

[cmlsharp]

Ah, I guess this is a difference. Without Ord in the type signature the following compiles

  example  :=
    let heap : BinaryHeap Nat := .empty
    letI := instOrdNat.opposite
    heap.insert 1

while with it, it doesn't.

[Edward van de Meent]

your example doesn't seem to compile either way?

[François G. Dorais]

There's a third option:

structure BinaryHeap (α : Type w) extends Ord α where
  arr : Array α

Please make a mwe to illustrate.

[cmlsharp]

Here is a mwe

[François G. Dorais]

Try the third option.

[cmlsharp]

The third option requires that 'empty' have an Ord constraint, but permits the example above. Here's the MWE with this version also

edit: sorry I was wrong, it does not require that empty have an ord constraint

[Robin Arnez]

It requires it for the implementation

[François G. Dorais]

But that's expected.

[cmlsharp]

Ah you're right, that makes sense. If I actually give a non sorry definition for the rhs of empty, then it gives an error if there is no Ord instance

[François G. Dorais]

Do you expect empty to work without an Ord instance?

[cmlsharp]

I think it's fine if it does (but like I said I'm coming from Rust where the idiomatic thing is usually to put the minimum trait bounds required to make the implementation works). That said, Rust does not allow multiple trait implementations for the same type, so in light of that I think it makes sense to put the [Ord a] bound on the structure definition

edit: just so I don't seem crazy, for example HashMap::new works for any key and value types, regardless of whether the key is hashable or not

[Robin Arnez]

I think the third option is something done more often in other programming languages (for example Java uses this principle for TreeMaps) where the empty map constructor requires a comparator but the other operations don't. But I don't think it fits well for Lean, in particular since it's very awkward to use this Ord instance, you'd need something like heap.toOrd.compare a b or let := heap.toOrd instead of just compare a b.
The second option is the safest because it ensures that you don't do any operations like insert with a different instance (in the sense of = since you can still cast).
The first option is most flexible but also loses wellformedness guarantees pretty quickly (and note that it is also not possible to embed a wellformedness invariant into the structure definition because of the lack of instance). Use this one if you don't care about wellformedness.
In Lean, the first option is docs#Std.HashMap.Raw and all other similar variants and the second option is docs#Std.HashMap and all other variants.
Also, as you said docs#Std.HashMap.Raw.instEmptyCollection has no hashable constraints:

import Std

#check ({} : Std.HashMap.Raw Prop Nat)

[cmlsharp]

Does this also have implications for runtime performance? I assume option 3 requires storing the actual comparator function at runtime. Does that have implications for inlining, etc?

[cmlsharp]

Regarding well-formedness, this comes up in a PR I have open in Batteries which adds formal verification to the BinaryHeap implementation. My current approach has been to just add extrinsic lemmas that verify the well-formedness properties (i.e. the well-formedness property is not bundled with the binary heap). I suppose one could imagine having a similar Raw dichotomy as in HashMap. What is the reasoning for having a "bundled" version as opposed to just a raw implementation and lemmas that prove the wellformedness property is preserved?

[Robin Arnez]

cmlsharp schrieb:

Does this also have implications for runtime performance?

Option 3 has performance implications by requiring more memory and the use of closure calls, option 1 and option 2 are identical in terms of performance.

[Robin Arnez]

cmlsharp schrieb:

What is the reasoning for having a "bundled" version as opposed to just a raw implementation

The proofs for the raw version require an additional wellformedness hypothesis while the bundled version has simpler lemmas that don't require such additional assumptions. Also, having a wellformedness guarantee can sometimes allow for faster paths (e.g. Std.TreeMap makes heavy use of balancing invariants to eliminate impossible cases in matches)

[Robin Arnez]

So actually, I take it back, option 2 + wellformedness can also have performance benefits over option 1

[cmlsharp]

Ah, I see, the non-raw version is easier to work with in proofs because you don't have to manually thread through the well-formedness condition. That makes sense. @François G. Dorais , do you have a thought about whether Batteries ought to have a similar raw/bundled dichotomy for BinaryHeap?

[François G. Dorais]

I think we've come full circle why the original implementation used an lt parameter instead of an Ord instance. Your verification work is excellent and I would not recommend moving back to lt. Using Ord should be just as efficient but there needs to be some library and compiler work upstream to make it work efficiently. This is a long term goal. In the shorter term, there are thoughts about reimplementing structures in core that could make option 3 behave mostly like option 1 but with the major benefits of option 2.

In any case, whatever you pick right now could be updated to a better option later so long as you don't commit too much to implementation details.

PS: Note that many Ord implementations are very inefficient. Most require two or three comparisons that could be optimized to just one. A good backend could optimize these out but we can't rely on that.

[cmlsharp]

Ok, I think the implementation I will go with for the moment is option 2.

Fwiw, I wrote a quick benchmarking script to test an 'lt function' an Ord instance and an 'extends Ord' based heap, and timed heapSort on arrays (of Nats) of increasing size. (times are the median of 20 trials, with a 5 trial warmup). [Ord Nat] and lt seem to be pretty comparable, but extends Ord is definitely slower.

=== Array size: 10000 ===
Name                 Time
-------------------  ---------------
Heap1 (lt function)  62.030611 ms
Heap2 ([Ord α])      64.925203 ms
Heap3 (extends Ord)  178.244899 ms

=== Array size: 100000 ===
Name                 Time
-------------------  ---------------
Heap1 (lt function)  802.539662 ms
Heap2 ([Ord α])      826.494604 ms
Heap3 (extends Ord)  1288.743552 ms

(edit: also with larger numbers of trials this difference between lt and [Ord \a] shrinks)