On Thu, Jul 12, 2007 at 10:11:07PM +0100, Andrew Coppin wrote:
Felipe Almeida Lessa wrote:
On 7/12/07, Andrew Coppin [EMAIL PROTECTED] wrote:
How come the set of all sets doesn't exist?
http://www.google.com/search?q=set+of+all+sets
leads to http://en.wikipedia.org/wiki/Set_of_all_sets which
On Thursday 12 July 2007 22:57, Steve Downey wrote:
Almost, I think. A functor is a mapping from the arrows, or morphisms,
in a category to arrows in a category.
Oops, yes, indeed. Good catch, thanks. :-)
Alexis.
___
Haskell-Cafe mailing list
On Thursday 12 July 2007 04:40, Andrew Coppin wrote:
I once sat down and tried to read about Category Theory. I got almost
nowhere though; I cannot for the life of my figure out how the
definition of category is actually different from the definition of
set. Or how a functor is any different
Bernie Pope wrote:
On 12/07/2007, at 4:43 AM, Andrew Coppin wrote:
Bernie Pope wrote:
This reminds me of a little joke that Conor McBride had in a post a
while ago:
unJust :: Maybe wmd - wmd
Oh, very good!
I must write that down somewhere...
I tell it to my Haskell students each
Alexis Hazell wrote:
On Thursday 12 July 2007 04:40, Andrew Coppin wrote:
I once sat down and tried to read about Category Theory. I got almost
nowhere though; I cannot for the life of my figure out how the
definition of category is actually different from the definition of
set. Or how a
Stefan O'Rear wrote:
On Thu, Jul 12, 2007 at 07:19:07PM +0100, Andrew Coppin wrote:
I'm still puzzled as to what makes the other categories so magical that
they cannot be considered sets.
I'm also a little puzzled that a binary relation isn't considered to be a
function...
From the
Alexis Hazell wrote:
On Thursday 12 July 2007 04:40, Andrew Coppin wrote:
I once sat down and tried to read about Category Theory. I got almost
nowhere though; I cannot for the life of my figure out how the
definition of category is actually different from the definition of
set. Or how
AC I'm still puzzled as to what makes the other categories so magical
AC that they cannot be considered sets.
They are just too big. The set of all sets can't exist, you know.
That's news.
How come the set of all sets doesn't exist?
Well, you mentioned that you have some knowledge of
On 7/12/07, Andrew Coppin [EMAIL PROTECTED] wrote:
How come the set of all sets doesn't exist?
http://www.google.com/search?q=set+of+all+sets
leads to http://en.wikipedia.org/wiki/Set_of_all_sets which has the
answer, I think.
--
Felipe.
___
They are just too big. The set of all sets can't exist, you know.
That's news.
It was news to Frege.
How come the set of all sets doesn't exist?
Russell's paradox - see e.g. Halmos: Naive Set Theory.
___
Haskell-Cafe mailing list
On Thu, 12 Jul 2007 20:36:47 +0100, you wrote:
How come the set of all sets doesn't exist?
In naive set theory, the existence of the set of all sets leads to a
logical paradox. Specifically, the set of all sets would have to contain
as a member the set of all sets that are not members of
On 7/12/07, Andrew Coppin [EMAIL PROTECTED] wrote:
Stefan O'Rear wrote:
On Thu, Jul 12, 2007 at 07:19:07PM +0100, Andrew Coppin wrote:
I'm still puzzled as to what makes the other categories so magical that
they cannot be considered sets.
I thought I'd dive in with a comment to explain why
Felipe Almeida Lessa wrote:
On 7/12/07, Andrew Coppin [EMAIL PROTECTED] wrote:
How come the set of all sets doesn't exist?
http://www.google.com/search?q=set+of+all+sets
leads to http://en.wikipedia.org/wiki/Set_of_all_sets which has the
answer, I think.
Ouch.
Clearly, set theory is way
On Jul 12, 2007, at 17:11 , Andrew Coppin wrote:
Felipe Almeida Lessa wrote:
On 7/12/07, Andrew Coppin [EMAIL PROTECTED] wrote:
How come the set of all sets doesn't exist?
http://www.google.com/search?q=set+of+all+sets
leads to http://en.wikipedia.org/wiki/Set_of_all_sets which has the
Cale Gibbard wrote:
On 10/07/07, Andrew Coppin [EMAIL PROTECTED] wrote:
Stefan O'Rear wrote:
Another good example:
foo :: ∀ pred : Nat → Prop . (∀ n:Nat . pred n → pred (n + 1))
→ pred 0 → ∀ n : Nat . pred n
x_x
Which you can read as For all statements about natural numbers, if the
Tim Chevalier wrote:
On 7/10/07, Andrew Coppin [EMAIL PROTECTED] wrote:
On the one hand, it feels exciting to be around a programming language
where there are deep theoretical discoveries and new design territories
to be explored. (Compared to Haskell, the whole C / C++ / Java /
JavaScript /
Jim Burton wrote:
Andrew Coppin wrote:
On the one hand, it feels exciting to be around a programming language
where there are deep theoretical discoveries and new design territories
to be explored. (Compared to Haskell, the whole C / C++ / Java /
JavaScript / Delphi / VisualBasic / Perl /
Tony Morris wrote:
I'd like throw in another vote for TAPL. I've been reading it lately
and it
honestly makes type theory feel fairly simple and natural. I think
Pierce's
writing is very clear, but occasionally the exercises make the problem
sound
harder than it is and it gets a little
Michael T. Richter wrote:
On Tue, 2007-10-07 at 20:59 +0100, Andrew Coppin wrote:
But it rambled on for, like, 3 pagefulls of completely opaque
set-theoretic gibberish before I arrived at the (cryptically phrased)
statements I presented above. Why it didn't just *say* that in the first
place
Once during a talk I noticed I was getting strange looks and realized
I was using the term string too freely with an audience of non-
technical people. About half of them were in a beginning linguistics
class and could at least handle trees later on (which terminology I
had thought in
Andrew Coppin wrote:
Jim Burton wrote:
Andrew Coppin wrote:
On the one hand, it feels exciting to be around a programming language
where there are deep theoretical discoveries and new design territories
to be explored. (Compared to Haskell, the whole C / C++ / Java /
JavaScript /
Jim Burton wrote:
Andrew Coppin wrote:
The other downside is that you end up with a world where most of the
tools are in fact one-man research projects or small toys.
There are a few good, powerful, useful things out there. (GHC and Parsec
immediately spring to mind.) But there's also a
On 10/07/07, Andrew Coppin [EMAIL PROTECTED] wrote:
Stefan O'Rear wrote:
Another good example:
foo :: ∀ pred : Nat → Prop . (∀ n:Nat . pred n → pred (n + 1))
→ pred 0 → ∀ n : Nat . pred n
x_x
Which you can read as For all statements about natural numbers, if the
statement applies
OK, so technically it's got nothing to do with Haskell itself, but...
I was reading some utterly incomprehensible article in Wikipedia. It was
saying something about categories of recursive sets or some nonesense
like that, and then it said something utterly astonishing.
By playing with the
On Tuesday 10 July 2007, Andrew Coppin wrote:
OK, so technically it's got nothing to do with Haskell itself, but...
Actually, it does: the basic technologies underlying Haskell (combinatory
logic and the Hindley-Milner type system) were originally invented in the
course of this stream of
On Tue, Jul 10, 2007 at 08:19:53PM +0100, Andrew Coppin wrote:
OK, so technically it's got nothing to do with Haskell itself, but...
I was reading some utterly incomprehensible article in Wikipedia. It was
saying something about categories of recursive sets or some nonesense like
that, and
Stefan O'Rear wrote:
On Tue, Jul 10, 2007 at 08:19:53PM +0100, Andrew Coppin wrote:
So is this all a huge coincidence? Or have I actually suceeded in
comprehending Wikipedia?
Yup, you understood it perfectly.
This is a rare event... I must note it on my calendar! o_O
This is
On 7/10/07, Andrew Coppin [EMAIL PROTECTED] wrote:
But what does, say, Maybe x - x say?
Maybe X is the same as True or X, where True is the statement that
is always true. Remember that the definition is
data Maybe X = Nothing | Just X
You can read | as 'or', 'Just' as nothing but a wrapper
On Tue, Jul 10, 2007 at 08:59:16PM +0100, Andrew Coppin wrote:
http://haskell.org/haskellwiki/Curry-Howard-Lambek_correspondence might
be interesting - same idea, but written for a Haskell audience.
An interesting read - although again a little over my head.
I find myself wondering... A
Stefan O'Rear wrote:
On Tue, Jul 10, 2007 at 08:59:16PM +0100, Andrew Coppin wrote:
I find myself wondering... A polymorphic type signature such as (a - b) -
a - b says given that a implies b and a is true, b is true. But what
does, say, Maybe x - x say?
Given that x may or may not
On 7/10/07, Dan Piponi [EMAIL PROTECTED] wrote:
On 7/10/07, Andrew Coppin [EMAIL PROTECTED] wrote:
But what does, say, Maybe x - x say?
Silly me. You reversed the arrows and I copied you. (Could it be
something to do with the other conversation we were having?)
I meant to say:
So x - Maybe
Jonathan Cast wrote:
On Tuesday 10 July 2007, Andrew Coppin wrote:
OK, so technically it's got nothing to do with Haskell itself, but...
Actually, it does
I rephrase: This isn't *specifically* unique to Haskell, as such.
Now, Wikipedia seems to be suggesting something really
I means that you can view programming as constructing witnesses to
proofs - programs becoming the (finite) steps that, when followed,
construct a proof.
Intuitionism only allows you to make statements that can be proved
directly - no Reductio ad absurdum only good, honest to goodness
Andrew Coppin wrote:
On the one hand, it feels exciting to be around a programming language
where there are deep theoretical discoveries and new design territories
to be explored. (Compared to Haskell, the whole C / C++ / Java /
JavaScript / Delphi / VisualBasic / Perl / Python thing
On 7/10/07, Jim Burton [EMAIL PROTECTED] wrote:
Andrew Coppin wrote:
On the one hand, it feels exciting to be around a programming language
where there are deep theoretical discoveries and new design territories
to be explored. (Compared to Haskell, the whole C / C++ / Java /
JavaScript
I'd like throw in another vote for TAPL. I've been reading it lately
and it
honestly makes type theory feel fairly simple and natural. I think
Pierce's
writing is very clear, but occasionally the exercises make the problem
sound
harder than it is and it gets a little confusing. A friend
On Jul 10, 2007, at 15:59 , Andrew Coppin wrote:
I find myself wondering... A polymorphic type signature such as (a -
b) - a - b says given that a implies b and a is true, b is
true. But what does, say, Maybe x - x say?
Actually, because parentheses naturally group to the right in type
On 11/07/2007, at 9:02 AM, Brandon S. Allbery KF8NH wrote:
On Jul 10, 2007, at 15:59 , Andrew Coppin wrote:
I find myself wondering... A polymorphic type signature such as (a
- b) - a - b says given that a implies b and a is true, b is
true. But what does, say, Maybe x - x say?
On Tue, 2007-10-07 at 20:59 +0100, Andrew Coppin wrote:
But it rambled on for, like, 3 pagefulls of completely opaque
set-theoretic gibberish before I arrived at the (cryptically phrased)
statements I presented above. Why it didn't just *say* that in the first
place I have no idea...
39 matches
Mail list logo
