Телеграмм чат группы ru_catheory страница 382

Size: a a a

Теория категорий

2019 December 23

У меня для койонеды вроде тайпчекнулось с forall

cophi :: (forall x . (x -> a) -> f x) -> f a
cophi alpha = alpha id

copsi :: Contravariant f => f a -> (forall x . (x -> a) -> f x)
copsi fa h = contramap h fa

источник

16:44пожаловаться #1

Alex Zhukovsky in Теория категорий

судя по тому как в стд сделано они с помощью дата-класса контравариант на копси переделали на вариантный функтор на кофи

источник

16:49пожаловаться #2

ЗП

Зигохистоморфный Препроморфизм in Теория категорий

Alex Zhukovsky

У меня для койонеды вроде тайпчекнулось с forall

cophi :: (forall x . (x -> a) -> f x) -> f a
cophi alpha = alpha id

copsi :: Contravariant f => f a -> (forall x . (x -> a) -> f x)
copsi fa h = contramap h fa

это контрвариантная йонеда

источник

16:54пожаловаться #3

Alex Zhukovsky in Теория категорий

источник

16:55пожаловаться #4

Alex Zhukovsky in Теория категорий

Я что-то не понимаю

источник

16:55пожаловаться #5

Alex Zhukovsky in Теория категорий

может речь про это сноску?

источник

16:56пожаловаться #6

Alex Zhukovsky in Теория категорий

судя по стд хачкеля это как раз таки койонеда: https://hackage.haskell.org/package/kan-extensions-5.2/docs/src/Data.Functor.Coyoneda.html#Coyoneda

источник

16:56пожаловаться #7

Alex Zhukovsky in Теория категорий

по крайней мере сигнатура listCoyoneda/lowerCoyoneda совпадает с тем что у меня (сточностью до Functor/Contravariant, но я вроде сказал что с дата-классом это можно решить)

источник

16:57пожаловаться #8

ЗП

Зигохистоморфный Препроморфизм in Теория категорий

Alex Zhukovsky

судя по стд хачкеля это как раз таки койонеда: https://hackage.haskell.org/package/kan-extensions-5.2/docs/src/Data.Functor.Coyoneda.html#Coyoneda

нет в GADTs, что ты видишь через стрелку это как тип произведение

источник

16:57пожаловаться #9

Alex Zhukovsky in Теория категорий

я ведь понимаю, что чтобы доказать =~ нужно написать две функции с такой сигнатурой в ту и обратную сторону

источник

16:58пожаловаться #10

ЗП

Зигохистоморфный Препроморфизм in Теория категорий

data Coyoneda f a where
  Coyoneda :: (b -> a) -> f b -> Coyoneda f a

это

data Coyoneda f a = forall b. Coyoneda (b -> a) (f b)

это же

type Coyoneda f a = exists b. (b -> a, f b)

источник

16:59пожаловаться #11

Alex Zhukovsky in Теория категорий

То есть дата классом кодируется именно существование (раз мы смогли создать его инстанс)?

источник

17:01пожаловаться #12

Oℕ

Oleg ℕizhnik in Теория категорий

давайте про кодирование экзистов в другой чат

источник

17:04пожаловаться #13

ЗП

Зигохистоморфный Препроморфизм in Теория категорий

Oleg ℕizhnik

давайте про кодирование экзистов в другой чат

он во всех чатах одно и тоже спрашивает)

источник

17:05пожаловаться #14

Alex Zhukovsky in Теория категорий

Зигохистоморфный Препроморфизм

он во всех чатах одно и тоже спрашивает)

в двух. Потому не знаю, хачкельный или категорный для этого подходит.

И спрашиваю несколько разное

источник

23:47пожаловаться #15

Alex Zhukovsky in Теория категорий

Alex Zhukovsky

но если вернутсья к этой картинке тут нет экзистов, а автор называет это койонедой

источник

23:47пожаловаться #16

Alex Zhukovsky in Теория категорий

либо он ошибаетсЯ, либо одно из двух

источник

23:48пожаловаться #17

Kirill Valyavin in Теория категорий

Щас на четвертый круг пойдём

источник

23:50пожаловаться #18

Alex Zhukovsky in Теория категорий

Alex Zhukovsky

У меня для койонеды вроде тайпчекнулось с forall

cophi :: (forall x . (x -> a) -> f x) -> f a
cophi alpha = alpha id

copsi :: Contravariant f => f a -> (forall x . (x -> a) -> f x)
copsi fa h = contramap h fa

вот это буквально то что записано на картинке выше

источник

23:54пожаловаться #19

Alex Zhukovsky in Теория категорий

автор говорит "это койонеда", вы говорите "это коваирантная йонеда"

источник

23:54пожаловаться #20