4 ms·

Author of the blog post here. This is a great overview of internal categories and profunctors. A couple comments 1. I would say the primary application is to p

Author of the blog post here. This is a great overview of internal categories and profunctors. A couple comments 1. I would say the primary application is to proving that certain casts (function cast, etc.) are the primary result of the paper. We basically showed that graduality + extensionality determines almost all of the behavior of casts. 2. Exception handling for type errors is actually in direct conflict with graduality. The reason is that the type error is the least element and every term has to be monotone with respect to the type error, so if you catch a type error, to be monotone you have to show that the result you produce is less dynamic than the result you would have produced if there was no exception. This means that if you want to catch type errors you need to have a fancy catch form, or you need to do it at an "extra-linguistic" level, or you can use modal types (think monads) to say that catching a type error is a "reflective" operation and so any code that does it is uses the reflection modality. Also as a side-note, in my opinion profunctors are an essential component of category theory, and it's really a shame that in intro courses we explain everything in terms of adjunctions, limits, presheaves, etc when profunctors are ultimately simpler. They are unavoidable when you do enriched/internal category theory and they are more directly useful in designing type theories than adjunctions.

danharaj 9y ago
> 1. I would say the primary application is to proving that certain casts (function cast, etc.) are the primary result of the paper. I think you accidentally a word. Re 2: That makes sense to me. In Haskell any terms can contain exceptions but they can only be caught in IO. I look forward to reading the paper this weekend! I started really appreciating profunctors when I first learned what an equipment was, they just seemed to make everything fall into place. One thing I find intriguing about your paper is that the equipment participates directly in the models of the type theory instead of being a way to relate different models ala formal category theory. Perhaps the reason why profunctors aren't highlighted more often is the same prejudice that gives functions a more central place than relations.
- maxiepoo 9y ago
  Ah whoops, I meant to say that the definitions of most of the casts are uniquely determined by soundness (i.e. beta, eta) and graduality (i.e. being an equipment).

danharaj 9y ago

> 1. I would say the primary application is to proving that certain casts (function cast, etc.) are the primary result of the paper. I think you accidentally a word. Re 2: That makes sense to me. In Haskell any terms can contain exceptions but they can only be caught in IO. I look forward to reading the paper this weekend! I started really appreciating profunctors when I first learned what an equipment was, they just seemed to make everything fall into place. One thing I find intriguing about your paper is that the equipment participates directly in the models of the type theory instead of being a way to relate different models ala formal category theory. Perhaps the reason why profunctors aren't highlighted more often is the same prejudice that gives functions a more central place than relations.

maxiepoo 9y ago
Ah whoops, I meant to say that the definitions of most of the casts are uniquely determined by soundness (i.e. beta, eta) and graduality (i.e. being an equipment).