зачем тут (b -> a) ?

без него будет обычный ковариантный функтор

зачем тут (b -> a) ?

требует доказательство существования такой функции

такая функция всегда существует: const a

зачем тут (b -> a) ?

Затем, что без такой функции не получить f b

Тогда функтор контравариантный, и не нужна (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) не нужна

хотя это не имеет отношения к вопросу. Есть ли такой функтор в хаскеле? – говоря функтор обычно представляешь тайпкласс а тут конкретная не полиморфная функция вроде раньше ещё не было разговоров про то есть ли в хаскеле хоть что-то помогающее при доказательстве

так здесь всё равно (b -> a) не нужна

возможно нужна

decMap f (No contra) = No contra

Это предикат, тип может быть либо населенным, либо ненаселенным. (b -> a) здесь точно нужна, потому что contra : a -> Void это не то же, что и contra : b -> Void.

decMap f (No contra) = No contra

оно же даст тип Dec a

Верно.

с отображением здесь интуиция слабая и наверное есть более лучшее название для этой функции

оно же даст тип Dec a

да. Тогда: decMap f (No contra) = No (const Void)

слишком просто

Void это ненаселенный тип, у него нету термов

тем не менее кажется такое выражение будет справедливо в хаскеле

А есть что-то вроде функтора, у чего map с такой (a -> b) -> (b -> a) -> f a -> f b сигнатурой?

экспоненциальный функтор или что-то типа того такой был в какой-то либе

эм, тогда нет способа содать и (a -> Void) ?

https://hackage.haskell.org/package/category-extras-0.53.0/docs/Control-Functor-Exponential.html

лол

Спасибо, @kana_sama.

эм, тогда нет способа содать и (a -> Void) ?

Если a ненаселен, то есть.

странно, что в инстансах нет a -> a .

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)

так data Dec один из инстансов просто, да?

Чего инстансов?

Это предикат, тип может быть либо населенным, либо ненаселенным. (b -> a) здесь точно нужна, потому что contra : a -> Void это не то же, что и contra : b -> Void.

что говорит этот предикат

экспоненциального функтора

какие ещё есть случаи кроме населён/ненаселён

http://comonad.com/reader/2008/rotten-bananas/

ну да

придумай сам ироничную фразу. тут кажется очень много хороших подступов для неё есть но я боюсь зафейлить

кметт)

Знания теории графов необходимы для разработки? А если и менее обходимы, то есть ли смысл лезть в дискретный матан и изучать все эти штуки?

Знания теории графов необходимы для разработки? А если и менее обходимы, то есть ли смысл лезть в дискретный матан и изучать все эти штуки?

Смотря чем вы планируете заниматься. Хотя чем бы ни планировали - 95% работы в IT - это чистить вилкой - раз-раз-раз! и графы тут не пригодятся.

Знания теории графов необходимы для разработки? А если и менее обходимы, то есть ли смысл лезть в дискретный матан и изучать все эти штуки?

дискретка оче широкое понятие

@t91x0 ну а всякие замысловатые слова и прочие вещи, которые есть в фп понимаются без этих знаний в т.ч.?

графы не нужны

самую малость. пару алгоритмов для собесов

хм, ну не всегда так

я на фронте работу взял, так мне дали онли тестовое задание, посмотрели, понравилось, взяли

@t91x0 ну а всякие замысловатые слова и прочие вещи, которые есть в фп понимаются без этих знаний в т.ч.?

то есть от тега дискретная математика можно перейти к тегам вот этого хаскельного фп то есть и там и там могут говорить что нечто образует решётку например и у меня с вузовым этим бекграундом начнут появляться ассоциации и я успокоюсь что эта фраза была мусором и можно просто позавидовать наблюдательности докладчика и похлопать ему за это

@t91x0 ну а всякие замысловатые слова и прочие вещи, которые есть в фп понимаются без этих знаний в т.ч.?

Вряд ли. Я лично не отличу ковариантность от контрвариантности, хотя скорее всего и знаю, что это - на практике, но не сами термины. Ещё следует привыкнуть, что функциональщики вместо осмысленных названий любят i,j,k, O o, и марсианскую букву хфы

хм, ну не всегда так

на всякий случай не более того. иначе рискуешь оплошать и весь день ходить грустный

Вряд ли. Я лично не отличу ковариантность от контрвариантности, хотя скорее всего и знаю, что это - на практике, но не сами термины. Ещё следует привыкнуть, что функциональщики вместо осмысленных названий любят i,j,k, O o, и марсианскую букву хфы

ммм... скорей всего не знаешь штука на которую не обращаешь внимания пока язык не начнёт тебе навязывать

+ и -

ммм... скорей всего не знаешь штука на которую не обращаешь внимания пока язык не начнёт тебе навязывать

В дженериках оно может быть?

д

хотя насчет хаскелла я хз

там только функторы ко и контр видел

думаю из-за иммутабельности ко и контр не проявляется

хотя насчет хаскелла я хз

в хаскеле нет сабтайпинга

ну слова эти употребимы да

у функторов это про сторону стрелок

аа ну да

думаю можно употребить слово с вариативностью если в разных местах функции поставить forall

А есть что-то вроде функтора, у чего map с такой (a -> b) -> (b -> a) -> f a -> f b сигнатурой?

это ж профунктор https://hackage.haskell.org/package/profunctors-5.2.1/docs/Data-Profunctor.html#v:dimap

ERROR: S client not available

Как вам Idris? Какие у него неожиданности?

Пошёл в #Idris :)

grug gateway to зависимые типы

неожиданностей нету, от языка плейграунда Брейди и не ожидаешь большего

Знания теории графов необходимы для разработки? А если и менее обходимы, то есть ли смысл лезть в дискретный матан и изучать все эти штуки?

Если ты не угораешь по всяким лизергиноморфизмам, то единственная область дискретки, которая тебе на самом деле нужна будет на практике, -- теория типов

Если ты не угораешь по всяким лизергиноморфизмам, то единственная область дискретки, которая тебе на самом деле нужна будет на практике, -- теория типов

а графы и булевая логика?

Ну графы любому программисту нужны, хаскель тут не при чём. А булева логика это не раздел никакой, чо там изучать-то?

Ну графы любому программисту нужны, хаскель тут не при чём. А булева логика это не раздел никакой, чо там изучать-то?

разложение булевых функций на всякие СКНФ и NAND

Согласен, это достаточно нетривиально, но в практике программирования нужно только для прологов всяких

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

лизергиноморфизмы надо запомнить и взять на вооружение

у меня ассоциации только с морфизмами между линзами и зергами

хаскель больше на язык от протосов похож

хаскель больше на язык от протосов похож

у терранов слишком маленький мозг, они не способны понять технологии протосcов LOTV

а вообще весь этот чат нужно сжечь за использование ксенотехнологий

лизергиноморфизмы надо запомнить и взять на вооружение

?️‍?

у меня ассоциации только с морфизмами между линзами и зергами

Ну ЛСД же

я в этом вашем не шарю

мескалиноморфизм

это ж профунктор https://hackage.haskell.org/package/profunctors-5.2.1/docs/Data-Profunctor.html#v:dimap

Нет, профунктор Type -> Type -> Type, контравариантен по первому параметру и ковариантен по второму параметру, а экспоненциальный функтор Type -> Type и его вариантность заранее неизвестна.

никто в квантовые шахматы не хочет поиграть? (знаю что оффтоп)

если ключ кинешь

никто в квантовые шахматы не хочет поиграть? (знаю что оффтоп)

Что такое квантовые шахматы? Это когда в игре несколько партий, находящихся в состоянии суперпозиции? А как происходит декогеренция?

http://truly-quantum-chess.sloppy.zone

бесплатная версия

там wiki почти полная

вкратце можно сделать квантовый ход, это 2 обычных, но бить не можешь, в итоге фигура будет в суперпозиции старого и нового состояний

и со всем из этого ввтекающим

Декогеренция происходит в момент атаки?

Затестил сейчас, интересная концепция)