[blep_]

This is also really kind of an artifact of how GROUP BY works in most database engines.

I've always liked the way MySQL/MariaDB let you omit things from the GROUP BY if they're provably unique in each group (here, if foo_id is a primary key of foo, and you're grouping by it, there can only ever be one foo.some_float for each foo_id).

I suspect in practice this would get rid of approximately all occurrences of group-by-float.