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 > <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 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/ > _______________________________________________ > 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