Scott Brickner wrote:
It's actually not arbitrary.
[...]
A ≤ B iff A ⊆ B
A ⊆ B iff (x ∊ A) ⇒ (x ∊ B)
Alternatively and dually but equally naturally,
A ≥ B iff A ⊆ B iff (x ∊ A) ⇒ (x ∊ B)
and then we would have False > True.
Many of you are platonists rather than formalists; you have a strong
conviction in your intuition, and you call your intuition natural. You
think ∅≤U is more natural than ∅≥U because ∅ has fewer elements than U.
(Why else would you consider it unnatural to associate ≥ with ⊆?) But
that is only one of many natural intuitions.
There are two kinds of natural intuitions: disjunctive ones and
conjunctive ones. The elementwise intuition above is a disjunctive one.
It says, we should declare {0}≤{0,1} because {0} corresponds to the
predicate (x=0), {0,1} corresponds to the predicate (x=0 or x=1), you
see the latter has more disjuncts, so it should be a larger predicate.
However, {0} and {0,1} are toy, artificial sets, tractible to enumerate
individuals. As designers of programs and systems, we deal with real,
natural sets, intractible to enumerate individuals. For example, when
you design a data type to be a Num instance, you write down two
QuickCheck properties:
x + y = y + x
x * y = y * x
And lo, you have specified a conjunction of two predicates! The more
properties (conjuncts) you add, the closer you get to ∅ and further from
U, when you look at the set of legal behaviours. Therefore a conjunctive
intuition deduces ∅≥U to be more natural.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
