Вячеслав Шебанов - Системы типов в двух словах

[@cristopherrobin938]

Капец как годно.

[@rustonelove]

Засыпаться через 5 минут. Годнота годнот.

[@kost9kost]

Духота

[@rustonelove]

35:40 - никакого отношения к типизации не имеет. Тут существует одна фундаментальная проблема. Такого уровня компилятор, как CompCert, нахрен никому ненужен и в нём итак не будет ошибок. К тому же, нужно понимать, что любая формальная верификация имеет в основе аксиоматическую природу. Очевидно, что никак нельзя доказать верность аксиомы. Это не имеет смысла. Если говорить более широко, то можно определить какую-либо модель и доказать соответствие логики(написанной в программе) логике определённой в данной модели. Именно этим занимается верификация. Проблемы тут очевидны. Всё имеет аксиоматическую природу(что модель, что доказательства) и как следствие это вообще ничего не доказывает. Подобная проблема неразрешима. Любая верификация зависит от верификации и далее по рекурсии. Любая верификация лишь условность. Если говорить проще - механизм отмывания бабла с грантов, путём производства бесполезного мусора.

[@vyorkin]

все посылки, вроде бы, верные, но не понятно как вы пришли к > механизм отмывания бабла с грантов, путём производства бесполезного мусора

[@rustonelove]

​@@vyorkin Да очень просто. Если что-то не имеет смысла и применения - зачем оно нужно? Зачем о нём рассказывать, зачем рассказывать аудитории, которая нихрена не понимает в теме? Это что-то не имеет объективных предпосылок к существованию, а его адепты и ваятели не имеют права существовать в том качестве, котором о себе заявляют. В конечном итоге возможно два варианта. Люди либо не понимают, либо идиоты. Очевидно, что если они идиоты - это ломает все устои общества и мы можем на это ссылаться. Если они не понимают - есть два варианта. В любом случае какое-то развитие быть должно. Но мы его не видим. Все эти методички как созданы в 70 лет назад - так слово в слово и ретранслируются. И вот они два варианта - либо идиоты, либо существуют скрытые мотивы. Первое мы отрицаем. Остаётся второе. А какие могут быть скрытые мотивы? Эти мотивы очевидны. Каждый повязанных с тем же CompCert, живущий на грантах, не состоятелен вне это схемы. По крайне мере нет свидетельств обратному. Кормёжка с грантом - это кормёжка без обязательств, но есть одно условие. Вся эта схема базируется на вере, вернее в успешность развиваемой базы, которая в будущем станет фундаментом бизнеса. А как бизнес может оценить перспективность направления? Правильно - хайпом. Бизнес считает, что некое профессиональное сообщество аналитиков и просто целевой аудитории данных разработок - ему сообщит об успешности/не успешности. Таким образом чем больше из каждого утюга орут "это будущие" - тем больше грантов идёт в карман паразитам.

[@rustonelove]

@@vyorkin Точно так же - почему адепты выбирают ФП? Почему ФП бежит в веб? Правильно - конкуренция. Слабые бояться конкуренции и потому выбирают слабые области, слабую ЦА. Нужно орать там, где можно ничего не делать. Банальный пример - где и кому рассказывается о CompCert? В среде веб-неофитов, либо в среде тех же сишников? Правильно - в среде веб-неофитов. Они более фанатичны, более ничего не знают. Им можно впарить что угодно. Они мало что знают, потому как их область требует минимального кол-во специальных знаний. Но среди кого нужно о чём-то говорить, если ты хочешь развиваться и получить адекватный фидбек? Правильно - в среде условных сишников. Но почему этого не происходит? Причина может быть только одна и я назвал. В конечном итоге всё это можно свести к банальному сектантству. Каждый сектант будучи не способным выдерживать давление среды и конкуренции - живёт в рамках эхо-камеры. А далее фокус заключается в том, что слабых в мире много. И можно создать видимость, что эта эхо-камера и есть мир.

[@rustonelove]

@@vyorkin Просто последи за развитием всякого бездарного говна. Вон тут опять упоминается говнораст. Казалось бы, убийца С/С++. Системный язык. Убийца всего, но чем заняты его адепты? Как организовано его продвижение? Правильно - в среде веба, скриптухи и прочего. И всё это продвижение базируется на вранье, воровстве и прочих прелестях. И обмануть веб-ребёнка не составляет никакого труда. Он верит чему угодно. А далее уже неважно что есть на самом деле. Никому ненужно, что-бы эта скриптуха кого-то там убивала и заменяла. Нужен хайп, потому как хайп - это успех. Успех в контексте сбора бабла. А всё остальное никому ненужно.

[@montykay6003]

Что ты имеешь ввиду под "любая формальная верификация имеет в основе своей аксиоматическую природу"?

[@rustonelove]

17:55 - это именно пруф того, чем являются генерики не поверх "концепции единого типа". Шаблон(который был тут упомянут) - это на то и шаблон, что это НЕ ФУНКЦИЯ. Шаблон нужно превратить в функцию. Именно поэтому это и называется фичей языка, а генерики и ts фичей не является. Концепция шаблонов намного более мощная и фундаментальная. И создатели go запаривались куда больше создателей ts и любого другого скриптового языка. Но запаривались не так сильно как создатели того же, упомянутого тут, С++. Вначале нам из шаблона нужно создать функцию, а далее её вызвать. Это может быть автоматизировано, но это нужно всегда делать.

[@rustonelove]

14:44 - пошла идеологическая ангажированность. Именно ad-hoc является фундаментальной фичей языка. 15:00 - дальше можно не смотреть. Подобной конструкции вообще существовать в принципе - она требует динамической типизации. Об этом было сказано изначально(хотя лучше бы про память ничего не говорилось, что-бы не позориться). Если у нас есть память в которой записано "непонятно что", то мы никак не сможет это интерпретировать. Таким образом мы возвращаемся к концепции единого типа, которой и являются все динамические языки. Т.е. типизации у нас попросту нет.

[@alikhanmukhanaliyev2857]

Почему Вы считаете, что шаблонные функции(или методы) имеют место быть только в динамически типизированных языках?

[@rustonelove]

@@alikhanmukhanaliyev2857 Нигде я такого не писал. Всё как раз наоборот. Только шаблоны(т.е. ad-hoc) могут существовать в статическом языке. Всё остальное - только динамическое. К тому же "динамически" относится не только к "типизации".

[@nuxs]

@@rustonelove А как же Haskell, в котором сильная статическая типизация? В нём абсолютно валидны функции типа a -> a -> a, никакого привлечения при этом динамической типизации нет

[@rustonelove]

@@nuxs Есть там динамическая типизация. У тебя либо шаблоны, либо динамический полиморфизм. Третьего не дано. Подтипы это именно динамический полиморфизм. Любой полиморфизм называемый запартой полиморфизмом - является динамическим, кроме ad-hoc, который они полиморфизмом не называют.

[@rustonelove]

@@nuxs Моя группа в телеге: proriv_zaparti - я там писал об этом. Можешь поискать, либо проси я тебе найду. Что-либо объяснять здесь мне лень.

[@rustonelove]

30:15 - "значение зависит от типа" и показывает ts, в котором значение от типа никак не зависит(как и в любом другом скриптом(да и не только) языке).

[@vyorkin]

понятное дело, что System F к ts не имеет отношения :) вероятно, ему просто нужно было хоть какой-то пример показать на том языке, который понимает аудитория

[@rustonelove]

​@@vyorkin Ты плохо смотрел. Очевидно, что я рассматривал уже этот вариант. Но вот ведь незадача - 38:45 - он указывает это явно. И в этом проблема. Проблема в том, что пациент не способен даже осознать то, о чём говорит. И он пытается что-то кому-то рассказывать не понимая очевидных вещей. И в этом вся скриптуха. Самое интересное то, что почти ни один недоязычок показанный им не соответствует описанной им классификации. А мог бы взять С++.

[@vyorkin]

@@rustonelove А, да, теперь вижу (я не стал смотреть до конца это видео). Ну ладно, никто всё равно ничего не заметил

[@lvn5609]

У вас есть презентации, может где-нибудь преподаете?

[@rustonelove]

​@@lvn5609 Нет, но возможно когда-нибудь буду. Создал группу в телеге proriv_zaprti . Можешь спросить что-нибудь. Там напишу если что-то изменится.