Topic: Functional data structures
Jannis Limperg (Jan 18 2021 at 17:19):
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 (Jan 18 2021 at 17:23):
Data.Sequence in Haskell;
tries; suffix trees -- although getting good functional implementations of those is not that straightforward
Rob Lewis (Jan 18 2021 at 17:35):
Jannis Limperg (Jan 18 2021 at 18:29):
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.
Last updated: May 16 2021 at 21:11 UTC