Zulip Chat Archive

Stream: general

Topic: type class traversable


Simon Hudon (Mar 07 2018 at 23:37):

I have written a type class traversable similar to that of Haskell. Universe polymorphism has made the task challenging but I think I have reached a reasonable compromise. I'd love to hear what the community thinks of it:

https://github.com/cipher1024/mathlib/commit/2f4aa9ed9c0e83d26ea3ae876b801851db6fb8ec

Simon Hudon (Mar 07 2018 at 23:46):

To the non-haskellers: traversable is a way of generalizing Lean's mmap : (α → m β) → list α → m (list β) so that it works with more collections than just list.

Andrew Ashworth (Mar 08 2018 at 02:36):

heh, i haven't used mmap either, unfortunately

Andrew Ashworth (Mar 08 2018 at 02:36):

is this similar to Iterable or Sequence in other languages?

Simon Hudon (Mar 08 2018 at 02:37):

It is similar. The big difference is that is has a nice specification

Simon Hudon (Mar 08 2018 at 02:39):

If you compare to map, map allows you to replace any element of a list but does not allow you to perform any effect (updating state, performing, I/O, raising exceptions, etc) in the process. Having a monad m (actually, we only need m to be an applicative) allows you to perform arbitrary effects in the process of replacing the elements of the collection.

Andrew Ashworth (Mar 08 2018 at 02:40):

so for example, how might I traverse the rb-tree implementation in lean core?

Andrew Ashworth (Mar 08 2018 at 02:40):

is it easy to adapt an arbitrary data structure to fit the interface?

Simon Hudon (Mar 08 2018 at 02:41):

If you have ask_age : string -> io nat which prompts the user for their age using stdin and stdout, mmap ask_age user_list creates the list of the age of all users

Simon Hudon (Mar 08 2018 at 02:46):

is it easy to adapt an arbitrary data structure to fit the interface?

It would be tricky for rbtree because we have an assumption, the ordering, on the type parameter. functor, foldable, traversable, applicative and monad requires that any type can be substituted for the type variable. But if you have rbmap, you can traverse the value and you can extend the interface to indexed_traversable so that when you traverse the value, you can read the key as well.

Andrew Ashworth (Mar 08 2018 at 02:48):

interesting, i wish i could provide feedback, but I think I'd need to sit down with haskell for awhile first and learn how these all work

Andrew Ashworth (Mar 08 2018 at 02:50):

but i can see how useful it would be to have a uniform interface for any data-structure, and traverse it in some deterministic order

Simon Hudon (Mar 08 2018 at 02:53):

I find it very useful in Haskell and easier to reason about than the iterable patterns that I have encountered. I'm hoping having access to traversable laws will make them awesomer

Mario Carneiro (Mar 08 2018 at 02:56):

What is the difference between a traversable and something that coerces to a list?

Mario Carneiro (Mar 08 2018 at 02:57):

I'm not so sure about how you dealt with the universe stuff

Simon Hudon (Mar 08 2018 at 02:59):

If you're looking at my_collection, traverse : (α → m β) → my_collection α → m (my_collection β). You're getting a my_collection back afterwards. Coercible to list would be the weaker foldable.

Simon Hudon (Mar 08 2018 at 03:00):

And it is still better than coercible from list because structures like vectors, matrices and even pairs cannot be made from arbitrary lists

Mario Carneiro (Mar 08 2018 at 03:07):

Although it is a little limiting, I think you should make all the universes the same in traversable, similar to how monad works

Simon Hudon (Mar 08 2018 at 03:12):

I have considered that. With monad, we have Type u -> Type v (two universes) which constrains the type variable to be of type Type u and not to change. If I take a similar approach, the collection has to be of type Type u -> Type u (only one universe) and also limits the type of applicative used. I thought of separating has_traverse and traversable to limit the polymorphism in traversable but not in has_traverse

Simon Hudon (Mar 08 2018 at 03:13):

Another option is to limit the polymorphism in both but provide type classes like can_traverse my_appl my_collection to provide more flexible traversals and laws

Mario Carneiro (Mar 08 2018 at 03:26):

Right, I think the monad/applicative also has to be Type u -> Type u for the statement of has_traverse to make sense. The way this has been done in things like list.bind is to have the definition itself be fully polymorphic, but the definition that gets used in the instance is universe monomorphic. So the polymorphic functions are still available, you just don't get the typeclass niceties in this case

Mario Carneiro (Mar 08 2018 at 03:27):

Luckily, almost all programming stuff fits in Type 0

Mario Carneiro (Mar 08 2018 at 03:28):

except existential types, but these have their own issues

Simon Hudon (Mar 08 2018 at 03:33):

That makes sense. Thinking back, the reason I was obstinate about making traversable as polymorphic as possible is that I was trying to mimic the bound Haskell library which encodes de Bruijn indices in type parameters. That gave me something of type Type 0 -> Type 1 but luckily, on the google group, someone proposed a nicer encoding. I think I will survive making traversable universe monomorphic

Simon Hudon (Mar 08 2018 at 19:17):

@Sebastian Ullrich Would this be more at home in the core library?

Sebastian Ullrich (Mar 08 2018 at 22:00):

@Simon Hudon Not sure. Almost all recent additions to core lib are things we actually need there, but I wouldn't mind having access to sequence.

Simon Hudon (Mar 08 2018 at 22:03):

My thinking was that traversable is such an organizing principle in the Haskell base library that supporting right from the start might generalize a good portion of the machinery there. There was a recent version of the base library (I think 4.9) that made that step and de facto reduced some of the redundancy

Simon Hudon (Mar 08 2018 at 22:04):

And sequence is a fun thing to have when you need f and g to commute in any f (g a) type.

Scott Morrison (Mar 08 2018 at 23:53):

(deleted)


Last updated: Dec 20 2023 at 11:08 UTC