[Haskell-cafe] Re: Laws and partial values

[David Menendez]

On Sat, Jan 24, 2009 at 4:31 PM, Thomas Davie <tom.davie at gmail.com> wrote:
>
> On 24 Jan 2009, at 22:19, Henning Thielemann wrote:
>
>>
>> On Sat, 24 Jan 2009, Thomas Davie wrote:
>>
>>> On 24 Jan 2009, at 21:31, Dan Doel wrote:
>>>
>>>> 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.
>>
>> Zero- and one-constructor data types would then significantly differ from
>> two- and more-constructor data types, wouldn't they?
>
> Yes, they would, but not in any way that's defined, or written in, the fact
> that they have a nice property of being able to tell something about what
> bottom looks like is rather nice actually.

It sounds like you're suggesting that all pattern matching on
single-constructor data types should be irrefutable. In other words,
"\(x,y) -> ..." would be equivalent to "\ ~(x,y) -> ...".

I'm pretty sure this would cause problems if suddenly introduced in
Haskell, but it might work in a new language.

How would this work with seq? If (_|_,_|_) = _|_, does (_|_,_|_) `seq`
() = _|_ ?

-- 
Dave Menendez <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>