[Haskell-cafe] Re: Laws and partial values

[Thomas Davie]

On 24 Jan 2009, at 21:31, Dan Doel wrote:

> On Saturday 24 January 2009 3:12:30 pm Thomas Davie wrote:
>> 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 ().
>
> For integers, is _|_ equal to 0? 1? 2? ...
Hypothetically (as it's already been pointed out that this is not the  
case in Haskell), _|_ in the integers would not be known, until it  
became more defined.  I'm coming at this from the point of view that  
bottom would contain all the information we could possibly know about  
a value  while still being the least value in the set.

In such a scheme, bottom for Unit would be (), as we always know that  
the value in that type is (); bottom for pairs would be (_|_, _|_), as  
all pairs look like that (this incidentally would allow fmap and  
second to be equal on pairs); bottom for integers would contain no  
information, etc.

>>> , 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?
>
> From the report: "Since Haskell is a non-strict language, all  
> Haskell types
> include _|_."
>
> http://www.haskell.org/onlinereport/exps.html#basic-errors
>
> Although some languages probably have the semantics you're thinking  
> of (Agda,
> for instance, although you can write non-terminating computations  
> and it will
> merely flag it in red, currently), Haskell does not.

Yep, indeed.

Bob