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

[Alexander Solla]

On Sat, Mar 5, 2011 at 5:06 AM, wren ng thornton <wren at freegeek.org> wrote:

> 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 _|_
>
>
That is vacuously true.  I will demonstrate the source of the contradiction
later.  But you also have "_|_ == One _|_", by evaluation:

> Just undefined
Just *** Exception: Prelude.undefined



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

'seq' is not a "function", since it breaks referential transparency and
possibly extensionality in function composition.  By construction, "seq a b
= b", and yet "seq undefined b /= b".  Admittedly, the Haskell report and
the GHC implementation, diverge on this issue.  Haskell98 specifically
defines seq in terms of a comparison with bottom, whereas GHC "merely"
reduces the first argument to WHNF.  In any case, the reduction is a side
effect, with which can lead to inconsistent semantics if 'seq' is included
in "the language".

It is nice to know that we can work in a consistent language if we avoid
certain constructs, such as 'seq', 'unsafePerformIO', and probably others.
 In addition to making the "core language" conceptually simpler, it means
that we can be sure we aren't inadvertently destroying the correctness
guarantees introduced by the Howard-Curry correspondence theorem.


>
> Nope, it contains one. Just ask any proof theorist, or anyone who uses
> witnesses to capture information in the type system.
>
>
I have studied enough proof theory, model theory, and lattice theory to know
that there is room for both positions.  Just because you /can/ lift a
lattice into one with bottom, it doesn't mean you /should/, if it means
losing conceptual clarity.  In particular, I don't see why you want to
generate an algebra of special cases that add no expressiveness, and include
them in "the language", when you can use a quotient construction to remove
them from the language.  As a practical matter, 'seq' is necessary.  But it
should be treated as a special case (like unsafePerformIO), because it IS
one.

Also, there is no need for a set to contain an element for it to be named or
quantified over.  The empty set can be a witness just as well as a singleton
set.  EmptyDataDecls works just as well whether you interpret (undefined ::
Blah) to mean "a Blah that is not defined" or "a Blah that is the value
'undefined'".  Indeed, the latter is paradoxical.  'undefined = undefined'
type checks, but it is not well-founded -- which is exactly why it is not
defined!  'undefined' is not a value.   It is the name for a thing which
cannot be evaluated.  We happen to know that there are a lot of things which
cannot be evaluated, but the quotient construction treats them all the same.
 (There is the practical issue of GHC handling Prelude.undefined differently
than the other bottoms.  But I won't complain about that ;0)


>  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
>
>
seq is not a function, and is removed from consideration by the quotient
construction I have mentioned, specifically because of how it behaves on
bottom and the fact that the Haskell98 report defines it in terms of
comparing values to bottom, an operation which is known to be impossible.
 notBottom and isBottom are also not functions, for the same reason.


>
>

>  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


Does it matter?  We give syntax its semantics by interpreting it. The only
reason we can say [] a  or (,) a is because they were included as special
cases, for syntactic sugar.  As a matter of fact, it is entirely unnecessary
to be able to introduce the machinery to express the type '(a)', because we
can just express the isomorphic type '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:
>
>    _|_ /= (_|_,_|_)
>

> (undefined, undefined)
(*** Exception: Prelude.undefined

That is as close to Haskell-equality as you can get for a proto-value that
does not have an Eq instance.  As a consequence of referential transparency,
evaluation induces an equivalence relation.  This implies that (_|_, _|_) =
_|_ = (_|_, _|_).

I value referential transparency, and so reject constructs which violate it.


Please demonstrate a proof that _|_ /= (_|_, _|_), so that I can exclude the
unsound constructs you will undoubtedly have to use from my interpretation
of "the language".  I am more interested in finding the consistent fragment
of what you call Haskell than defending what I call Haskell.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110307/a95a40aa/attachment.htm>