## Stream: new members

### Topic: 23trees

#### Edward Ayers (Aug 09 2018 at 23:14):

Dear all, I am writing a tactic and I want to keep a set of things in a datastructure for quick access. In other languages you would use a 23tree or similar. Is there something like this in the Lean library? Otherwise I am fine just keeping a list of objects and removing the dupes but I thought I'd check if the datastructure is in there.

#### Simon Hudon (Aug 09 2018 at 23:17):

Yes there's the rbmap which should be available without imports

#### Edward Ayers (Aug 09 2018 at 23:17):

perhaps I can just use set and lean will magically figure it out?

#### Simon Hudon (Aug 09 2018 at 23:18):

perhaps I can just use set and lean will magically figure it out?

Unfortunately, not yet.

thanks

No problems :)

#### Edward Ayers (Aug 09 2018 at 23:20):

If I want to write my own helper methods for list, is it correct to write in the form def list.myextension ...?

#### Simon Hudon (Aug 09 2018 at 23:26):

Yes, sure. You can also put it in namespace list ... end list so that, inside the namespace, you don't have to specify list. everywhere but outside, you can still use my_list.myextension to call it with argument my_list

#### Edward Ayers (Aug 09 2018 at 23:41):

Is there a better way of listing all of the local constants which appear in an expr other than recursion over expr?

#### Simon Hudon (Aug 09 2018 at 23:43):

you can use expr.fold.

#### Simon Hudon (Aug 09 2018 at 23:45):

But if you use mathlib, you can import meta.exprand use expr.list_local_const

fab

#### Edward Ayers (Aug 09 2018 at 23:57):

What is the difference between import and open?

#### Simon Hudon (Aug 09 2018 at 23:58):

import is about modules i.e. source files and open is about namespaces which can span multiple files.

#### Edward Ayers (Aug 10 2018 at 00:00):

if I import a source file, is that effectively the same as pasting it above my code?

#### Simon Hudon (Aug 10 2018 at 00:02):

You could say that. But it's a smart paste: it does not paste the same module more than once.

#### Mario Carneiro (Aug 10 2018 at 01:54):

perhaps I can just use set and lean will magically figure it out?

Is that a thing people want? It is conceivable that we could associate data to a typeclass on set, basically the same as fintype s currently but with a tree-like data structure. Currently you have to use explicit data structures like rbmap or hash_map or finmap

#### Simon Hudon (Aug 10 2018 at 01:59):

What would the type class be applied to? The element type?

the set

#### Simon Hudon (Aug 10 2018 at 02:10):

I'm not eager to go down that rabbit hole. In Haskell, a similar situation has created multiple types for strings and multiple solutions to simplify the situation once and for all with unclear consequences.

#### Mario Carneiro (Aug 10 2018 at 02:11):

in some ways it seems appealing, similar to decidability of a prop, you have representability of a set

#### Mario Carneiro (Aug 10 2018 at 02:12):

but it's probably not good if the typeclass is not a subsingleton, meaning you have to hide a lot of structure

#### Simon Hudon (Aug 10 2018 at 02:12):

Yeah but with prop and decidability, the representation is unique.

#### Mario Carneiro (Aug 10 2018 at 02:13):

you can always perform a suitable quotient to make it a subsingleton

#### Mario Carneiro (Aug 10 2018 at 02:14):

but you need more than decidable_eq if you want to have any representation better than an association list (which you already get with fintype s)

#### Simon Hudon (Aug 10 2018 at 02:14):

That creates another mess: if you take two sets as parameters, you have to anticipate that they have vastly different representations.

#### Mario Carneiro (Aug 10 2018 at 02:15):

what do you mean? If it is a binary tree structure the only representation ambiguity is wrt tree rotations

#### Simon Hudon (Aug 10 2018 at 02:16):

No I mean if you have a function that takes two sets as a parameter, one might be a binary search tree, the other may be represented as an assoc list (if I understand your quotient idea properly). That makes taking their union needlessly complicated.

#### Mario Carneiro (Aug 10 2018 at 02:16):

oh, no I wasn't thinking that

#### Mario Carneiro (Aug 10 2018 at 02:17):

if you have two data structures which are both applicable here you have two typeclasses

#### Mario Carneiro (Aug 10 2018 at 02:17):

I'm not even sure how to implement type ambiguity of that kind

#### Simon Hudon (Aug 10 2018 at 02:18):

Actually, I think existential types would be the best way to go. But I don't advise trying it at home.

#### Mario Carneiro (Aug 10 2018 at 02:18):

existential types don't really work in lean though

#### Mario Carneiro (Aug 10 2018 at 02:18):

because of predicativity

#### Simon Hudon (Aug 10 2018 at 02:19):

Really? But if you have structure where one of the field is a type and the next is a type class assumption, doesn't that work?

#### Mario Carneiro (Aug 10 2018 at 02:19):

It's possible but it will live in a higher universe

#### Simon Hudon (Aug 10 2018 at 02:20):

Yeah, it is annoying to say the least

#### Mario Carneiro (Aug 10 2018 at 02:20):

I guess it might work if it acts a bit like monad or traversable-type typeclasses

#### Simon Hudon (Aug 10 2018 at 02:20):

What kind of type classes do you have in mind? Do they including operations like union, intersection, empty set?

#### Mario Carneiro (Aug 10 2018 at 02:21):

At the very least

#### Mario Carneiro (Aug 10 2018 at 02:21):

Indeed there probably isn't much else they can support

#### Simon Hudon (Aug 10 2018 at 02:21):

I found curious wrinkle about finset and traversable by the way but I think it's a different conversation.

#### Mario Carneiro (Aug 10 2018 at 02:22):

that sounds ominous

#### Mario Carneiro (Aug 10 2018 at 02:22):

I recall Johannes having difficulty defining the BNF instance for multiset because of quotients, I assume the issue is similar here

#### Simon Hudon (Aug 10 2018 at 02:23):

I think having that kind of type class would be useful but it should be a last resort of generalization. You should probably stick to concrete types of set representations in the type of your computable functions as much as possible.

#### Mario Carneiro (Aug 10 2018 at 02:24):

Does haskell have a typeclass for finite maps? Or is it just traversable

#### Simon Hudon (Aug 10 2018 at 02:25):

As for the wrinkle. I managed to make multiset sort-of traversable -- sort-of because in traverse (not its laws) I require the applicative to be lawful and commutative. In finset, I didn't manage to make it sort-of traversable because I would need seq to be idempotent. That's not a big wrinkle but our conversation reminded me of that.

#### Simon Hudon (Aug 10 2018 at 02:26):

Officially, it's mostly just traversable and the like. Some packages have classes for that but they aren't very useable and don't simplify much.

#### Simon Hudon (Aug 10 2018 at 02:27):

I think I just understood why you talked of monad and traversable. I think you're right. You might also need a lattice or a monoid

#### Mario Carneiro (Aug 10 2018 at 02:34):

Why does seq have to be idempotent? Seems like the finset traverse should just refer to multiset traverse

#### Simon Hudon (Aug 10 2018 at 02:35):

Because somewhere in the laws, you need to prove the equivalence between pruning duplicates before and after a traversal with pruning them only after.

#### Simon Hudon (Aug 10 2018 at 02:38):

That's for a lawful traversable instance. The traverse implementation itself works for finset

#### Mario Carneiro (Aug 10 2018 at 02:40):

I just noticed that there are five axioms in is_lawful_traversable. Are none of them redundant?

#### Simon Hudon (Aug 10 2018 at 02:40):

I suspect one might be but I haven't managed to prove it.

#### Simon Hudon (Aug 10 2018 at 02:41):

Two of them look really similar and it's odd that I can't prove one from the other.

#### Mario Carneiro (Aug 10 2018 at 02:43):

do you know any category theoretic treatment of traversable?

#### Simon Hudon (Aug 10 2018 at 02:44):

I know of a few papers that I still need to read. I don't know how far they go into category theory

#### Mario Carneiro (Aug 10 2018 at 02:47):

the map_traverse and traverse_map axioms aren't mentioned

#### Simon Hudon (Aug 10 2018 at 02:51):

That's right but the laws it does mention do not connect map and traverse. In the case of finset, the trouble comes from proving comp_traverse anyway.

#### Simon Hudon (Aug 10 2018 at 02:52):

(the map of t, not f)

#### Mario Carneiro (Aug 10 2018 at 02:58):

Lol @ "origami programming"

In the origami style of programming (Meijer et al. , 1991; Gibbons, 2002; Gibbons, 2003), the structure of programs is captured by higher-order recursion operators such as map, fold and unfold. [from http://www.cs.ox.ac.uk/jeremy.gibbons/publications/iterator.pdf ]

:laughing:

#### Simon Hudon (Aug 10 2018 at 02:59):

I guess you now know that bifunctor and bitraversable are coming

#### Simon Hudon (Aug 10 2018 at 03:00):

Also: monotraversable to use traversable-like techniques on monomorphic structures like strings

#### Mario Carneiro (Aug 10 2018 at 03:13):

what does that mean? What is the type of traverse in this case?

#### Simon Hudon (Aug 10 2018 at 03:16):

that would look like

class mono_traversable (t a : Type u) :=
(traverse : Π {m : Type u → Type u} [applicative m],
(a → m a) → t → m t)


#### Johan Commelin (Aug 10 2018 at 04:50):

Lean has chosen to handle modules and namespaces orthogonally. A nice choice, I think. It means that if you need to prove something about lists, it doesn't need to go into the file list.lean, you can just prove list.foobar in your own file. Or you write

namespace list

lemma foobar : ....

end list


Of course, that also means that you don't get access to list.foobar by just import data.list. You will also have to import the file where list.foobar is stated.

open list means that inside the section/file where you issued the open command, you can just write foobar instead of list.foobar. If you already had a foobar, this would lead to ambiguity. You can close one of them with close. The root namespace is called _root_.

#### Johan Commelin (Aug 10 2018 at 07:11):

But if you use mathlib, you can import meta.exprand use expr.list_local_const

I really think that it is a pity that there is group theory in core, and stuff like this in mathlib... I wish it was the other way round (-;

Last updated: May 11 2021 at 00:31 UTC