3
$\begingroup$

Are there builtin dictionary/map types in Lean 4 prover?

I'd like to use dictionaries in my program and prove properties about it, but I am not sure if there is a dictionary type in Lean 4. A similar question in SO was about whether there is a dictionary type in Idris 2. The answer was there there is no builtin type and one is provided in the contrib called Data.SortedMap. As the linked question pointed out, dictionary is a basic data structure (so commonly used that languages like lua depend on it.)

Upon closer look, there is not much support for proofs in Idris's Data.SortedMap. For example, the only lookup function returns a Maybe value. There seems to be no way to provide a proof that the lookup key is inBounds and get a value of the original type. The constructor type M : SortedDMap k (const v) -> SortedMap k v is also a bit mysterious to a newcomer like me. Hence the question here.

A more general question is,

is it generally more difficult to construct a dictionary type in proof languages via algebraic data types and constructors like List's and their nil and cons? (and what are the difficulties?)

$\endgroup$
1
  • $\begingroup$ What is the definition of "dictionary" you are using? Is List (Key * Value) a valid dictionary type? $\endgroup$
    – Trebor
    Sep 17, 2023 at 0:35

1 Answer 1

4
$\begingroup$

Lean has both functional (persistent) key-value data structures like Std.RBMap which are easy to use in a functional programming context as well as more standard structures like Std.HashMap, but for the later it is important (if performance matters) to update the map without making a copy so you don’t accidentally duplicate the underlying data structure every time you change it.

If performance doesn’t matter then Std.AssocList (which is basically just List (Key x Value)) is a simple and easy to use option.

More generally, to answer your second questions, there is an art to persistent data structures in functional languages. They basically work by using tree and list like objects underneath at the cost of a slower (usually just a large constant) runtime. See Purely functional data structures or the book by the same name.

As for the standard hashmaps, that is supported by Lean 4 since Lean 4 has destructive updates, where if you still only have one reference to an object after updating it then it changes it in place. So you can work with constant time access arrays directly just like in any standard programming language. See the paper Counting immutable beans.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.