add `dflip`, a dependent version of `flip`

[joelberkeley]

This came out of https://github.com/idris-lang/Idris2/issues/2589. I thought, since @buzden gave it a 👍🏻 I'd see if there was wider support for it

I'm very aware this is in one of the most core modules in the stdlib, so we'll want to be sure it's worth adding.

[andrevidela]

The goal of prelude is to be as small as possible. dflip hasn't been something that's been asked for before so there is little reason to conclude it needs to exist in prelude. It would be nice to have but in that case, I would suggest to have it in base or maybe even contrib

[joelberkeley]

Happy to move it. Just let me know where

[andrevidela]

To remain consistent with #2456 We should place this in the same spot. I proposed Basics.Dependent, I suggest you chime in the thread to tell us what you think of this namespace for it

[gallais]

Control.Function, maybe? (I don't why it's in Control rather than Data like in Haskell).

[andrevidela]

That would be fine but then what would be the namespace for #2456?

[joelberkeley]

moved it to Control.Function. Put it at the top of the file so it doesn't get confused with the [Bi]injective stuff further down

[gallais]

Ah shoot the derive_traversable test is leaking information about the internal state of the compiler. :( Strange that the printing of EqMap uses named application rather than auto's @{}. :thinking:

[andrevidela]

Are we putting this in Basics.Dependent? @gallais @joelberkeley

[gallais]

I don't have a strong opinion one way or the other.

[joelberkeley]

I also don't have a strong opinion, though I would find it odd there being a Basics.Dependent without anything in Basics

[joelberkeley]

Ah shoot the derive_traversable test is leaking information about the internal state of the compiler. :( Strange that the printing of EqMap uses named application rather than auto's @{}. thinking

@gallais am i right in thinking that's not to do with this change? Should I wait for that to be fixed elsewhere?

[joelberkeley]

Ah shoot the derive_traversable test is leaking information about the internal state of the compiler. :( Strange that the printing of EqMap uses named application rather than auto's @{}. thinking

@gallais this PR still appears to be failing for this reason. Do you know when or if that issue will be fixed?

[gallais]

The canonical solution is to use a bit of sed to drop numbers in the output

[joelberkeley]

The canonical solution is to use a bit of sed to drop numbers in the output

sorry I'm not following at all

[gallais]

For instance: https://github.com/idris-lang/Idris2/blob/main/tests/idris2/basic044/run

[joelberkeley]

yeah I don't want this PR that much. Can close if no-one feels strongly