Zulip Chat Archive

Stream: general

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):

Seq from 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):

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

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: Dec 20 2023 at 11:08 UTC