## User login## Navigation |
## Using Category Theory to Design Implicit Conversions and Generic OperatorsUsing Category Theory to Design Implicit Conversions and Generic Operators, John C. Reynolds, 1980. (Try this if the official link doesn't work.)
This is an old, but still cute, paper. The basic intuition is that a good design principle for a language with implicit conversions is that whatever order of conversions the language takes, you should get the same result. He then formalizes that by giving a category of types and conversions, and demanding that everything commute properly. And these give just the conditions the language designer has to check to make sure that he or she hasn't screwed anything up. Someone could probably get a fun little paper by taking this idea and shooting some dependent types into it. (Maybe somebody already has?) If you've got an abstract type, a coercion function, and a proof that it satisfies Reynolds' conditions, now your compiler can silently insert those coercions for you as needed, but you can still be sure that it won't mess up the meaning of your program. |
## Browse archives
## Active forum topics |

## Recent comments

6 hours 54 min ago

6 hours 54 min ago

7 hours 29 min ago

7 hours 59 min ago

8 hours 6 min ago

8 hours 21 min ago

8 hours 52 min ago

10 hours 19 min ago

13 hours 15 min ago

21 hours 36 min ago