[Haskell-cafe] Learn You a Haskell for Great Good - a few doubts
wren ng thornton
wren at freegeek.org
Sat Mar 5 14:06:38 CET 2011
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
_|_ /= 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
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
(,,) a b c
But you can't say
>> 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.
> 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
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.
More information about the Haskell-Cafe