Feb. 5th, 2013
typeclasses take 5
Feb. 5th, 2013 09:42 pmДа всё фигня, никакие там теории и модели не нужны. Происходит вот что (выражаясь в наивной теории категорий, т.е., в сущности, в терминах внутренних категорий в топосе).
Берём эндофунктор Т, берём категорию алгебр над Т, и забывающий U из алгебр в, э, базовую категорию.
К забывающему, предположительно, есть левый сопряженный, свободные алгебры над Т. В терминах "языков программирования" эти свободные алгебры получаются путём взятия неограниченного числа переменных и применения к ним различного рода конструкторов, определяемых Т.
Ну, например, для эндофунктора "Моноид" конструкторов будет два, один без параметров, даёт нейтральный элемент, а другой с двумя, даёт выражение "a+b".
Тут мне не совсем понятно, шо це за эндофунктор такой, "моноид", надо разобраться. В принципе, он как раз получается из "теории моноида".
Ну и модели, т.е. инстансы тайпкласса - это просто алгебры над каким-то эндофунктором; а категория таких алгебр и есть тайпкласс.
Что не так?
Тут ещё можно привлечь монаду коплотности, но эта монада, выше, и является монадой коплотности, где расширение Кана тривиально порождается сопряженной парой.
Берём эндофунктор Т, берём категорию алгебр над Т, и забывающий U из алгебр в, э, базовую категорию.
К забывающему, предположительно, есть левый сопряженный, свободные алгебры над Т. В терминах "языков программирования" эти свободные алгебры получаются путём взятия неограниченного числа переменных и применения к ним различного рода конструкторов, определяемых Т.
Ну, например, для эндофунктора "Моноид" конструкторов будет два, один без параметров, даёт нейтральный элемент, а другой с двумя, даёт выражение "a+b".
Тут мне не совсем понятно, шо це за эндофунктор такой, "моноид", надо разобраться. В принципе, он как раз получается из "теории моноида".
Ну и модели, т.е. инстансы тайпкласса - это просто алгебры над каким-то эндофунктором; а категория таких алгебр и есть тайпкласс.
Что не так?
Тут ещё можно привлечь монаду коплотности, но эта монада, выше, и является монадой коплотности, где расширение Кана тривиально порождается сопряженной парой.