23trees

Stream: new members

[Edward Ayers]

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]

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

[Edward Ayers]

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

[Simon Hudon]

You can see the api here: https://github.com/leanprover/lean/blob/a666c7f04eb77ecfd29f253b7fc389a4507404f1/library/init/data/rbmap/basic.lean

[Simon Hudon]

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

Unfortunately, not yet.

[Edward Ayers]

thanks

[Simon Hudon]

No problems :)

[Edward Ayers]

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

[Simon Hudon]

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]

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

[Simon Hudon]

you can use expr.fold.

[Simon Hudon]

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

[Edward Ayers]

fab

[Edward Ayers]

What is the difference between import and open?

[Simon Hudon]

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

[Edward Ayers]

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

[Simon Hudon]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

the set

[Simon Hudon]

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]

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

[Mario Carneiro]

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

[Simon Hudon]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Simon Hudon]

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]

oh, no I wasn't thinking that

[Mario Carneiro]

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

[Mario Carneiro]

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

[Simon Hudon]

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

[Mario Carneiro]

existential types don't really work in lean though

[Mario Carneiro]

because of predicativity

[Simon Hudon]

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]

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

[Simon Hudon]

Yeah, it is annoying to say the least

[Mario Carneiro]

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

[Simon Hudon]

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

[Mario Carneiro]

At the very least

[Mario Carneiro]

Indeed there probably isn't much else they can support

[Simon Hudon]

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

[Mario Carneiro]

that sounds ominous

[Mario Carneiro]

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

[Simon Hudon]

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]

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

[Simon Hudon]

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]

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]

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]

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

[Simon Hudon]

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]

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

[Mario Carneiro]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Mario Carneiro]

do you know any category theoretic treatment of traversable?

[Simon Hudon]

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]

Haskell only mentions axioms 1,2,5

[Mario Carneiro]

the map_traverse and traverse_map axioms aren't mentioned

[Simon Hudon]

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]

(the map of t, not f)

[Mario Carneiro]

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 ]

[Simon Hudon]

:laughing:

[Simon Hudon]

I guess you now know that bifunctor and bitraversable are coming

[Simon Hudon]

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

[Mario Carneiro]

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

[Simon Hudon]

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]

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]

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 (-;