[Haskell-cafe] Re: Laws and partial values

Conal Elliott conal at conal.net
Sat Jan 24 18:55:51 EST 2009


>
> It's obvious because () is a defined value, while bottom is not - per
> definitionem.
>

I wonder if this argument is circular.

I'm not aware of "defined" and "not defined" as more than informal terms.

Which definition(s) are you referring to?

  - Conal

On Sat, Jan 24, 2009 at 12:31 PM, Daniel Fischer
<daniel.is.fischer at web.de>wrote:

> 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
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090124/7e996e19/attachment.htm


More information about the Haskell-Cafe mailing list