[Haskell-cafe] Re: Laws and partial values

[Thomas Davie]

On 24 Jan 2009, at 20:28, Jake McArthur wrote:

> Thomas Davie wrote:
>> But, as there is only one value in the Unit type, all values we  
>> have no information about must surely be that value
>
> The flaw in your logic is your assumption that the Unit type has  
> only one value. Consider
>
>    bottom :: ()
>    bottom = undefined
>
> Oviously, bottom is not ()
Why is this obvious – I would argue that it's "obvious" that bottom  
*is* () – the data type definition says there's only one value in the  
type.  Any value that I haven't defined yet must be in the set, and  
it's a single element set, so it *must* be ().

> , but its type, nonetheless, is Unit. Unit actually has both () and  
> _|_. More generally, _|_ inhabits every Haskell type, even types  
> with no constructors (which itself requires a GHC extension, of  
> course):

Does it?  Do you have a document that defines Haskell types that way?

>    data Empty
>
>    bottom' :: Empty
>    bottom' = undefined
>
> If you only ever use total functions then you can get away with not  
> accounting for _|_. Perhaps ironically a function that doesn't  
> account for _|_ may be viewed philosophically as a partial function  
> since its contract doesn't accommodate all possible values.

Now that one is interesting, I would argue that this is a potential  
flaw in the type extension – values in the set defined here do not  
exist, that's what the data definition says.

Bob