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