On Fri, Mar 26, 2010 at 11:07 AM, Edward Kmett wrote:

On Fri, Mar 26, 2010 at 11:04 AM, Edward Kmett wrote:

...

-- as long as you're ignoring 'seq' terminateSeq :: a -> Unit terminateSeq a = a `seq` unit

Er ignore that language about seq. a `seq` unit is either another bottom or undefined, so there remains one canonical morphism even in the presence of seq (ignoring unsafePerformIO) =)

It all depends on how you define equality for functions. If you mean indistinguishable in contexts which may involve seq, then there are at least two values of type Unit -> (). foo :: (Unit -> ()) -> () foo x = x `seq` () foo terminate = () foo undefined = undefined Even this uses the convention that undefined = error "whatever" = loop, which isn't technically true, since you can use exception handling to write code which treats them differently. -- Dave Menendez http://www.eyrie.org/~zednenem/

Edward Kmett wrote:

Of course, you can argue that we already look at products and coproducts through fuzzy lenses that don't see the extra bottom, and that it is close enough to view () as Unit and Unit as Void, or go so far as to unify Unit and Void, even though one is always inhabited and the other should never be.

The alternative is to use _consistently_ "fuzzy lenses" and not consider bottom to be a value. I call this the "bottomless" interpretation. I prefer it, because it's easier to reason about. In the bottomless interpretation, laws for Functor, Monad etc. work. Many widely-accepted instances of these classes fail these laws when bottom is considered a value. Even reflexivity of Eq fails. Bear in mind bottom includes non-termination. For instance: x :: Integer x = x + 1 data Nothing n :: Nothing n = seq x undefined x is bottom, since calculation of it doesn't terminate, but one cannot write a program even in IO to determine that x is bottom. And if Nothing is inhabited with a value, does n have that value? Or does the calculation to find which value n is not terminate, so n never gets a value? I avoid explicit "undefined" in my programs, and also hopefully non-termination. Then the bottomless interpretation becomes useful, for instance, to consider Nothing as an initial object of Hask particularly when using GADTs. I also dislike "Void" for a type declared empty, since it reminds me of the C/C++/C#/Java return type "void". In those languages, a function of return type "void" may either terminate or not, exactly like Haskell's "()". -- Ashley Yakeley

wagnerdm@seas.upenn.edu wrote:

Forgive me if this is stupid--I'm something of a category theory newbie--but I don't see that Hask necessarily has an initial object in the bottomless interpretation. Suppose I write

data Nothing2

Then if I understand this correctly, for Nothing to be an initial object, there would have to be a function f :: Nothing -> Nothing2, which seems hard without bottom.

This is a difference between Hask and Set, I guess: we can't write down the "empty function".

Right. It's an unfortunate limitation of the Haskell language that one cannot AFAIK write this: f :: Nothing -> Nothing2; f n = case n of { }; However, one can work around it with this function: never :: Nothing -> a never n = seq n undefined; Of course, this workaround uses undefined, but at least "never" has the property that it doesn't return bottom unless it is passed bottom. -- Ashley Yakeley

Getting back to the question, whatever happened to empty case expressions? We should not need bottom to write total functions from empty types. Correspondingly, we should have that the map from an empty type to another given type is unique extensionally, although it may have many implementations. Wouldn't that make any empty type initial? Of course, one does need one's isogoggles on to see the uniqueness of the initial object. An empty type is remarkably useful, e.g. as the type of free variables in closed terms, or as the value component of the monadic type of a server process. If we need bottom to achieve vacuous satisfaction, something is a touch amiss. Cheers Conor On 30 Mar 2010, at 22:02, Edward Kmett wrote:

The uniqueness of the definition of Nothing only holds up to isomorphism.

This holds for many unique types, products, sums, etc. are all subject to this multiplicity of definition when looked at through the concrete-minded eye of the computer scientist.

The mathematician on the other hand can put on his fuzzy goggles and just say that they are all the same up to isomorphism. =)

-Edward Kmett

On Tue, Mar 30, 2010 at 3:45 PM, wrote: Quoting Ashley Yakeley :

data Nothing

I avoid explicit "undefined" in my programs, and also hopefully non- termination. Then the bottomless interpretation becomes useful, for instance, to consider Nothing as an initial object of Hask particularly when using GADTs.

Forgive me if this is stupid--I'm something of a category theory newbie--but I don't see that Hask necessarily has an initial object in the bottomless interpretation. Suppose I write

data Nothing2

Then if I understand this correctly, for Nothing to be an initial object, there would have to be a function f :: Nothing -> Nothing2, which seems hard without bottom. This is a difference between Hask and Set, I guess: we can't write down the "empty function". (I suppose unsafeCoerce might have that type, but surely if you're throwing out undefined you're throwing out the more frightening things, too...)

~d

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

I believe I was claiming that, in the absence of undefined, Nothing and Nothing2 *aren't* isomorphic (in the CT sense). But this is straying dangerously far from Ashley's point, which I think is a perfectly good one: Hask without bottom is friendlier than Hask with bottom. ~d Quoting Edward Kmett :

The uniqueness of the definition of Nothing only holds up to isomorphism.

This holds for many unique types, products, sums, etc. are all subject to this multiplicity of definition when looked at through the concrete-minded eye of the computer scientist.

The mathematician on the other hand can put on his fuzzy goggles and just say that they are all the same up to isomorphism. =)

-Edward Kmett

On Tue, Mar 30, 2010 at 3:45 PM, wrote:

...

Quoting Ashley Yakeley :

data Nothing

...

I avoid explicit "undefined" in my programs, and also hopefully non-termination. Then the bottomless interpretation becomes useful, for instance, to consider Nothing as an initial object of Hask particularly when using GADTs.

Forgive me if this is stupid--I'm something of a category theory newbie--but I don't see that Hask necessarily has an initial object in the bottomless interpretation. Suppose I write

data Nothing2

Then if I understand this correctly, for Nothing to be an initial object, there would have to be a function f :: Nothing -> Nothing2, which seems hard without bottom. This is a difference between Hask and Set, I guess: we can't write down the "empty function". (I suppose unsafeCoerce might have that type, but surely if you're throwing out undefined you're throwing out the more frightening things, too...)

~d

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Of course Haskell' should have an empty case. As soon as empty data declarations are allowed then empty case must be allowed just by using common sense. On Tue, Mar 30, 2010 at 11:03 PM, Ashley Yakeley wrote:

wagnerdm@seas.upenn.edu wrote:

...

I believe I was claiming that, in the absence of undefined, Nothing and Nothing2 *aren't* isomorphic (in the CT sense).

Well, this is only due to Haskell's difficulty with empty case expressions. If that were fixed, they would be isomorphic even without undefined.

-- Ashley Yakeley _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Tuesday 30 March 2010 4:34:10 pm Ashley Yakeley wrote:

Worse than that, if bottom is a value, then Hask is not a category! Note that while undefined is bottom, (id . undefined) and (undefined . id) are not.

Hask can be a category even if bottom is a value, with slight modification. That specific problem can be overcome by eliminating seq (and associated stuff; strict fields, bang patterns, ...), because it is the only thing in the language that can distinguish between the extensionally equal: undefined \_ -> undefined the latter being what you get from id . undefined and undefined . id. Bottom, or more specifically, lifted types, tend to ruin other nice categorical constructions, though. Lifted sums are not Hask coproducts, lifted products are not Hask products, the "empty" type is terminal, rather than initial, and () isn't terminal. But, if we ignore bottoms, these deficiencies disappear. See, of course, Fast and Loose Reasoning is Morally Correct. * -- Dan [*] http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf