TR
Ну вот вы взяли, например, и категориальную логику вычеркнули искусственно. Да и теория типов это раздел логики
Это я когда читал вспомнил обсуждение категорной логики
Size: a a a
2020 January 08
2020 January 12
AZ
Эмм, а как этот бот понял что требуется? И что такое $map_F ?
YS
Эмм, а как этот бот понял что требуется? И что такое $map_F ?
> Эмм, а как этот бот понял что требуется?
есть алгоритмы населения типов, скорее всего, lambdabot вызывает программу https://hackage.haskell.org/package/djinn
есть алгоритмы населения типов, скорее всего, lambdabot вызывает программу https://hackage.haskell.org/package/djinn
YS
Эмм, а как этот бот понял что требуется? И что такое $map_F ?
> И что такое $map_F ?
вероятно, реализация fmap для F, то есть
вероятно, реализация fmap для F, то есть
fmap @F, если записать на современном ХаскелеAZ
а fmap h тогда что?
AZ
я не понимаю почему два разных fmap и в чем разница между ними
МБ
А чего они всё на Вадлера-то ссылаются? Theorems for free - это статья Рейнодьдса из 70-ых годов
AZ
А чего они всё на Вадлера-то ссылаются? Theorems for free - это статья Рейнодьдса из 70-ых годов
ну ссылка на этот пейпер: https://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf
AZ
и я не видел более ранних вариантов. Этот самый известный вроде
AZ
Так в чем разнича между $map_F и fmap?
AZ
ну мне кажется, это более ранняя работа, но не совсем про фри теоремы. Фри теоремы развитие этой идеи, но не она сама
МБ
ну мне кажется, это более ранняя работа, но не совсем про фри теоремы. Фри теоремы развитие этой идеи, но не она сама
Почему? Там прямо есть эти следствия
МБ
Вадлер просто мутный какой-то персонаж. Например, монады для вычислений придумал Плоткин и Могги. А приписывают их тоже Вадлеру. Он там зав. лаб какой-то важный?
AZ
Почему? Там прямо есть эти следствия
тогда почему бы не написать в глазгов "сволочи, вы тут уперли чужой пейпер и выдали за свой" если ты считаешь что этот не имеет ценности?
МБ
Ну... Кто я, а кто Вадлер? Мне просто интересно, почему так дела обстоят
NI
Ну... Кто я, а кто Вадлер? Мне просто интересно, почему так дела обстоят
Вадлер один из аффтаров хаскеля.
Монады он в хаскель затащил, например.
Ну и просто известный популяризатор.
Например, про линейную логику.
Монады он в хаскель затащил, например.
Ну и просто известный популяризатор.
Например, про линейную логику.
МБ
тогда почему бы не написать в глазгов "сволочи, вы тут уперли чужой пейпер и выдали за свой" если ты считаешь что этот не имеет ценности?
Кстати, он ссылается на Рейнольдса. Но у Рейнольдса почти то же самое написано о параметричности
МБ
Вадлер один из аффтаров хаскеля.
Монады он в хаскель затащил, например.
Ну и просто известный популяризатор.
Например, про линейную логику.
Монады он в хаскель затащил, например.
Ну и просто известный популяризатор.
Например, про линейную логику.
Типа, на правах патриарха?