AZ
а концы при чем?
Size: a a a
2019 December 23
NI
а концы при чем?
"А я всегда про них думаю" ;-)
При том, что это очень важная конструкция, которая возникает рядом.
Важна формулировка леммы Йонеды через (ко)концы.
А важна потому, что они легко выражаются в хаскеле, давая удобную хаскельную формулировку.
При том, что это очень важная конструкция, которая возникает рядом.
Важна формулировка леммы Йонеды через (ко)концы.
А важна потому, что они легко выражаются в хаскеле, давая удобную хаскельную формулировку.
NI
Ну и в целом, не только хаскельную, а тут надо за параметричность говорить.
AZ
вот я как раз про "in terms", ведь можно и не in terms?
AZ
если брать во эту картинку с
forall то =~ можно заменить на пару функций туда и обратноOℕ
У бартоша в каком-то блоге есть и про концовую/лимитную формулирвку
Oℕ
не помню, в каком
Oℕ
вот я как раз про "in terms", ведь можно и не in terms?
можно и не, но коЙонеда делается через соответствие конца коконцу
Oℕ
в койонеде будет что-то вроде
exists a. (a -> x, f a) <~> f x
exists a. (a -> x, f a) <~> f x
AZ
ну так все которые не forall имплаятся как exists
Oℕ
ну или
exists a (x -> a, f a) <~> f a
для контравариантных
exists a (x -> a, f a) <~> f a
для контравариантных
AZ
получается phi :: exists a . (forall x . ((a -> x) -> F x) -> F a)
AZ
насколько я понял RankNTypes оно так работает
Oℕ
ну так все которые не forall имплаятся как exists
если в хошкеле трансформировать exists в forall будет такое что-то
forall x . ((forall r. (forall a. (a -> x) -> f a -> r)) <~> f x)
forall x . ((forall r. (forall a. (a -> x) -> f a -> r)) <~> f x)
AZ
если в хошкеле трансформировать exists в forall будет такое что-то
forall x . ((forall r. (forall a. (a -> x) -> f a -> r)) <~> f x)
forall x . ((forall r. (forall a. (a -> x) -> f a -> r)) <~> f x)
я имею ввиду что тут нет двух фороллов
Oℕ
я имею ввиду что тут нет двух фороллов
не понял, где вы имеете это в виду, где - тут, и о чём вы говорите.
Я говорю о ко-Йонеде
Я говорю о ко-Йонеде
AZ
ну вы говорите что должен быть экзистс, я говорю что в оригинальной формулировке он там есть, просто неявный, потому что все переменные для которых не объявили явно forall полагаются exists
Oℕ
нет
AZ
в койонеде будет что-то вроде
exists a. (a -> x, f a) <~> f x
exists a. (a -> x, f a) <~> f x
А в таком виде это эквивалентно этому утверждению