[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: mail at joachim-breitner.de | ICQ# 74513189 | GPG-Key: 4743206C
  JID: nomeata at joachim-breitner.de | http://www.joachim-breitner.de/
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 197 bytes
Desc: Dies ist ein digital signierter Nachrichtenteil
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20090202/19bf7473/attachment.bin