@Electrosnail я вот читаю про категорию Hask, и она определяется

Question

@Electrosnail я вот читаю про категорию Hask, и она определяется

так, что объекты в ней - типы, а стрелки - (->).
Я рассуждаю так, что если co-X, это X, где все стрелки развёрнутый в обратную сторону, то с Hask получается именно так, что (f: a -> b) => (co(f): b -> a).

Здесь ошибка в том, что Со - это не просто переворачивание стрелок?

0

04.08.2024

2 ответов

13 просмотров

Лев Дворкин

Если в терминах класса Category, то Hask есть instance Category A где newtype A a b = a -> b, а Hask* есть instance Category CA где newtype CA a b = b -> a. При этом ваш op на функциях действует как перепаковка newtype'ов (то есть coerce) Всё, что записывается в двойственной категории можно записать и в исходной, перевернув стрелки. В этом смысле различия чисто формальные. Но они есть. Например, тип композиции (с точностью до newtype будет `(c -> b) -> (b -> a) -> c -> a``` Не знаю, стало ли что-то понятнее.

0

2 месяца назад

Глафира Слоникова · Accepted Answer

Понятие двойственной категории чисто формально, в категории Hask^* морфизм из a в b - это отображение из b в a в Hask. Двойственные категории были придуманы по той причине, что многие функторы переворачивают направление стрелок. Один из самых типичных функторов - это функтор кольца непрерывных функций на пространстве. Если у вас есть непрерывное отображение пространства X в пространство Y, q : X -> Y, а C(X) и C(Y) - кольца непрерывных функций, то C(q) - это отображение из C(Y) в C(X) (получаемое композицией функции на Y с q, f(q(.)) - это функция на Y, получаемая из функции f(.) на X, точка из X сначала приезжает на q в Y а потом от нее берется функция). Это называется "обратный образ". Таким образом, C - не совсем функтор, он оборачивает стрелочки. Сначала такое называли "контравариантный функтор", а потом решили, что можно сказать, что это обычный, "ковариантный" функтор, но из двойственной к Top категории (или, наоборот, из Top в двойственную к Ring). Понятие двойственной категории чисто формально (вроде?)

Похожие чаты

@Electrosnail я вот читаю про категорию Hask, и она определяется

2 ответов

Похожие вопросы