Вячеслав Шебанов - Системы типов в двух словах
HTML-код
- Опубликовано: 28 мар 2019
- Ближайшая конференция - HolyJS 2024 Autumn, 7 ноября (online), 14-15 ноября (Санкт-Петербург + трансляция).
Подробности и билеты: jrg.su/K18Cxd
- -
. . История систем типов. Анализ текущего состояния языков. Взгляд в будущее системы типов.
Лямбда-исчисление Черча. Лямбда-куб. Линейные типы.
Глубоко. Основательно. Доходчиво.
Прогоны доклада расширили сознание некоторых членов ПК.
Приложения на JS становятся больше и сложнее, а инструменты вроде Flow и TypeScript набирают популярность. Статическая типизация становится обычной темой в JS-мире, при этом мы редко задаем себе вопрос, почему эти типы выглядят так или иначе. Как формировались системы типов современных языков, какая теория за ними лежит и куда все это движется? Попробуем коротко об этом поговорить. 
Наука
Капец как годно.
Засыпаться через 5 минут. Годнота годнот.
Духота
35:40 - никакого отношения к типизации не имеет. Тут существует одна фундаментальная проблема. Такого уровня компилятор, как CompCert, нахрен никому ненужен и в нём итак не будет ошибок. К тому же, нужно понимать, что любая формальная верификация имеет в основе аксиоматическую природу. Очевидно, что никак нельзя доказать верность аксиомы. Это не имеет смысла. Если говорить более широко, то можно определить какую-либо модель и доказать соответствие логики(написанной в программе) логике определённой в данной модели. Именно этим занимается верификация. Проблемы тут очевидны. Всё имеет аксиоматическую природу(что модель, что доказательства) и как следствие это вообще ничего не доказывает. Подобная проблема неразрешима. Любая верификация зависит от верификации и далее по рекурсии. Любая верификация лишь условность. Если говорить проще - механизм отмывания бабла с грантов, путём производства бесполезного мусора.
все посылки, вроде бы, верные, но не понятно как вы пришли к
> механизм отмывания бабла с грантов, путём производства бесполезного мусора
@@vyorkin Да очень просто. Если что-то не имеет смысла и применения - зачем оно нужно? Зачем о нём рассказывать, зачем рассказывать аудитории, которая нихрена не понимает в теме? Это что-то не имеет объективных предпосылок к существованию, а его адепты и ваятели не имеют права существовать в том качестве, котором о себе заявляют.
В конечном итоге возможно два варианта. Люди либо не понимают, либо идиоты. Очевидно, что если они идиоты - это ломает все устои общества и мы можем на это ссылаться. Если они не понимают - есть два варианта. В любом случае какое-то развитие быть должно. Но мы его не видим. Все эти методички как созданы в 70 лет назад - так слово в слово и ретранслируются. И вот они два варианта - либо идиоты, либо существуют скрытые мотивы. Первое мы отрицаем. Остаётся второе.
А какие могут быть скрытые мотивы?
Эти мотивы очевидны. Каждый повязанных с тем же CompCert, живущий на грантах, не состоятелен вне это схемы. По крайне мере нет свидетельств обратному. Кормёжка с грантом - это кормёжка без обязательств, но есть одно условие. Вся эта схема базируется на вере, вернее в успешность развиваемой базы, которая в будущем станет фундаментом бизнеса.
А как бизнес может оценить перспективность направления? Правильно - хайпом. Бизнес считает, что некое профессиональное сообщество аналитиков и просто целевой аудитории данных разработок - ему сообщит об успешности/не успешности.
Таким образом чем больше из каждого утюга орут "это будущие" - тем больше грантов идёт в карман паразитам.
@@vyorkin Точно так же - почему адепты выбирают ФП? Почему ФП бежит в веб? Правильно - конкуренция. Слабые бояться конкуренции и потому выбирают слабые области, слабую ЦА. Нужно орать там, где можно ничего не делать.
Банальный пример - где и кому рассказывается о CompCert? В среде веб-неофитов, либо в среде тех же сишников? Правильно - в среде веб-неофитов. Они более фанатичны, более ничего не знают. Им можно впарить что угодно. Они мало что знают, потому как их область требует минимального кол-во специальных знаний.
Но среди кого нужно о чём-то говорить, если ты хочешь развиваться и получить адекватный фидбек? Правильно - в среде условных сишников. Но почему этого не происходит? Причина может быть только одна и я назвал.
В конечном итоге всё это можно свести к банальному сектантству. Каждый сектант будучи не способным выдерживать давление среды и конкуренции - живёт в рамках эхо-камеры. А далее фокус заключается в том, что слабых в мире много. И можно создать видимость, что эта эхо-камера и есть мир.
@@vyorkin Просто последи за развитием всякого бездарного говна. Вон тут опять упоминается говнораст. Казалось бы, убийца С/С++. Системный язык. Убийца всего, но чем заняты его адепты? Как организовано его продвижение? Правильно - в среде веба, скриптухи и прочего. И всё это продвижение базируется на вранье, воровстве и прочих прелестях. И обмануть веб-ребёнка не составляет никакого труда. Он верит чему угодно.
А далее уже неважно что есть на самом деле. Никому ненужно, что-бы эта скриптуха кого-то там убивала и заменяла. Нужен хайп, потому как хайп - это успех. Успех в контексте сбора бабла. А всё остальное никому ненужно.
Что ты имеешь ввиду под "любая формальная верификация имеет в основе своей аксиоматическую природу"?
14:44 - пошла идеологическая ангажированность. Именно ad-hoc является фундаментальной фичей языка. 15:00 - дальше можно не смотреть. Подобной конструкции вообще существовать в принципе - она требует динамической типизации. Об этом было сказано изначально(хотя лучше бы про память ничего не говорилось, что-бы не позориться). Если у нас есть память в которой записано "непонятно что", то мы никак не сможет это интерпретировать. Таким образом мы возвращаемся к концепции единого типа, которой и являются все динамические языки. Т.е. типизации у нас попросту нет.
Почему Вы считаете, что шаблонные функции(или методы) имеют место быть только в динамически типизированных языках?
@@alikhanmukhanaliyev2857 Нигде я такого не писал. Всё как раз наоборот. Только шаблоны(т.е. ad-hoc) могут существовать в статическом языке. Всё остальное - только динамическое.
К тому же "динамически" относится не только к "типизации".
@@rustonelove А как же Haskell, в котором сильная статическая типизация? В нём абсолютно валидны функции типа a -> a -> a, никакого привлечения при этом динамической типизации нет
@@nuxs Есть там динамическая типизация. У тебя либо шаблоны, либо динамический полиморфизм. Третьего не дано. Подтипы это именно динамический полиморфизм. Любой полиморфизм называемый запартой полиморфизмом - является динамическим, кроме ad-hoc, который они полиморфизмом не называют.
@@nuxs Моя группа в телеге: proriv_zaparti - я там писал об этом. Можешь поискать, либо проси я тебе найду. Что-либо объяснять здесь мне лень.
30:15 - "значение зависит от типа" и показывает ts, в котором значение от типа никак не зависит(как и в любом другом скриптом(да и не только) языке).
понятное дело, что System F к ts не имеет отношения :) вероятно, ему просто нужно было хоть какой-то пример показать на том языке, который понимает аудитория
@@vyorkin Ты плохо смотрел. Очевидно, что я рассматривал уже этот вариант. Но вот ведь незадача - 38:45 - он указывает это явно. И в этом проблема. Проблема в том, что пациент не способен даже осознать то, о чём говорит. И он пытается что-то кому-то рассказывать не понимая очевидных вещей. И в этом вся скриптуха.
Самое интересное то, что почти ни один недоязычок показанный им не соответствует описанной им классификации. А мог бы взять С++.
@@rustonelove А, да, теперь вижу (я не стал смотреть до конца это видео). Ну ладно, никто всё равно ничего не заметил
У вас есть презентации, может где-нибудь преподаете?
@@lvn5609 Нет, но возможно когда-нибудь буду. Создал группу в телеге proriv_zaprti . Можешь спросить что-нибудь. Там напишу если что-то изменится.
17:55 - это именно пруф того, чем являются генерики не поверх "концепции единого типа". Шаблон(который был тут упомянут) - это на то и шаблон, что это НЕ ФУНКЦИЯ. Шаблон нужно превратить в функцию. Именно поэтому это и называется фичей языка, а генерики и ts фичей не является. Концепция шаблонов намного более мощная и фундаментальная. И создатели go запаривались куда больше создателей ts и любого другого скриптового языка. Но запаривались не так сильно как создатели того же, упомянутого тут, С++. Вначале нам из шаблона нужно создать функцию, а далее её вызвать. Это может быть автоматизировано, но это нужно всегда делать.