Re: [Haskell-cafe] type metaphysics

[Dan Doel]

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 computable, however, as discussed elsewhere.

This is all correct, except that exponentials are just part of algebraic data 
types, not generalized algebraic data types. Generalized algebraic data types 
are similar to inductive families, in that you can target constructors at 
specific type-indices, like so:

  data T t where
I :: T Int
P :: T a -> T b -> T (a,b)

Both of those are genuine GADT constructors. There's also things like:

E :: T a -> T b -> T b

But those are doable by 'mere' ADTs plus existential quantification:

  data T b = ... | forall a. P (T a) (T b)

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

Re: [Haskell-cafe] type metaphysics

[wren ng thornton]

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Gregg Reynolds]

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?
Since we can define "aleph" constructors, each of which can yield "aleph"
values, well that's a lot of values.)


>
> >> 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.
>
> I don't see why you would consider it the same type.  Since, given any
> two data types, I could remove all the data constructors, this would
> make them, and by extension, all types the same, wouldn't it?
>

I don't think so; considered as sets, they have different intensions, and
considered as predicates, they're clearly distinct even if there are no
objects.  Different names (descriptions), different things, unless we
declare they are equal.

You would probably find "When is one thing equal to another thing", by Barry
Mazur (at 
http://www.math.harvard.edu/~mazur/).
A fascinating discussion of equality in the context of category theory.  See
also "On Sense and Intension" at http://consc.net/papers.html

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

Re: [Haskell-cafe] type metaphysics

[Eugene Kirpichov]

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
>
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[wren ng thornton]

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 "really" is.
 For example, definitions of the typed lambda calculus usually define
some type symbols and rules like "a : T means a is of type T", and
then reasoning ensues without discussion of what "type" means.


The non-explication of types is intentional: by not saying anything 
about what a type is (other than that values/expressions can have one) 
that frees the theory to operate generally, regardless of what types 
actually are in any specific instantiation. When trying to say as little 
as possible, people frequently refer to them as "sorts". By calling them 
"types" we often mean we know a little bit more about them than sorts; 
though the terminology is relatively interchangeable.


Not that this helps you any.



The only discussion I've found that addresses this is at the Stanford
Encyclopedia of Philosophy, article "Types and Tokens" [1].  It's all
very philosophical, but there is one point there that I think has
relevance to Haskell.  It's in section 4.1, discussing the distinction
between types and sets:


The type--token distinction uses a different notion of type. In this 
context "type" means a sort of platonic notion of some thing (a value 
idealized), whereas "tokens" are specific instantiations/references to 
that thing. Consider, for example, the English word "Foo". When 
discussing Foo generally as a word in the English language, we're 
discussing the type Foo. But if I'm doing natural language parsing on 
this email, each time that three-letter sequence occurs is a different 
token (or instance, or use-in-context) of the type. In NLP/MT the 
distinction is helpful because, due to context, different tokens of the 
same type may need different treatment even though they're "the same 
word". For example, if "the" occurs fifteen times in a sentence, we 
probably shouldn't translate all of them into a single occurence of 
"der" in the German translation.


Mathematically this is the same distinction between the idea of 1 
(choose any particular idea), vs the usage of 1. Due to referential 
transparency we don't tend to worry about this in Haskell since all 
tokens are interchangeable. Consider instead an object-oriented 
language. We can have an object over here that is "1", and it's separate 
from an object over there that's also "1". We can have mutation which 
makes one of the tokens different, say "2", without affecting the other 
token (though now they are no longer tokens of the same type). This is 
different from making the *type* different, which would affect all its 
tokens.


(And philosophically it matters because of the relation to whether the 
presence or absence of a token is effectful on the definitions of other 
things, e.g. sets or species as in your citation.)


Obviously this has some relation to the programmatic theory of types, 
but it's indirect. In the NLP/MT context the mapping from tokens to 
types is fairly straightforward, but in general there's the question of 
how we do the mapping which depends entirely on what our types look 
like. For example, is "Fooing" or "Fooer" a token of Foo, or do there 
exist types Fooing and Fooer instead? Usually in programming, singleton 
types aren't too helpful and so we use types that include all the 
"inflected forms" as well. But there are times when we do want to break 
these types apart into smaller types (via OOP inheritance, via case 
matching, via distinguishing instances of the same value,...).


--
Live well,
~wren
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Dan Piponi]

On Mon, Feb 2, 2009 at 3:18 PM, Reid Barton  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.
--
Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[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

Re: [Haskell-cafe] type metaphysics

[Luke Palmer]

On Mon, Feb 2, 2009 at 4:23 PM, Matthew Brecknell wrote:

> 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 argument; it is why there are countable
sets which are computably uncountable:  (nonconstructive) mathematics does
not need to decide, only programs need to do that :-)

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

Re: [Haskell-cafe] type metaphysics

[Matthew Brecknell]

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
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Reid Barton]

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Luke Palmer]

On Mon, Feb 2, 2009 at 3:41 PM, 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


Presumably under the condition that a /= b.

It's unlikely that you can.  At least you can't use Escardo's trick, because
while the space of pairs of cantor spaces (cantor space = Nat -> Bool) is
compact, the space of pairs of *different* cantors spaces is not.  This is
witnessed by the following function:

f (a,b) = length (takeWhile id (zipWith (==) a b))

This function finds the first index at which they differ.  Since they are
guaranteed to be different, this function is total.  Thus, if the space of
nonequal cantor spaces were compact, then so too would be Nat, which we know
is not the case.

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

Re: [Haskell-cafe] type metaphysics

[Joachim Breitner]

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


signature.asc
Description: Dies ist ein digital signierter Nachrichtenteil
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[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.)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Ryan Ingram]

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




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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Joachim Breitner]

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


signature.asc
Description: Dies ist ein digital signierter Nachrichtenteil
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Luke Palmer]

2009/2/2 Joachim Breitner 

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


What argument?  What was I trying to prove?

But I admit that my notation is confusing; I am not distinguishing between
Haskell types and their denotations.  I'll be more precise:

I will use N for the set of naturals, Nat for the Haskell type of (strict)
naturals, 2 for the set {0,1}, Bool for the Haskell type True|False, (->)
for a mathematical function, (~>) for a *total* computable function in
Haskell.

N -> 2  is uncountable, meaning there is no surjection N -> (N -> 2).

Nat ~> Bool is countable, meaning there is a surjection N -> (Nat ~> Bool).
Enumerate all program source codes (which is countable, so N -> SourceCode),
and pick out the ones which denote a total computable function Nat ~> Bool.

But Nat ~> Bool is *computably* uncountable, meaning there is no injective
function Nat ~> (Nat ~> Bool), by the diagonal argument above.

That's what I meant.

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

Re: [Haskell-cafe] type metaphysics

[Richard O'Keefe]

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?

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

Re: [Haskell-cafe] type metaphysics

[David Menendez]

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 

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

Re: [Haskell-cafe] type metaphysics

[Ketil Malde]

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? 

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

I don't see why you would consider it the same type.  Since, given any
two data types, I could remove all the data constructors, this would
make them, and by extension, all types the same, wouldn't it?

-k
-- 
If I haven't seen further, it is by standing in the footprints of giants
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Jonathan Cast]

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


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

Re: [Haskell-cafe] type metaphysics

[Joachim Breitner]

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


signature.asc
Description: Dies ist ein digital signierter Nachrichtenteil
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Gregg Reynolds]

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Gregg Reynolds]

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Ketil Malde]

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?

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

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

-k
-- 
If I haven't seen further, it is by standing in the footprints of giants
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Daniel van den Eijkel]

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 = 
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
  
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Daniel van den Eijkel]

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 = 
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

Re: [Haskell-cafe] type metaphysics

[Luke Palmer]

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


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

In summary, the set of total computable functions Nat -> Bool is a countable
set, but this fact is not observable by any algorithm.  (so is it
*really*countable after all? :-)

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

Re: [Haskell-cafe] type metaphysics

[Lennart Augustsson]

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 = 
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

Re: [Haskell-cafe] type metaphysics

[Lennart Augustsson]

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?

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.

There's a natural ordering of the elements {False,True,_|_}.  The _|_
is less than False and less than True, whereas False and True are
unordered with respect to each other.  Think of this ordering as how
much information you get.  Non-termination is less information than a
definite False or True.
Domain theory deals with this kind of ordered sets.

  -- Lennart

On Mon, Feb 2, 2009 at 4:51 PM, Gregg Reynolds  wrote:
> 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
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Dan Piponi]

On Mon, Feb 2, 2009 at 8:09 AM, Gregg Reynolds  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 functions in set theory - ie. set(A -> B) =
set(B)^set(A). But if you don't insist on such a constraint there's no
problem with sets.
--
Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Gregg Reynolds]

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Martijn van Steenbergen]

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

Re: [Haskell-cafe] type metaphysics

[Lennart Augustsson]

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 :
> Hi Martijn,
>
> On Mon, Feb 2, 2009 at 9:49 AM, Martijn van Steenbergen
>  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

Re: [Haskell-cafe] type metaphysics

[Krzysztof Skrzętnicki]

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, Gregg Reynolds  wrote:

> 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
> ___
> 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

Re: [Haskell-cafe] type metaphysics

[Lennart Augustsson]

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
>>
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Lennart Augustsson]

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
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Gregg Reynolds]

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

Re: [Haskell-cafe] type metaphysics

[Gregg Reynolds]

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Lutz Donnerhacke]

* 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
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Andrew Butterfield]

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)

--

Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Foundations and Methods Research Group Director.
School of Computer Science and Statistics,
Room F.13, O'Reilly Institute, Trinity College, University of Dublin
   http://www.cs.tcd.ie/Andrew.Butterfield/


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

Re: [Haskell-cafe] type metaphysics

[Martijn van Steenbergen]

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

[Haskell-cafe] type metaphysics

[Gregg Reynolds]

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 "really" is.
 For example, definitions of the typed lambda calculus usually define
some type symbols and rules like "a : T means a is of type T", and
then reasoning ensues without discussion of what "type" means.

The only discussion I've found that addresses this is at the Stanford
Encyclopedia of Philosophy, article "Types and Tokens" [1].  It's all
very philosophical, but there is one point there that I think has
relevance to Haskell.  It's in section 4.1, discussing the distinction
between types and sets:

"Another closely related problem also stems from the fact that sets,
or classes, are defined extensionally, in terms of their members. The
set of natural numbers without the number 17 is a distinct set from
the set of natural numbers. One way to put this is that classes have
their members essentially. Not so the species homo sapiens, the word
'the', nor Beethoven's Symphony No. 9. The set of specimens of homo
sapiens without George W. Bush is a different set from the set of
specimens of homo sapiens with him, but the species would be the same
even if George W. Bush did not exist. That is, it is false that had
George W. Bush never existed, the species homo sapiens would not have
existed. The same species might have had different members; it does
not depend for its existence on the existence of all its members as
sets do."

So it appears that one can think of a type as a predicate; any token
(value?) that satisfies the predicate is a token (member?) of that
type.

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.  My hunch is that it /cannot/ be a set, although I'm
not mathematician enough to prove it.  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).  To my naive mind this sounds
suspiciously like the set of all sets, so it's too big to be a set.
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
suspect this leads to DeepThink about classical v. constructivist
mathematics, but that's a subject for a different discussion.)

I'm not sure that works technically, but it seems kinda cool.  My
question for the list:  is the collection of e.g. Tcon Int values a
set, or not?  If it is, how big is it?

Thanks,

gregg

[1] http://plato.stanford.edu/entries/types-tokens/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe