On Sun, Dec 20, 2020 at 11:05:39PM +0100, Ben Franksen wrote:
Am 06.12.20 um 19:58 schrieb Sven Panne:
To me it's just the other way around: It violates aesthetics if it doesn't follow the mathematical definition in all cases, which is why I don't like NonEmpty here.
I think you've got that wrong.
x `elem` intersections [] = {definition} forall xs in []. x `elem` xs = {vacuous forall} true
Any proposition P(x) is true for all x in []. So the mathematical definition of intersections::[Set a]-> Set a would not be the empty set but the set of all x:a, which in general we have no way to construct.
Yes, and to bring this back to Sven's original claim | Why NonEmpty? I would expect "intersections [] = Set.empty", because | the result contains all the elements which are in all sets, | i.e. none. That's at least my intuition, is there some law which | this would violate? the correct definition of "intersections []" should be "all elements which are in all of no sets" i.e. _every_ value of the given type! Tom