# [Haskell-cafe] Re: Laws and partial values

Thomas Davie tom.davie at gmail.com
Sat Jan 24 16:11:38 EST 2009

```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
> include _|_."
>
>
> 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

```