Functional data structures

Stream: general

[Jannis Limperg]

I'm supervising a couple of undergraduates who would like to implement, and in some cases verify, some functional data structures in Lean (3 or 4). Are there any data structures that you'd particularly like to see implemented? In Lean 3, we currently have red-black trees and nothing else afaik (linked lists don't count); Lean 4 also has binomial heaps.

[Yakov Pechersky]

Seq from Data.Sequence in Haskell;
tries; suffix trees -- although getting good functional implementations of those is not that straightforward

[Rob Lewis]

See also https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/BSc.20Final.20Project

[Jannis Limperg]

Thanks! Finger trees (Seq) might be interesting, though Lean 4 also has some sort of persistent array which is probably more performant in practice. Tries would certainly be nice.