[Haskell-cafe] Where is the "convergence point" between Category Theory and Haskell?

[wren ng thornton]

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