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
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
Quoting Ashley Yakeley ash...@semantic.org:
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.
Ashley Yakeley wrote:
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
wagne...@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
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
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
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
wagne...@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
On Tue, Mar 30, 2010 at 11:26:39PM +0100, Conor McBride wrote:
Getting back to the question, whatever happened to empty case expressions? We
should not need bottom to write total functions from empty types.
Empty types? Toto, I've a feeling we're not in Haskell anymore.
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 ash...@semantic.org wrote:
wagne...@seas.upenn.edu wrote:
I believe I was claiming that, in
Hmm. What are benefits of data-category over category-extras?
Regards
signature.asc
Description: This is a digitally signed message part
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Mainly that category-extras doesn't have restricted categories, so most of the
categories in data-category cannot be defined with category-extras. This also
means that in category-extras many constructions are built from the ground up,
instead of being built with a few basic building blocks,
13 matches
Mail list logo
