Gregg Reynolds wrote:
On Mon, Feb 2, 2009 at 2:25 PM, Ketil Malde ke...@malde.org wrote:
Gregg Reynolds d...@mobileink.com writes:
Just shorthand for something like data Tcon a = Dcon a, applied to Int.
Any data constructor expression using an Int will yield a value of type
Tcon
Int.
On Tuesday 03 February 2009 9:05:08 pm wren ng thornton wrote:
Extending things to GADTs, this is also the reason why functions are
called exponential and denoted as such in category theory:
|N - M| = |M| ^ |N|
That's the number of functions that exist in that type. Not all of these
are
Martijn van Steenbergen wrote:
To my naive mind this sounds
suspiciously like the set of all sets, so it's too big to be a set.
Here you're probably thinking about the distinction between countable
and uncountable sets. See also:
http://en.wikipedia.org/wiki/Countable_set
No - it's even
* Martijn van Steenbergen wrote:
Int has 2^32 values, just like in Java.
Haskell Report 6.4 (revised):
The finite-precision integer type Int covers at least
the range [ - 2^29, 2^29 - 1].
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
Hi Martijn,
On Mon, Feb 2, 2009 at 9:49 AM, Martijn van Steenbergen
mart...@van.steenbergen.nl wrote:
There are many answers to the question what is a type?, depending on
one's
view.
One that has been helpful to me when learning Haskell is a type is a set
of
values.
That's the way I've
Thinking of types as sets is not a bad approximation. You need to add
_|_ to your set of values, though.
So, Bool={_|_, False, True}, Nat={_|_,Zero,Succ _|_, Succ Zero, ...}
2009/2/2 Gregg Reynolds d...@mobileink.com:
Hi Martijn,
On Mon, Feb 2, 2009 at 9:49 AM, Martijn van Steenbergen
Hi and thanks for the response,
On Mon, Feb 2, 2009 at 10:32 AM, Lennart Augustsson
lenn...@augustsson.netwrote:
Thinking of types as sets is not a bad approximation. You need to add
_|_ to your set of values, though.
So, Bool={_|_, False, True}, Nat={_|_,Zero,Succ _|_, Succ Zero, ...}
On Mon, Feb 2, 2009 at 8:09 AM, Gregg Reynolds d...@mobileink.com wrote:
Yes, that's my hypothesis: type constructors take us outside of set
theory (ZF set theory, at least). I just can't prove it.
It's too big for Set Theory if you insist on representing functions
in type theory as
If we're talking Haskell types here I think it's reasonable to talk
about the values of a type as those that we can actually express in
the Haskell program, any other values are really besides the point.
Well, if you have a more philosophical view of types then I guess
there is a point, but I
Lennart Augustsson wrote:
The Haskell function space, A-B, is not uncountable.
There is only a countable number of Haskell functions you can write,
so how could there be more elements in the Haskell function space? :)
The explanation is that the Haskell function space is not the same as
the
You can enumerate all possible implementations of functions of type
(Integer - Bool).
Just enumerate all strings, and give this to a Haskell compiler
f :: Integer - Bool
f = enumerated-string-goes-here
if the compiler is happy you have an implementation.
The enumerated functions do not include
I had the same idea, here's my implemention, running on an old Winhugs
2001 (and GHC 6.8).
regards, Daniel
import System
import Directory
chars = map chr [32..126]
string 0 = return
string n = do
c - chars
s - string (n-1)
return (c:s)
mkfun n = do
s - string n
return (f :: Integer -
oops, the '$ drop 1000' in the main function should not be there...
Daniel van den Eijkel schrieb:
I had the same idea, here's my implemention, running on an old Winhugs
2001 (and GHC 6.8).
regards, Daniel
import System
import Directory
chars = map chr [32..126]
string 0 = return
string
Gregg Reynolds d...@mobileink.com writes:
This gives a very interesting way of looking at Haskell type
constructors: a value of (say) Tcon Int is anything that satisfies
isA Tcon Int.
Reminiscent of arguments between dynamic and static typing camps - as
far as I understand, a dynamic type
On Mon, Feb 2, 2009 at 11:51 AM, Lennart Augustsson
lenn...@augustsson.netwrote:
If we're talking Haskell types here I think it's reasonable to talk
about the values of a type as those that we can actually express in
the Haskell program, any other values are really besides the point.
Well, if
On Mon, Feb 2, 2009 at 12:39 PM, Ketil Malde ke...@malde.org wrote:
Gregg Reynolds d...@mobileink.com writes:
This gives a very interesting way of looking at Haskell type
constructors: a value of (say) Tcon Int is anything that satisfies
isA Tcon Int.
Reminiscent of arguments between
Hi,
Am Montag, den 02.02.2009, 11:06 -0700 schrieb Luke Palmer:
That question has kind of a crazy answer.
In mathematics, Nat - Bool is uncountable, i.e. there is no function
Nat - (Nat - Bool) which has every function in its range.
But we know we are dealing with computable functions,
On Mon, 2009-02-02 at 17:30 +0100, Krzysztof Skrzętnicki wrote:
Do they? Haskell is a programing language. Therefore legal Haskell
types has to be represented by some string. And there are countably
many strings (of which only a subset is legal type representation, but
that's not important).
Gregg Reynolds d...@mobileink.com writes:
Just shorthand for something like data Tcon a = Dcon a, applied to Int.
Any data constructor expression using an Int will yield a value of type Tcon
Int.
Right. But then the set of values is isomorphic to the set of Ints,
right?
I don't follow
Hi Gregg,
Firsly: I'm not an expert on this, so if anyone thinks I'm writing
nonsense, do correct me.
There are many answers to the question what is a type?, depending on
one's view.
One that has been helpful to me when learning Haskell is a type is a
set of values. When seen like this it
On Mon, Feb 2, 2009 at 3:25 PM, Ketil Malde ke...@malde.org wrote:
Gregg Reynolds d...@mobileink.com writes:
Just shorthand for something like data Tcon a = Dcon a, applied to Int.
Any data constructor expression using an Int will yield a value of type Tcon
Int.
Right. But then the set of
The Haskell function space, A-B, is not uncountable.
There is only a countable number of Haskell functions you can write,
so how could there be more elements in the Haskell function space? :)
The explanation is that the Haskell function space is not the same as
the functions space in set theory.
Talking about the class of all Haskell types is a little tricky.
If one program has
data Foo x = Ick x | Ack x
and another program has
data Bar y = Ack y | Ick y
are {Program1}Foo and {Program2}Bar the same type or not?
They are certainly isomorphic.
Any Haskell program can be
Do they? Haskell is a programing language. Therefore legal Haskell types has
to be represented by some string. And there are countably many strings (of
which only a subset is legal type representation, but that's not
important).
All best
Christopher Skrzętnicki
On Mon, Feb 2, 2009 at 17:09,
2009/2/2 Joachim Breitner m...@joachim-breitner.de
Hi,
Am Montag, den 02.02.2009, 11:06 -0700 schrieb Luke Palmer:
That question has kind of a crazy answer.
In mathematics, Nat - Bool is uncountable, i.e. there is no function
Nat - (Nat - Bool) which has every function in its range.
Hi,
Am Montag, den 02.02.2009, 15:30 -0700 schrieb Luke Palmer:
That's what I meant.
thanks for the clarification, I indeed were confused by the notation and
saw Haskell functions where you meant mathematical functions.
Greetings,
Joachim
--
Joachim nomeata Breitner
mail:
2009/2/2 Luke Palmer lrpal...@gmail.com:
However! If we have a function f : Nat - Nat - Bool, we can construct the
diagonalization g : Nat - Bool as: g n = not (f n n), with g not in the
range of f. That makes Nat - Bool computably uncountable.
This is making my head explode. How is g not
2009/2/2 Luke Palmer lrpal...@gmail.com:
But Nat ~ Bool is computably uncountable, meaning there is no injective
(surjective?)
function Nat ~ (Nat ~ Bool), by the diagonal argument above.
Given that the Haskell functions Nat - Bool are computably
uncountable, you'd expect that for any
Hi,
Am Montag, den 02.02.2009, 14:41 -0800 schrieb Dan Piponi:
2009/2/2 Luke Palmer lrpal...@gmail.com:
But Nat ~ Bool is computably uncountable, meaning there is no injective
(surjective?)
function Nat ~ (Nat ~ Bool), by the diagonal argument above.
Given that the Haskell functions
The Haskell function space, A-B, is not uncountable.
There is only a countable number of Haskell functions you can write,
so how could there be more elements in the Haskell function space? :)
The explanation is that the Haskell function space is not the same as
the functions space in set theory.
On Mon, Feb 2, 2009 at 9:47 AM, Martijn van Steenbergen
mart...@van.steenbergen.nl wrote:
Lennart Augustsson wrote:
The Haskell function space, A-B, is not uncountable.
There is only a countable number of Haskell functions you can write,
so how could there be more elements in the Haskell
On Mon, Feb 2, 2009 at 3:41 PM, Dan Piponi dpip...@gmail.com wrote:
2009/2/2 Luke Palmer lrpal...@gmail.com:
But Nat ~ Bool is computably uncountable, meaning there is no injective
(surjective?)
function Nat ~ (Nat ~ Bool), by the diagonal argument above.
Given that the Haskell functions
On Mon, Feb 02, 2009 at 02:41:36PM -0800, Dan Piponi wrote:
2009/2/2 Luke Palmer lrpal...@gmail.com:
But Nat ~ Bool is computably uncountable, meaning there is no injective
(surjective?)
function Nat ~ (Nat ~ Bool), by the diagonal argument above.
Given that the Haskell functions Nat
Luke Palmer wrote:
and pick out the ones which denote a total computable function [...]
How important is totality to this argument? If it is important, how do you
decide it?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
On Mon, Feb 2, 2009 at 10:05 AM, Andrew Butterfield
andrew.butterfi...@cs.tcd.ie wrote:
Martijn van Steenbergen wrote:
To my naive mind this sounds
suspiciously like the set of all sets, so it's too big to be a set.
Here you're probably thinking about the distinction between countable and
On Mon, Feb 2, 2009 at 4:23 PM, Matthew Brecknell hask...@brecknell.orgwrote:
Luke Palmer wrote:
and pick out the ones which denote a total computable function [...]
How important is totality to this argument? If it is important, how do you
decide it?
It is at the very essence of the
On Mon, Feb 2, 2009 at 4:18 PM, Reid Barton rwbar...@math.harvard.eduwrote:
So here's a programming challenge: write a total function (expecting
total arguments) toSame :: ((Nat - Bool) - Nat) - (Nat - Bool,Nat
- Bool) that finds a pair that get mapped to the same Nat.
Ie. f a==f b
On Mon, Feb 2, 2009 at 3:18 PM, Reid Barton rwbar...@math.harvard.edu wrote:
toSame f = (const True, head [ ( k) | k - [1..], f (const True) == f ( k)
])
Nice! I like it because at first look it seems like there's no reason
for this to terminate, but as you correctly argue, it always does.
--
Gregg Reynolds wrote:
Hi,
The concept of type seems to be a little like porno: I know it when
I see it, but I can't define it (apologies to Justice Stewart). I've
picked through lots of documents that discuss types in various ways,
but I have yet to find one that actually says what a type
Luke, sorry for being offtopic, but you are more and more intriguing
me with topology.
I wonder if any stuff from it has, apart from applications in
computability/complexity, also computational applications as useful as
monoids or rings do (i.e. parallel prefix sums).
2009/2/3 Luke Palmer
On Mon, Feb 2, 2009 at 2:25 PM, Ketil Malde ke...@malde.org wrote:
Gregg Reynolds d...@mobileink.com writes:
Just shorthand for something like data Tcon a = Dcon a, applied to Int.
Any data constructor expression using an Int will yield a value of type
Tcon
Int.
Right. But then the
41 matches
Mail list logo
