haskell typeclasses

Stream: batteries

[Kim Morrison]

Yes, I wanted the complement --- are there any files in Control which are not imported outside of Control.

[Aaron Liu]

Kim Morrison said:

Yes, I wanted the complement --- are there any files in Control which are not imported outside of Control.

A quick search finds file#Control/Fold, file#Control/LawfulFix, and file#Control/Random

[Kim Morrison]

@Mario Carneiro would you want those files in Batteries?

If we could find another home for Haskell, I think that would be good. These files have not been receiving any love in Mathlib for years.

[Mario Carneiro]

It could move to batteries... I don't really want to maintain a leancolls style typeclass hierarchy but maybe it's something batteries could support, with the primary motivation being that it's a "vocabulary type", it's annoying if everyone redefines it.

[Mario Carneiro]

cc: @François G. Dorais , opinions?

[Notification Bot]

5 messages were moved here from #mathlib4 > Technical Debt Counters by Mario Carneiro.

[François G. Dorais]

I think it could move but I'm rather busy this week so this is just a preliminary opinion.