Leonid 🦇
Наверняка @A64m_qb0 тоже пришёл, но не палится
Зигохистоморфный
город не должен знать своих героев)
Denis
так, а я с делами разобрался и скоро буду
Anatolii
Так, это не дело, в след году надо тоже ехать к вам
Leonid 🦇
Ничего там на хай сиерре вроде не починили. Эппл ваш вечно все портит
Dmitry
Да
Dmitry
Всё в полной з.
Зигохистоморфный
и поэтому я пока на просто сиере) хотя тоже г и хочу снова на ель капитан
Зигохистоморфный
http://bitmath.blogspot.com/2017/12/bit-level-commutativity.html
Leonid 🦇
Полный поезд китайцев...
Leonid 🦇
Помяните меня хасклом с карри
Kirill
ты точно в Питер поехал?
Leonid 🦇
Ага
Leonid 🦇
Говорят они этот двухэтажный любят. А в прошлом году я один в купе ехал :(
Leonid 🦇
Вроде норм два мужика, болтать пытаются. Правда в туалет не попасть.
Andrey
всегда можно 50 г коньяку и закрыть глаза
Cheese
@qnikst не так уж далёк от истины
Donat
про хацкель?
Alexander
Декабрь 17 - F(by) Conf http://fby.by
Dmitry
йее
Alexander
извините если нотификации прислал
Vladislav
Есть такое в библиотеке уже? https://gist.github.com/int-index/e9b018a5f7f1313416903a12065161e3
Vladislav
бифункторы в Hask имеют tensorial strength по отношению к тьюплам
Кабачок
А есть что-то вроде функтора, у чего map с такой (a -> b) -> (b -> a) -> f a -> f b сигнатурой?
Сергей
зачем тут (b -> a) ?
Сергей
без него будет обычный ковариантный функтор
Сергей
такая функция всегда существует: const a
Сергей
Тогда функтор контравариантный, и не нужна (a -> b)
Кабачок
data Dec : Type -> Type where
Yes : (prf : a) -> Dec a
No : (contra : a -> Void) -> Dec a
decMap : (a -> b) -> (b -> a) -> Dec a -> Dec b
decMap f g (Yes prf) = Yes (f prf)
decMap f g (No contra) = No (contra . g)
Кабачок
Кажется, это не map, но что?
Сергей
хитро
Влод
не доходит
Dec = decidable? = разрешимое? ну что-то такое
и у него либо доказательство либо опровержение
то есть если написано Dec a – единственная интуиция которая у нас есть это то что оно вычислимо (хотя это глупое предполжение тк вычислимость как-то немного вне этих языков описывается)
Сергей
так здесь всё равно (b -> a) не нужна
Влод
хотя это не имеет отношения к вопросу.
Есть ли такой функтор в хаскеле? – говоря функтор обычно представляешь тайпкласс а тут конкретная не полиморфная функция
вроде раньше ещё не было разговоров про то есть ли в хаскеле хоть что-то помогающее при доказательстве
Влод
Сергей
decMap f (No contra) = No contra
Кабачок
Это предикат, тип может быть либо населенным, либо ненаселенным.
(b -> a) здесь точно нужна, потому что contra : a -> Void это не то же, что и contra : b -> Void.
Влод
Кабачок
Верно.
Влод
с отображением здесь интуиция слабая и наверное есть более лучшее название для этой функции
Влод
слишком просто
Кабачок
Void это ненаселенный тип, у него нету термов
Влод
тем не менее кажется такое выражение будет справедливо в хаскеле
кана
Сергей
эм, тогда нет способа содать и (a -> Void) ?
кана
https://hackage.haskell.org/package/category-extras-0.53.0/docs/Control-Functor-Exponential.html
Влод
лол
Кабачок
Спасибо, @kana_sama.
Кабачок
кана
странно, что в инстансах нет a -> a .
Влод
Кабачок
Чего инстансов?
Влод
Влод
экспоненциального функтора
Влод
какие ещё есть случаи кроме населён/ненаселён
Кабачок
http://comonad.com/reader/2008/rotten-bananas/
Влод
ну да
Влод
придумай сам ироничную фразу. тут кажется очень много хороших подступов для неё есть но я боюсь зафейлить
andrei
кметт)
Egor
Знания теории графов необходимы для разработки?
А если и менее обходимы, то есть ли смысл лезть в дискретный матан и изучать все эти штуки?
Влод
Egor
@t91x0 ну а всякие замысловатые слова и прочие вещи, которые есть в фп понимаются без этих знаний в т.ч.?
Влод
графы не нужны
Влод
самую малость. пару алгоритмов для собесов
Egor
хм, ну не всегда так
Egor
я на фронте работу взял, так мне дали онли тестовое задание, посмотрели, понравилось, взяли
Влод
хм, ну не всегда так
на всякий случай не более того. иначе рискуешь оплошать и весь день ходить грустный
Влод
andrei
+ и -
Слава
Влод
д
andrei
хотя насчет хаскелла я хз
andrei
там только функторы ко и контр видел
Влод
думаю из-за иммутабельности ко и контр не проявляется