![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
i got it, got it
Apr. 29th, 2015 04:26 amIn short, there are small types and big types. Small types, you can call them data types, but that term is kind of taken.
Small types are what the OOP people draw in their class diagrams. Large types are whatever is available in your language.
Embedding (modeling) a small type in a large type is just Yoneda embedding.
So e.g. the diamond problem turns into the problem of building a limit or a colimit. Or rather a Kan extension of appropriate variance.
So-called inheritance is just about Kan extensions, which turn, when the base category ("large types" of a language) is a topos (has logic), into geometric morphisms... rather, into essential geometric morphisms.
That's it; that's why I just woke up and went down to write it down.
Maybe it's all pretty trivial, maybe not.
Upd:
http://arxiv.org/pdf/1206.0357.pdf
http://comonad.com/reader/2015/domains-sets-traversals-and-applicatives/
Small types are what the OOP people draw in their class diagrams. Large types are whatever is available in your language.
Embedding (modeling) a small type in a large type is just Yoneda embedding.
So e.g. the diamond problem turns into the problem of building a limit or a colimit. Or rather a Kan extension of appropriate variance.
So-called inheritance is just about Kan extensions, which turn, when the base category ("large types" of a language) is a topos (has logic), into geometric morphisms... rather, into essential geometric morphisms.
That's it; that's why I just woke up and went down to write it down.
Maybe it's all pretty trivial, maybe not.
Upd:
http://arxiv.org/pdf/1206.0357.pdf
http://comonad.com/reader/2015/domains-sets-traversals-and-applicatives/
