[Haskell-cafe] Learn You a Haskell for Great Good - a few doubts

[wren ng thornton]

On 3/4/11 4:33 PM, Alexander Solla wrote:
> On Thu, Mar 3, 2011 at 10:14 PM, wren ng thornton<wren at freegeek.org>  wrote:
>> On 3/3/11 2:58 AM, Antti-Juhani Kaijanaho wrote:
>>> On Thu, Mar 03, 2011 at 12:29:44PM +0530, Karthick Gururaj wrote:
>>>
>>>> Thanks - is this the same "unit" that accompanies IO in "IO ()" ? In
>>>> any case, my question is answered since it is not a tuple.
>>>>
>>>
>>> It can be viewed as the trivial 0-tuple.
>>>
>>
>> Except that this is problematic since Haskell doesn't have 1-tuples (which
>> would be distinct from plain values in that they have an extra bottom).
>>
>>
> I don't get this line of thought.  I understand what you're saying, but why
> even bother trying to distinguish between bottoms when they can't be
> compared by equality, or even computed?

If we have,

    data OneTuple a = One a

Then

     _|_ /= One _|_

This can be detected by seq: the left-hand side doesn't terminate, 
whereas the right-hand side does. And moreover, this can mess up other 
things (e.g., monads) by introducing too much laziness. Space leaks are 
quite a serious matter and they have nothing to do with trying to 
compare uncomputable values. Do you want a seemingly insignificant 
refactoring to cause your program to suddenly hang forever? Or to take 
up gobs more space than it used to?

This is very similar to the problems that people run into because,

     _|_ /= (\x -> _|_)


> The type (forall a . a) doesn't contain any values!

Nope, it contains one. Just ask any proof theorist, or anyone who uses 
witnesses to capture information in the type system.


> If you choose to interpret all bottoms as being the same non-existent,
> unquantifiable (in the language of Haskell) "proto-value", you get the
> isomorphism between types a and (a), as types.

Nope, because we have

     notBottom :: OneTuple a -> Bool
     notBottom x = x `seq` True

whereas

     isBottom :: a -> Bool
     isBottom x = x `seq` True


> Indeed, those are the
> semantics in use by the language.  A value written (a) is interpreted as a.
>   A type written (a) is interpreted as a.

That's a syntactic matter. Those are parentheses of grouping, not 
parentheses of tuple construction. For example, you can say:

     (,) a b

or

     (,,) a b c

But you can't say

     () a

>> In an idealized world, yes, unit can be thought of as the nullary product
>> which serves as left- and right-identity for the product bifunctor.
>> Unfortunately, Haskell's tuples aren't quite products.[1]
>
> I'm not seeing this either.  (A,B) is certainly the Cartesian product of A
> and B.  In what sense are you using "product" here? Is your complaint a
> continuation of your previous (implicit) line of thought regarding distinct
> bottoms?

It is not the case that for every pair, ab, we have that:

     ab == (fst ab, snd ab)

Why? Well consider ab = undefined:

     _|_ /= (_|_,_|_)

I'm using "product" in the category theoretic sense, which is the sense 
in which it applies to Compact Closed Categories (i.e., the models of 
lambda calculi). Though it also works in the domain theoretic sense 
(i.e., how people reason about laziness), since Haskell's tuples are 
neither domain products nor smash products.

-- 
Live well,
~wren