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

On Sat, Mar 5, 2011 at 5:06 AM, wren ng thornton wrote:

On 3/4/11 4:33 PM, Alexander Solla wrote:

...

On Thu, Mar 3, 2011 at 10:14 PM, wren ng thornton 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.