On 1/13/13 12:44 PM, Alexander Solla wrote:
Hask is a very rich category, and is suitable for encoding a lot (but not
all) of category theory. As far as I know, the actual boundary is as yet
unknown.
I'm not sure that's the most appropriate way to render things. In
general, rich categories like CCCs and Toposes are "good places" to do
mathematics. This means that we can translate the bulk of mathematics
into those settings--- where mathematics means the study of particular
structures like rings, groups, vector spaces, etc. These rich categories
also provide a good place to do logic/lambda-calculi; from which we get
the idea of categorifying Haskell and seeing where that leads us (i.e.,
asking what Hask looks like).
However, standard category theory does not provide a good place for
doing category theory. In order to provide a good place for doing
category theory, people move on to enriched CT and higher CT[1]. HCT is
about coming up with category theoretic definitions for things like
co/limits, adjunctions, etc, while moving away from the set theoretic
notions inherited from the original conceptions of these terms. In other
words, HCT is a good place for doing *meta*mathematics (and metalogic).
While there are apparent similarities, there are big differences between
doing mathematics and doing metamathematics, and one should be careful
not to get them confused. Asking what Haskell looks like when viewed
from CT is very different than asking what portions of CT we can
implement in Haskell. Haskell is a great place for doing mathematics,
but I'm wary of how good it is for doing metamathematics; we conflate
too many things which should be kept distinct (e.g., morphisms vs
exponentials) and we fail to monitor the boundary between object and
meta languages (e.g., a morphism in a category vs a mapping as described
in the language of category theory).
[1] For more discussion on this point, see n-Lab and n-Cafe:
http://ncatlab.org/
http://golem.ph.utexas.edu/category/
--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
