On Mon, Feb 2, 2009 at 10:05 AM, Andrew Butterfield 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 uncountable sets. See also:

http://en.wikipedia.org/wiki/Countable_set

No - it's even bigger than those !

He is thinking of proper classes, not sets.

http://en.wikipedia.org/wiki/Class_(set_theory)

Yes, that's my hypothesis: type constructors take us outside of set theory (ZF set theory, at least). I just can't prove it. Thanks, g

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).

Haskell possesses models[1] in which the carriers of all types are countable. Haskell also possesses the models[2] which do assign uncountable carriers to several Haskell types --- a -> b whenever a has an infinite carrier (and b is not a degenerate type of the form newtype B = B B ), [b] under the same conditions on b, etc. In many cases, these are the most insightful models, and I those models are what people mean when they talk about e.g. [Int] having an un-countable denotation. jcc [1] IIUC all models based on recursion theory have this property [2] IIUC most models based on domain theory have this property

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 represented as a sequence of bytes. (Proof: take your source tree, and use tar, pax, cpio, or whatever.) There is therefore a countable infinity of Haskell programs. In Haskell 98, a program can generate at most a countable infinity of types (taking a 'type' here to be an element of the "Herbrand base" generated by the type constructors, speaking somewhat loosely). So surely there can be at most a countable infinity of Haskell types?

Hi Martijn, On Mon, Feb 2, 2009 at 9:49 AM, Martijn van Steenbergen < martijn@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 always thought of types, never having had a good reason to think otherwise. But it seems it doesn't work - type theory goes beyond set theory. I've even found an online book[1] that uses type theory to construct set theory! At least I think that's what it does (not that I understand it.)

...

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". The tokens/values of Tcon Int may or may not constitute a set, but even if they, we have no way of describing the set's extension.

Int has 2^32 values, just like in Java. You can verify this in GHCi:

Ok, but that's an implementation detail. My question is what is the theoretical basis of types. Notice that the semantics of Haskell's built-in types are a matter of social convention. The symbols used - Int, 0, 1, 2, ... - are well-known, and we agree not to add data constructors. But we could if we wanted to. Say, Foo :: Int -> Int. Then Foo 3 is an Int, distinct from all other Ints; in particular it is not equal to "3". I suspect a full definition of type would have to say something about operations.

...

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:

It could be that values of a constructed type form an uncountably large set, rather than something too big to be a set at all. I'm afraid I don't know how to work with such critters. In any case, the more interesting thing (to me) is the notion that sets contain their members "essentially", but data types don't, as far as I can see. Thanks much, gregg [1] http://www.cs.chalmers.se/Cs/Research/Logic/book/

Hi and thanks for the response, On Mon, Feb 2, 2009 at 10:32 AM, Lennart Augustsson wrote:

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, ...}

I'm afraid I haven't yet wrapped my head around _|_ qua member of a set. In any case, I take it that sets being a reasonable /approximation/ of types means there is a difference. Back to metaphysics: you pointed out that the function space is countable, and Christopher noted that there are countably many strings that could be used to represent a function. So that answers my question about the size of e.g. Tcon Int. But then again, that's only if we're working under the assumption that the "members" of Tcon Int are those we can express with data constructors and no others. If we drop that assumption,then it seems we can't say much of anything about its size. FWIW, what started me on this is the observation that we don't really know anything about constructed types and values except that they are constructed. I.e. we know that "Foo 3" is the image of 3 under Foo, and that's all we know. Any thing else (like operations) we must construct out of stuff we do know (like Ints or Strings.) This might seem trivial, but to me it seems pretty fundamental, since it leads to the realization that we can use one thing (e.g. Ints) to talk about something we know nothing about, which seems to be what category theory is about. (Amateur speaking here.) Thanks, gregg

On Mon, Feb 2, 2009 at 11:51 AM, Lennart Augustsson wrote:

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 thought you wanted to know about Haskell types?

The metaphysics thereof. ;) I want to situate them in the larger intellectual context to get a more precise answer to "what is a type, really?"

There's nothing mysterious about _|_ being a member of a set. Say that you have a function (Int->Bool). What are the possible results when you run this function? You can get False, you can get True, and the function can fail to terminate (I'll include any kind of runtime error in this). So now we want to turn this bit of computing into mathematics, so we say that the result must belong to the set {False,True,_|_} where we've picked the name _|_ for the computation that doesn't terminate. Note that is is mathematics, there's no notion of non-termination here. The function simply maps to one of three values.

I like that, thanks. -gregg

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. Most importantly Haskell functions have to be monotonic (in the domain theoretic sense), so that limits the number of possible functions. http://en.wikipedia.org/wiki/Domain_theory -- Lennart On Mon, Feb 2, 2009 at 4:28 PM, 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 functions space in set theory. Most importantly Haskell functions have to be monotonic (in the domain theoretic sense), so that limits the number of possible functions.

http://en.wikipedia.org/wiki/Domain_theory

-- Lennart

On Mon, Feb 2, 2009 at 3:49 PM, Martijn van Steenbergen wrote:

...

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 makes sense to write: () = { () } Bool = { True, False } Maybe Bool = { Nothing, Just True, Just False }

Recursive data types have an infinite number of values. Almost all types belong to this group. Here's one of the simplest examples:

data Peano = Zero | Suc Peano

There's nothing wrong with a set with an infinite number of members.

Gregg Reynolds wrote:

...

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". The tokens/values of Tcon Int may or may not constitute a set, but even if they, we have no way of describing the set's extension.

Int has 2^32 values, just like in Java. You can verify this in GHCi:

Prelude> (minBound, maxBound) :: (Int, Int) (-2147483648,2147483647)

Integer, on the other hand, represents arbitrarily big integers and therefore has an infinite number of elements.

...

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

Haskell has types which have uncountably many values. They are all functions of the form A -> B, where A is an infinite type (either countably or uncountably).

If a set is countable, you can enumerate the set in such a way that you will reach each member eventually. For Haskell this means that if a type "a" has a countable number of values, you can define a list :: [a] that will contain all of them.

I hope this helps! Let us know if you have any other questions.

Martijn.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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 all mathematical functions of type (Integer -> Bool), but it does include the ones we usually mean by the type (Integer -> Bool) in Haskell. -- Lennart On Mon, Feb 2, 2009 at 4:47 PM, Martijn van Steenbergen 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 function space? :) The explanation is that the Haskell function space is not the same as the functions space in set theory. Most importantly Haskell functions have to be monotonic (in the domain theoretic sense), so that limits the number of possible functions.

I was thinking about a fixed function type A -> B having uncountably many *values* (i.e. implementations). Not about the number of function types of the form A -> B. Is that what you meant?

For example, fix the type to Integer -> Bool. I can't enumeratate all possible implementations of this function. Right?

Martijn.

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 n = do c <- chars s <- string (n-1) return (c:s)

mkfun n = do s <- string n return ("f :: Integer -> Bool; f = " ++ s)

test fundef = do system ("del test.exe") writeFile "test.hs" (fundef ++ "; main = return ()") system ("ghc --make test.hs") b <- doesFileExist "test.exe" if b then putStrLn fundef else return ()

main = do let fundefs = [0..] >>= mkfun mapM_ test $ drop 1000 fundefs

Lennart Augustsson schrieb:

...

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 all mathematical functions of type (Integer -> Bool), but it does include the ones we usually mean by the type (Integer -> Bool) in Haskell.

-- Lennart

On Mon, Feb 2, 2009 at 4:47 PM, Martijn van Steenbergen 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 function space? :) The explanation is that the Haskell function space is not the same as the functions space in set theory. Most importantly Haskell functions have to be monotonic (in the domain theoretic sense), so that limits the number of possible functions.

I was thinking about a fixed function type A -> B having uncountably many *values* (i.e. implementations). Not about the number of function types of the form A -> B. Is that what you meant?

For example, fix the type to Integer -> Bool. I can't enumeratate all possible implementations of this function. Right?

Martijn.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

------------------------------------------------------------------------

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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, so we can just enumerate all implementations. So the computable functions Nat -> Bool are countable.

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".

That argument has a flaw. Just because we have a function in the mathematical sense that sends ℕ to (Nat -> Bool) does not mean that we have Haskell function f of that type that we can use to construct g. Greetings, Joachim -- Joachim "nomeata" Breitner mail: mail@joachim-breitner.de | ICQ# 74513189 | GPG-Key: 4743206C JID: nomeata@joachim-breitner.de | http://www.joachim-breitner.de/ Debian Developer: nomeata@debian.org

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: mail@joachim-breitner.de | ICQ# 74513189 | GPG-Key: 4743206C JID: nomeata@joachim-breitner.de | http://www.joachim-breitner.de/ Debian Developer: nomeata@debian.org

Hi, Am Montag, den 02.02.2009, 14:41 -0800 schrieb Dan Piponi:

2009/2/2 Luke Palmer :

...

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 Haskell function (Nat -> Bool) -> Nat there'd always be two elements that get mapped to the same value.

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 where (a,b) = toSame f -- Dan

(PS I think this is hard. But my brain might be misfiring so it might be trivial.)

toSame _ = (const True, const True)

;-) Joachim -- Joachim "nomeata" Breitner mail: mail@joachim-breitner.de | ICQ# 74513189 | GPG-Key: 4743206C JID: nomeata@joachim-breitner.de | http://www.joachim-breitner.de/ Debian Developer: nomeata@debian.org

On Mon, Feb 02, 2009 at 02:41:36PM -0800, Dan Piponi wrote:

2009/2/2 Luke Palmer :

...

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 Haskell function (Nat -> Bool) -> Nat there'd always be two elements that get mapped to the same value.

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 where (a,b) = toSame f

(Warning: sketchy argument ahead.) Let f :: (Nat -> Bool) -> Nat be a total function and let g0 = const True. The application f g0 can only evaluate g0 at finitely many values, so f g0 = f (< k) for any k larger than all these values. So we can write

toSame f = (const True, head [ (< k) | k <- [1..], f (const True) == f (< k) ])

and toSame is total on total inputs. Regards, Reid

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 4:18 PM, Reid Barton wrote:

...

...

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 where (a,b) = toSame f

(Warning: sketchy argument ahead.) Let f :: (Nat -> Bool) -> Nat be a total function and let g0 = const True. The application f g0 can only evaluate g0 at finitely many values, so f g0 = f (< k) for any k larger than all these values. So we can write

...

toSame f = (const True, head [ (< k) | k <- [1..], f (const True) == f (< k) ])

and toSame is total on total inputs.

Well done! That's not sketchy at all! There is always such a k (when the result type of f has decidable equality) and it is the "modulus of uniform continuity" of f. This is computable directly, but the implementation you've provided might come up with a smaller one that still works (since you only need to differentiate between const True, not all other streams).

I guess I should hold off on conjecturing the impossibility of things... :-)

Luke

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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?

2009/2/2 Luke Palmer :

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 in the range of f? In particular, f is a program, which I can easily implement; given: compiler :: String -> Maybe (Nat -> Bool) mkAllStrings :: () -> [String] -- enumerates all possible strings I can write f as f n = validPrograms () !! n where validPrograms = map fromJust . filter isJust . map compiler . mkAllStrings Now, in particular, mkAllStrings will generate the following string at some index, call it "stringIndexOfG": <source code for compiler> <source code for mkAllStrings> <source code for f> g n = not (f n n) This is a valid program, so the compiler will compile it successfully, and therefore there is some index "validProgramIndexOfG" less than or equal to "stringIndexOfG" which generates this program. But your argument seems to hold as well, so where is the contradiction? -- ryan

On Mon, Feb 2, 2009 at 3:55 PM, Benedikt Huber wrote:

f is 'easy to implement' if it enumerates all functions, not just total ones. Otherwise, f is hard to implement ;)

In the first case, if we have (f n n) = _|_, then g n = not (f n n) = _|_ as well, so the diagonalization argument does not hold anymore.

Thanks for the insight, I see the contradiction! Luke said:

But we know we are dealing with computable functions, so we can just enumerate all implementations. So the computable functions Nat -> Bool are countable.

The contradiction is this: f, as specified by Luke enumerates all computable functions. But f is uncomputable! So while we can show that the number of computable functions is at most countable (due to the number of programs being countable), we cannot actually enumerate which ones they are. Since f is uncomputable, so is g. Therefore, there is no diagonalization; even if we had a magic oracle that enumerated the set of computable functions, g would not be present, since it is not computable! On the other hand, if we allow f to construct nonterminating functions, as in my implementation, g does not diagonalize, as Benedikt pointed out! -- ryan

On Mon, Feb 2, 2009 at 12:39 PM, Ketil Malde wrote:

Gregg Reynolds 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" is just a predicate. So division by zero is a "type error", since the domain of division is the type of all numbers except zero.

In contrast, I've always thought of (static) types as disjoint sets of values.

...

My reasoning is that we can define an infinite number of data constructors for it, including at least all possible polynomials (by which I mean data constructors of any arity taking args of any type).

I guess I don't quite understand what you mean by "Tcon Int" above. Could you give a concrete example of such a type?

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.

...

To my naive mind this sounds suspiciously like the set of all sets, so it's too big to be a set.

I suspect that since types and values are separate domains, you avoid the complications caused by self reference.

...

In any case, Tcon Int does not depend on any particular constructor, just as homo sapiens does not depend on any particular man. So it can't be a set because it doesn't have its members essentially.

I don't follow this argument. Are you saying you can remove a data constructor from a type, and still have the same type? And because of this, the values of the type do not constitute a set?

Yep. Well, that is /if/ you start from the "Open-World Assumption" - see http://en.wikipedia.org/wiki/Open_World_Assumption (very important in ontologies e.g. OWL and Description Logics). Just because we know that e.g. expressions like Dcon 3 yield values of type Tcon Int does not mean that we know that those are the only such expressions. So we can't really say anything about how big it can be. Who knows, it might actually be a useful distinction for an OWL reasoner in Haskell.

I guess it boils down to how "Tcon Int" does not depend on any particular constructor.

That seems like a good way of putting it. -g

On Mon, Feb 2, 2009 at 3:25 PM, Ketil Malde wrote:

Gregg Reynolds 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?

Only if you're ignoring non-terminating values. Otherwise, you have to deal with the fact that Tcon Int contains _|_ and DCon _|_. -- Dave Menendez http://www.eyrie.org/~zednenem/

Gregg Reynolds wrote:

On Mon, Feb 2, 2009 at 2:25 PM, Ketil Malde wrote:

...

Gregg Reynolds 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?

The values constructed by that particular constructor, yes; good point. Isomorphic, but not the same. (And also, if we have a second constructor, what's our cardinality? The first one "uses up" all the integers, no?

No. If we have the type (Either Integer Integer) we have W+W values. There's a tag to distinguish whether we chose the Left or Right variety of Integer, but having made that choice we still have the choice of any Integer. Thus, this type adds one extra bit to the size of the integers, doubling their cardinality. Which is why ADTs are often called "sum--product types". Replacing products and coproducts with, er, products and summations we can talk about the cardinality of types (ignoring _|_): |()| = 1 |Bool| = 1 + 1 |Maybe N| = 1 + |N| |(N,M)| = |N| * |M| |Either N M| = |N| + |M| etc Really we're just changing the evaluation function for our ADT algebra. 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 computable, however, as discussed elsewhere. -- Live well, ~wren