gbdj
es

Прибыл в нерезиновый Mournhold. Вежливо попросили встать на учет в течении трех дней. Что поделаешь, столица, ординаторы блюдут.

gbdj

Ах вот оказывается для чего они запилили GADT: "to construct a safe list type for which the equivalent of head [] fails to typecheck and thus does not give the usual runtime error: *** Exception: Prelude.head: empty list". Хорошо надрачивают! Уже думаю пора пойти посмотреть что полезного можно сделать при помощи линеаризованных типов. Понятно что след за утечками памяти в прошлое уйдет и сборщик мусора, но вот можно ли будет так с ними жить...

gbdj

Наконец нормальное разъяснение контравариантных функторов typeclasses.com . Главное тут написано где надо, а главное где не надо искать этот паттерн. Как только осознаешь что речь идет про морфизмы по сути своей сводящимися к (-> z) сразу перестаешь ломать голову как же блин построить обратную функцию, а начинаешь уже думать в контексте функциональной композиции. Нет путаницы в примерах когда не понятно кто из этих конкретных типов в предикате на самом деле свободных параметр или что в каждом контексте значит тип a

gbdj

Поскольку голове несколько полегчало, то в планах на вечер вешить хаскелевую задачку на доказательство леммы Yoneda. codewars.com Чтоб показать изоморвизм надо среди прочего, судя по необходимому типу, определить контравариантный функтор (a -> b) -> f b -> f a И если на диаграмке со стрелочками еще можно сообразить почему он должен существовать, то как реализовать его в реальности да еще и параметрически полиморфным образом мыслей пока нет.