Zulip Chat Archive

Stream: general

Topic: Functional data structures


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Rob Lewis (Jan 18 2021 at 17:35):

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

view this post on Zulip 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