[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 = <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
> <martijn at 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?
>>
>> Martijn.
>>
>>     
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>   
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090202/ec937f17/attachment.htm