NI
Если имеется в виду типазависимый чатег, то Арсений уже там.
Size: a a a
2018 May 31
ЕО
А, ну другого нету :)
AG
ну он не то чтобы по идрису, просто я адепт идриса :)
NI
ну он не то чтобы по идрису, просто я адепт идриса :)
Главное, что там теорию типов, в основном, вполне допустимо обсуждать.
А именно про это и речь.
А именно про это и речь.
AT
Осталось еще адепта Coq пропиарить 😉 Есть чатик, где мы помогаем с док-вом теорем при помощи Coq. В основном работаем с книгой Software Foundations. Добро пожаловать кому это интересно (как помогать, так и учиться) https://t.me/joinchat/E5XRcA_qvtjO9Z9bdLtWsg
2018 June 01
P
Осталось еще адепта Coq пропиарить 😉 Есть чатик, где мы помогаем с док-вом теорем при помощи Coq. В основном работаем с книгой Software Foundations. Добро пожаловать кому это интересно (как помогать, так и учиться) https://t.me/joinchat/E5XRcA_qvtjO9Z9bdLtWsg
а как этому учиться вообще? начинать с книжки Software Foundations?
P
я просто вообще ничего не знаю, только про общие принципы слышал
AT
Да. Имхо, лучшая книга для начинающих в этой области
IY
Да. Имхо, лучшая книга для начинающих в этой области
имхо, зависит от того, чего хочется. Если взять и начать доказывать теоремы, то да. Но некоторые непростые вопросы там заботливо заметаются под ковер
DR
имхо, зависит от того, чего хочется. Если взять и начать доказывать теоремы, то да. Но некоторые непростые вопросы там заботливо заметаются под ковер
Не без этого, но мне SF очень нравится - с толком и расстановкой, но не обескураживающе сложно
2018 June 10
к
аппликатив это endo lax monoidal functor в декартово замкнутой категории?
AG
по моему как раз необязательно эндо
AG
lax monoidal with strength чото такое
к
ну аппликатив хаскельный я имею в виду, там же не может быть не endo
я думал, аппликатив - это чисто cs-абстракция
я думал, аппликатив - это чисто cs-абстракция
AG
изначально да
к
tensorial strength выглядит странно
к
к
типа разве это не просто map функтора
к
(a, b) -> fmap (a ,) b