[Haskell-cafe] type metaphysics

[Luke Palmer]

2009/2/2 Joachim Breitner <mail at joachim-breitner.de>

> Hi,
>
> Am Montag, den 02.02.2009, 11:06 -0700 schrieb Luke Palmer:
>
> > That question has kind of a crazy answer.
> >
> > In mathematics, Nat -> Bool is uncountable, i.e. there is no function
> > Nat -> (Nat -> Bool) which has every function in its range.
> >
> > 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090202/f656bd2f/attachment.htm