ЗФ
себе) что не херню придумал и не нарушаешь законы абстракции
вот зачем эти пруверы все, если потом сидишь и все равно сам эту поебень докпзываешь
Size: a a a
2020 February 25
ЗП
вот зачем эти пруверы все, если потом сидишь и все равно сам эту поебень докпзываешь
пруверы как раз доказывают, но хаскель это не прувер, система типов не достаточно полна для автоматических доказательств
👨M
вот зачем эти пруверы все, если потом сидишь и все равно сам эту поебень докпзываешь
Ну есть же люди, которые сами с собой разговаривают, и головой так шатают ещё над листом бумаги
SФ
Ну есть же люди, которые сами с собой разговаривают, и головой так шатают ещё над листом бумаги
Они называются математики
AR
Ну есть же люди, которые сами с собой разговаривают, и головой так шатают ещё над листом бумаги
ты слышишь голос в своей голове?
👨M
ты слышишь голос в своей голове?
Всегда, кстати. Как и все люди в целом. Хотя не понятно, что слышат глухие
SФ
Всегда, кстати. Как и все люди в целом. Хотя не понятно, что слышат глухие
Далеко не все. Есть разные типы мышления
SФ
Вот похоже ты не умеешь картинками, а умеешь голосом
👨M
Вот похоже ты не умеешь картинками, а умеешь голосом
Тоесть, когда ты «про себя» размышляешь, ты это картинками делаешь?
ЗП
например сделал ты моноид и вот это вот тебе руками описать надо, а пруверы это выводят из-за того что у них есть мощность доказательной базы
https://github.com/JetBrains/arend-lib/blob/master/src/Algebra/Monoid.ard#L7-L9
https://github.com/JetBrains/arend-lib/blob/master/src/Algebra/Monoid.ard#L7-L9
AR
Далеко не все. Есть разные типы мышления
я нормально так офигел когда узнал что не у всех диалог в голове
ЗФ
например сделал ты моноид и вот это вот тебе руками описать надо, а пруверы это выводят из-за того что у них есть мощность доказательной базы
https://github.com/JetBrains/arend-lib/blob/master/src/Algebra/Monoid.ard#L7-L9
https://github.com/JetBrains/arend-lib/blob/master/src/Algebra/Monoid.ard#L7-L9
ты описываешь свои моноиды?
ЗП
ну понятие внутреннего диалога растяжимое, и его можно и приглушать и усиливать
ЗП
ты описываешь свои моноиды?
бывает) это же мощная концепция) и имея моноидальные свертки ты не паришься про бинарный оператор, для моноидальной конструкции
ЗФ
бывает) это же мощная концепция) и имея моноидальные свертки ты не паришься про бинарный оператор, для моноидальной конструкции
я могу верифицировать код на тайпскрипте, например залупу написанную с fp-ts
👨M
Объясните, как это вместо диалога - картинки?
SФ
Объясните, как это вместо диалога - картинки?
Да, образы, картинки, а может быть что-то совсем другое, как чистое понимание
ЗП
совсем недавно было, что
Монада - это просто моноид в категории эндофункторов
потом
Монада - это просто подмонада continuation монады
и вот я недавно пришел к такому)
Монада - это просто предпучок в степени профунктора
Монада - это просто моноид в категории эндофункторов
потом
Монада - это просто подмонада continuation монады
и вот я недавно пришел к такому)
Монада - это просто предпучок в степени профунктора
👨M
совсем недавно было, что
Монада - это просто моноид в категории эндофункторов
потом
Монада - это просто подмонада continuation монады
и вот я недавно пришел к такому)
Монада - это просто предпучок в степени профунктора
Монада - это просто моноид в категории эндофункторов
потом
Монада - это просто подмонада continuation монады
и вот я недавно пришел к такому)
Монада - это просто предпучок в степени профунктора
SФ
Тоесть, когда ты «про себя» размышляешь, ты это картинками делаешь?
Где-то был недавно тред в тви вот про это все