AZ
вроде
Size: a a a
2019 December 22
AZ
ну да, так и есть
AZ
наверно, лемма правильная. напишите доказательство в общем виде. выразите
to :: (forall x . (x -> a) -> F x) -> F a
from :: F a -> (forall x . (x -> a) -> F x)
через fmapпросто автор подразумевает некоторые вещи которые я не понимаю
AZ
Prelude> :{
Prelude| phi :: (forall x . (a -> x) -> Maybe x) -> Maybe a
Prelude| phi alpha = alpha id
Prelude| :}
Prelude>AZ
эмм, а как он схавал это?
AZ
откуда он 'a' взял?
PG
Хаскель по дефолту добавляет forall для каждой свободной перменной в типе
AZ
а как определить свободная или нет? и x и a используются справа от (a -> x)
ЕО
Свободная это та, которая не связана ни с каким forall'ом
ЕО
Т.е. если ты явно не поставишь forall, то компилятор за тебя в самом начале его допишет
AZ
я пытаюсь понять, почему тут один forall а не два
PG
Если ты пишешь
(a -> b) -> c это будет forall a b c. (a -> b) -> c, но (forall a. a -> b) -> c это уже forall b c. (forall a. a -> b) -> cAZ
Чтобы это понять переписал на родной шарпик:
Где он логично жалуется, что не может из A в X преобразовать
struct Maybe<T> { }
Maybe<A> Phi<A, X>(Func<Func<A, X>, Maybe<X>> alpha) => alpha(_ => _);Где он логично жалуется, что не может из A в X преобразовать
O
какой тут приоритет у операторов? (x -> a) -> (F x =~ F a) ?
AZ
какой тут приоритет у операторов? (x -> a) -> (F x =~ F a) ?
я думаю у ~= самый низкий
O
тогда всё встаёт на свои места
AZ
((x -> a) -> F x) =~ F a
AZ
в общем я не очень понимаю эту запись:
phi :: (forall x . (a -> x) -> Maybe x) -> Maybe aAZ
такое ощущение что a это просто экзистенциальный тип
AZ
типа существует такая функа a -> x что получится Maybe a