Re: [Haskell-cafe] What puts False before True?
You're right. I didn't put that precisely enough. But, the inverse of
/any/ partial order is still a partial order.
With the set of natural numbers, is it still reasonable to say that the
order that puts 2 ≤ 1 is just as natural as the conventional order?
Probably not.
So, ⊆ is the /conventional/ order for sets, ⇒ is the conventional order
for predicates, ≤ is the conventional order for numbers, and so on. That
still dictates that False True is the conventional order for booleans.
Albert Y. C. Lai wrote:
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
--
-
What part of ph'nglui bglw'nafh Cthulhu R'lyeh wagn'nagl fhtagn don't you
understand?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What puts False before True?
All these smart math guys hanging around and nobody's given a really
decent answer to this?
It's actually not arbitrary. There's a strong connection between
predicates (functions that return boolean values) and sets. Any
predicate uniquely determines a set - the set of values for which it
returns true. Similarly, any set determines a predicate - one that
returns true exactly when the argument is a member of the set.
It's natural to define a partial order among sets from inclusion: A ≤ B
iff A ⊆ B. Viewing the sets as predicates, the corresponding
relationship between the predicates is implication. A ⊆ B iff (x ∊ A) ⇒
(x ∊ B) - so predicates are naturally ordered by implication. Viewed as
sets, the predicate that always returns False is equivalent to ∅ - the
empty set, while the predicate that always returns True is equivalent to
U - the universal set that contains everything (in naive set theory,
anyway - in axiomatic theories it gets a little more complicated).
So, since subset gives a natural order to sets, implication gives
a natural order to predicates, thus it's natural to say that the
Haskell expressions (const False) and (const True), which are
predicates, are ordered: (const False) (const True). And therefore,
it's natural to say that False True.
Anyway, that's my explanation for it. :)
Derek Elkins wrote:
Henning Thielemann wrote:
On Thu, 31 May 2007, Paul Hudak wrote:
PR Stanley wrote:
I think so, too. In Boolean algebra (which predates computers,
much less
C), FALSE has traditionally been associated with 0, and TRUE with
1. And
since 1 0, TRUE FALSE.
The question, however, still remains: why False = 0 and True 1? I
appreciate that it's so in boolean algebra but why? Why not True = 0
and False = 1?
Because if you take () to be (*), and (||) to be (+), you get a
homomorphism between the two resulting algebras (assuming 1+1 = 1).
It seems however, that if the number representations of False and True
are flipped, then we only need to flip the interpretations of () and
(||).
For me the choice fromEnum False == 0 fromEnum True == 1 seems rather
arbitrary.
It -is- arbitrary, in boolean algebra as well. not is an automorphism
between the two. However, we tend to think of 0 as associated with
nothing/the empty set and that maps naturally to {x | False}. There
are intuitive reasons why this choice was chosen, but no formal
reasons. Obviously, there are pragmatic reasons to use this choice in
programming languages, e.g. many languages use 0 to represent false
and non-zero or 1 to represent true and this is consistent with that.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
--
-
What part of ph'nglui bglw'nafh Cthulhu R'lyeh wagn'nagl fhtagn don't you
understand?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Versioning
Jacques Carette wrote: Neil Mitchell wrote: The biggest runtime crasher is probably pattern match failings, something that most of these type extensions don't catch at all! Array out-of-bounds, fromJust, head on an empty list, and pattern-match failures are in my list of things I wish the type system could help me with. And sometimes it can [again, see Oleg's posts]. But is definitely where I am *eager* to see developments. If I understand things correctly (admittedly, a big if ;) ) this is kind of the point of dependent types. A type is a set - when you put a type on an expression, you're asserting that the expression evaluates to a member of that set. So, foo :: Integer - Rational, among other things, asserts that the result of foo x (given that x is a member of the set of Integers) is a member of the set of Rationals. But why stop there? Why not be able to say that foo x is a /positive/ rational, or a non-negative rational between 0 and 1? Or, since we're just describing sets, why not explictly allow the set to depend on x? Why not let the result type be the set of rationals r such that 1/r == x? The Curry-Howard isomorphism leads to all of that. A program that outputs some value x is (isomorphic to) a proof that x is a member of some type. We just generally lack a sufficiently powerful type grammar to express that directly in the program. Dependent types let you make the types of output /depend/ on the actual values of the input. Check out Conor McBride and James McKinna's paper The View From the Left, and their work on the Epigram language to see where they've taken this... http://www.dcs.st-andrews.ac.uk/~james/ - fascinating stuff. I agree with you, though - I'm very eager to see further developments along these lines. It's the main reason I started learning Haskell, and I'm absolutely convinced that functional programming and this kind of increasingly strong typing are the way of the future for programming. -- - What part of ph'nglui bglw'nafh Cthulhu R'lyeh wagn'nagl fhtagn don't you understand? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Versioning
Jacques Carette wrote: Lennart Augustsson wrote: I must second this opinion. There's this (false) perception that you need all kinds of extensions to make Haskell usable. It's simply not true. Certain extensions can make your life easier, but that's it. To write code in Haskell, this is true. However, one of the wonderful things about Haskell is how much the type system helps you. And if you want the type system to help you even more [which, as a programmer having suffered from dynamic typing too long, I really want], those extensions are really needed. In other words, you can program in Haskell just fine without extensions. But if you want that next level in type safety, extensions is where it's at, at least for the kind of code I write. Or, to go the other way, if you don't care about type safety, you might as well program in Javascript. -- - What part of ph'nglui bglw'nafh Cthulhu R'lyeh wagn'nagl fhtagn don't you understand? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] what are the points in pointsfree?
Donald Bruce Stewart wrote: sdowney: i'm not naive enough to think they are the composition function, and i've gathered it has something to do with free terms, but beyond that i'm not sure. unless it also has something to do with fix points? The wiki knows all! :) http://haskell.org/haskellwiki/Pointfree 1 But pointfree has more points! A common misconception is that the 'points' of pointfree style are the (.) operator (function composition, as an ASCII symbol), which uses the same identifier as the decimal point. This is wrong. The term originated in topology, a branch of mathematics which works with spaces composed of points, and functions between those spaces. So a 'points-free' definition of a function is one which does not explicitly mention the points (values) of the space on which the function acts. In Haskell, our 'space' is some type, and 'points' are values. Hm. I've been lurking for a while, and this might be a bit of nit-picking as my first post, especially given I'm still a bit of a n00b in Haskell. I've been programming a long time, though - coming up on three decades now and virtually all of it really programming, no management. Anyway, as I understood it, the points were the terminal objects of the category in which you're working - in this case, pointed continuous partial orders (CPO), and the points are effectively values in the domain. The usage of point for terminal objects comes from the category of topological spaces, as you say,. and algebraic topology is where category theory found it's first big home - but that's not really what we're talking about here, is it? Category theory got the term from topology, which got it from geometry. So you could say point is position without dimension - but that's just not the point we're talking about anymore. So, the usage of point here refers a terminal object in the CPO category, which means a value of some datatype - in this particular case, a value in the domain of the function being defined. So when you give a definition that uses patterns for the parameters, the variables in the patterns get bound to the values in the domain of the function. If you write the function in a higher-order style, where you don't bind the values, your definition doesn't refer to the point at which it's being evaluated, hence point-free. -- - What part of ph'nglui bglw'nafh Cthulhu R'lyeh wagn'nagl fhtagn don't you understand? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
