[Haskell-cafe] Re: Laws and partial values

[Daniel Fischer]

Am Samstag, 24. Januar 2009 21:12 schrieb 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 ().

It's obvious because () is a defined value, while bottom is not - per 
definitionem.
The matter is that besides the elements declared in the datatype definition, 
every Haskell type also contains bottom.

>
> > , 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?

Section 4.2.1 of the report
http://haskell.org/onlinereport/decls.html#sect4.2
>
> >    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