traversable

Stream: general

[Kenny Lau]

is free_group traversable?

[Simon Hudon]

I didn't read all that thread. Did you end up with a quotient on an inductive type for free_group?

[Kenny Lau]

sure

[Simon Hudon]

What is the equivalence relation and the inductive type?

[Kenny Lau]

https://github.com/leanprover-community/mathlib/blob/master/src/group_theory/free_group.lean

[Kenny Lau]

/-- Reduction step: `w * x * x⁻¹ * v ~> w * v` -/
inductive red.step : list (α × bool) → list (α × bool) → Prop
| bnot {L₁ L₂ x b} : red.step (L₁ ++ (x, b) :: (x, bnot b) :: L₂) (L₁ ++ L₂)

[Simon Hudon]

That looks traversable

[Simon Hudon]

Oh, wait, no, that's more complex than I thought. I'm not sure

[Reid Barton]

Probably not. One thinig you can do with traversable T is write a function T a -> list a which lists "all the as in a T a in order". I think this function is also supposed to be natural in a.
Now "all the as in a T a" may not really have a meaning a priori, but still it seems unlikely that you could write a sensible instance for something like the free group or free commutative monoid or any structure where the relations involve duplicating, dropping, or reordering variables.

[Reid Barton]

Maybe you could define a traversable_up_to_order class which only quantifies over commutative monads, and then it could have instances which are types formed by a quotient which reorders as, etc. This stuff grew out of Haskell, which doesn't have quotient types, so variants like this haven't been explored as far as I know.

[Simon Hudon]

For a group you probably need idempotency too ... and probably more now that I think of it. Some sort of cancellation

[Simon Hudon]

Thanks for the name traversable_up_to_order. I've been thinking about adding this class

[Reid Barton]

Yes, for free_group, you would need a monad where you can undo effects, and that doesn't sound like the kind of thing there would be many examples of.

[Simon Hudon]

Actually, that might be an opportunity for a sort of undo / redo design pattern

[Nicholas Scheel]

@Reid Barton I think you just need a commutative applicative, where f <$> fa <*> fb = flip f <$> fb <*> fa ... option is a good example of an applicative functor that supports that, plus the writer monad (over a commutative monoid) ... similarly, applicative validation[1] over a commutative monoid will be a commutative applicative – of course, it would be slightly ironic to traverse a free commutative monoid into another free commutative monoid, but it would work :wink:

[1] https://pursuit.purescript.org/packages/purescript-validation/4.2.0/docs/Data.Validation.Semigroup