поищи по Artyom в списке участников чата, если он не вышел

это твоя что ли статья?

нет конечно, это очень годный ресурс по линзам

похоже или переименовался так что не узнать или из чятика вышел

Dmitry я наверное снимаю pinned message наверху, все равно никто уже не отвечает; как сайт обновите пните, я туда объявление про fby (а заодно и мск-шную конфу добавлю)

Да, спасибо!

ресурс действительно очень годный, я, правда, на третьей статье уже сдался, до профункторов не дошёл...

NICTA lens тоже ничо так

там как раз задачи на переизобретение линз

причем сначала более простых версий

правда тут как с МОНАДАМИ

пока практического опыта использования нормальных линз не набрать, даже при понимании теории есть сложности

я так и не набрал, не считая всякой неинтересной тривиальщины

NICTA lens тоже ничо так

ссылку?)

https://github.com/data61/lets-lens

или забанят

>Приз: токены LAT Это что ещё за фантики?:) В рублях то сколько?

самое заманчивое здесь это конечно же божественные токены LAT

Есть у кого-нибудь годные текстовые ресурсы по теориям типов, доказательств, лямбда исчислению, HoTT? P.S. Желательно понятным для нематематика языком и с примерами использования в реальном мире, например, как у Милевского по теоркату

Типы в языках программирования. Пирса уже прочитаны?

Нет, спасибо, почитаю

наверное must read книга

потом уже к всяким HoTT идти

Да я в целом очертил, то во что хочу въехать, так что порядок изучения мне тоже интересно узнать

Software Foundations (типа TaPL, но не вся) - можно въехать в компьютерные доказательства, очень доходчиво написано, главный автор тот же B.C. Pierce (книга бесплатная). Type-Driven Development with Idris by E. Brady- отличная книга с упором на зависимые типы

надо кстати software foundations почитать

А лучше начинать с практики (хаскель) или с теории (тапл, CT)? Я пока параллельно читаю

SF надо не сколько читать сколько писать :)

ну и TaPL писать надо

без этого не так много толку

Ну у меня сейчас haskell programming параллельно с category theory от awodey

ну на haskell можно писать без CT вообще

и уйти достаточно далеко

потом появятся зайчатки знаний по СТ все равно

причем достаточные чтобы кметтолибы читать (возможно)

надо кстати software foundations почитать

а там еще и 3-й том от Аппеля зарелизился недавно!

ну что ж за жизнь ещё и по sequential calculus кучу ресурсов читать

о боги! в SF Coq

ну на haskell можно писать без CT вообще

вспомнился вот этот вопрос: https://cs.stackexchange.com/questions/3028/is-category-theory-useful-for-learning-functional-programming

Там прикольный коммент к вопросу: "Learning Category Theory to become better in Haskell" is a bit like "Learning physics to become better in tennis"

вот да

Всем привет

кто-то из великих говорил, что изучать ТК, чтобы понимать Хаскелл — это как учить испанский, чтобы понимать буррито

Привет

ну ты сравнил конечно

хаскел с бурито

это не тот который говорил что монады как бурито?

кто-то из великих говорил, что изучать ТК, чтобы понимать Хаскелл — это как учить испанский, чтобы понимать буррито

есть куча людей, говорящих на кастильском испанском, но они не очень понимают в буррито 😉

ну тогда аналогия логична

ксть те кто знают ТК, но не понимают Haskell

what is TK?

what is TK?

what is CT? тогда 😉

Never mind, I hadn't became to know about this better =)

Кстати, господа, есть ли где-то стажировки для хаскеллистов?

Хммм, тут, пожалуй немного в другом фишка

Хаскелл позволяет естественным образом строить категорные конструкции

у нас были, но нужно во Франции быть и я не знаю требований

Это... красиво

Хаскелл позволяет естественным образом строить категорные конструкции

почти) если бы не жопы

жопы?

bottom

_|_

оо крутая терминология

/me убил котика, извините

стикеры запрещены?

Да, любой траверс будет линзой. Но не все функторы аппликативные

type Traversal' a b = forall f . Applicative f => (b -> f b) -> (a -> f a)

он может задать только такой f, который Applicative

как следствие этот же f автоматически будет и Functor

т.е. как следствие будет подходить для любой линзы

type Lens' a b = forall f . Functor f => (b -> f b) -> (a -> f a)

https://arstechnica.com/gadgets/2017/09/microsoft-quantum-toolkit/

@kana_sama и?

ну значит не каждая линза может быть траверсом, хоть все траверсы - линзы

да, я там криво сказал

А как вы код форматируете в телеграме? :D

` <- вначале и вконце

три `

Ого. спасибо

>не отправлять pdf с кодом созданную с lstlistings

@kana_sama что такое линза, это функция которая для любого f подставленного пользователем делает (b -> f b) -> (a -> f b) испольщуя только ту информацию, что f это функтор