Я хочу видеть, возвращает ли функция результат сейчас, или её надо подождать, прям в её типах, и хочу, чтобы компилятор мне говорил, если мои ожидания расходятся с реальностью.
Асинхронность — это просто один из эффектов. Эффекты полезно видеть в типах. Особенно в большой кодовой базе.
Настоящий программист должен точно знать, сколько байт памяти выделяет его код, в какие машинные инструкции он преобразуется
А плюсы этого больше не дают, всё. Без оптимизаций у вас std::move может быть отдельной функцией (а может и не быть), но без оптимизаций на плюсах на практике никто не пишет (кроме совсем настоящих программистов, пишущих такой код, что глупый оптимизатор его ломает), а с оптимизациями — там такая же магия, как в каком-нибудь JIT-языке.
уметь писать собственные аллокаторы, контейнеры и т.д.
Контейнеры-то легко, и это можно делать на любом языке, а аллокаторы в плюсах — не стоит вскрывать эту тему. Про это на конференциях доклады делают, причём не об алгоритмике и машинных особенностях, а об особенностях языка (типа, как пропагейтить аллокатор std::vector'а в std::string'и, которые там лежат).
И, кстати, почему настоящий программист должен машинные инструкции и аллокаторы? Почему не категориальную семантику его программы и монадические регионы?
Когда я открываю реальный промышленный код на хаскеле, то там нормально всё с newtype.
На плюсах, в принципе, тоже. Правда, когда я собеседуюсь на приплюснутого ассенизатора, то при написании кода на интервью я вполне себе говорю (и пишу) о типобезопасности и смотрю на реакцию интервьювера, поэтому у меня тут не совсем репрезентативная выборка.
Это, конечно, отсылка к личному опыту и вообще немного выпендрёж, но по-другому отвечать на тезисы «в реальном продакшен-коде не используются несовместимые алиасы типов / тесты / системы контроля версий» тяжеловато.
Другое дело, что он не ко всем проектам подходит (я вот, например, сегодня добавил поддержку нового обрабатываемого типа данных в выполняющуюся программу прямо на ходу, не останавливая её)
Мне как-то (не) везёт писать такой код, где между мной и продом либо несколько слоёв стейджинга, либо это вообще библиотеки и вещи уровня «тайпчекер и интерпретатор для языка смарт-контрактов», где «менять программу при выполнении» не имеет особого прикладного смысла.
Поэтому, короче, я не могу эффективно спорить на этой территории за отсутствием наработанных паттернов. Какой тип добавили? Зачем? В чём конкретно это добавление выражается? Где бы вы упёрлись в выразительном статически типизированном языке? ХЗ.
Если выкинуть из вашей фразы слово «паскалевской», то не соглашусь: приблизит.
В какой версии буста там STRONG_TYPEDEF появилось? Судя по копирайту в хедере (2002-й год) — рано появилось, может, даже раньше boost.lambda и всего такого. Надо, наверное, зачем-то людям разделять типы, чтобы неявных преобразований и ошибочных присваиваний не было.
Нет, Паскаль образец языка с полумерами в отношении системы типов, которые и в смысле контроля ничего особенного не дают, и лишнюю писанину делать заставляют.
О, здесь мы согласны. Но из этого есть простой вывод: не надо рассматривать паскаль (а не «не надо рассматривать статическую типизацию»).
До JS и CPython.
У меня есть разные знакомые, работающие в веб-экосистеме, причём в компаниях от местных консалтинг-бодишопов на три боди до фаанга, и если судить по их рассказам, то проектов на чистом JS, без тайпскрипта, не встречалось уже очень давно.
Другое дело, что в части проектов на TS половина типов — any, но это, гм, другое дело.
Я хочу знать, что написал ерунду, ещё до деплоя в прод (в идеале — вот прям когда я пишу конкретно эту строку, прям в IDE), а не в три часа ночи оповещением с прода, что ровно здесь случилась редкая комбинация условий, которая пошла по тому бранчу, который привёл к прибавлению единицы к адресу.
Религиозной традицией я назвал декларации типов переменных.
А почему вы смешиваете отсутствие типизации (нет, я никогда не буду в серьёзных разговорах использовать оксюморон «динамическая типизация») и неявную типизацию?
Более того, статическая типизация – это шаг к нестрогой типизации, то есть к неявным преобразованиям типов. Даже в Паскале
Паскаль у нас теперь образец языка с сильной и выразительной системой типов?
Реальная востребованность их, как видим, невелика.
Ну куда уж TS и mypy до Lisp и Scheme, понятное дело.
Однако в качестве примеров почему-то приводите задачи ввода-вывода, где статическая типизация не имеет существенного значения. Вы же не предлагаете на самом деле раскидывать нюансы работы с внешним миром по всей программе, вместо того чтобы обучать отрабатывать сериализацию/десериализацию данных на границах слоев?
Статическая типизация как раз помогает доказать убедиться, что на границах слоя сериализация/десериализация была выполнена, и что все части слоя согласны с тем, что именно должно было быть (де)сериализовано.
Вы не подумайте, я не против статической типизации, а очень даже за. Кстати, скажите, если у переменной xs тип Vect n Int (n — число), а ys : Vect m Int, то какой тип у конкатенации xs и ys — Vect (n + m) Int или Vect (m + n) Int? В ряде теорий это два разных типа.
Это перевод "Оптического журнала", ведущего журнала в этой области.
А ведущесть в области в мире наглядно видна по параметрам переводной версии, да.
Впрочем, найти какие-то наукометрические показатели у исходной русскоязычной версии исключительно тяжело. Какие-то цифры есть только здесь: https://geomag.izmiran.ru/files/jrating-IF2.pdf , и там у русскоязычной версии IF — почти те же 0.62. Журнал в надёжной компании таких именитых и серьёзных изданий, как «Вестник СГУГиТ (Сибирского государственного университета геосистем и технологий)» и «Анналы аритмологии».
Конечно, по IF самому по себе нельзя судить, его нужно нормировать на тему, но квартилей-то нет!
"Компьютерная оптика" (в ней у меня 2 статьи) имеет Q1
Как вы квартили русскоязычных журналов находите? Поделитесь, пожалуйста, мне для личного интереса.
Впрочем, в списке выше IF, конечно, тоже получше, целых 0.695.
и не имеет переводной версии. Другие статьи - Q2, К1
Но ссылок на них нет, читателю предлагается найти их самостоятельно поиском по этой теме.
Вы в библиографии ссылки тоже так делаете — «[7] найдите поиском по этой теме»? Если не секрет, какой bibtex-ключ соответствует этому виду ссылок?
Только их не существует (особенно если рассматривать «просто множества»).
По крайней мере, не существует в ZF. В ZF нет ни пар, ни троек, ни других n-туплов как примитивов, там есть только множества. Пары там определяются как, упрощая, синтаксический шорткат: например, можно определить (и дальше в ZF можно доказать, что это определение ведёт себя как ожидается, вроде ), или как (это эквивалентное определение, но ему ЕМНИП не нужна аксиома регулярности из ZF).
Соответственно, пара и пара — это сильно разные множества. И вместе с — это тоже сильно разные множества (которые в ZF строятся такими-то костылями, и данные вами в прошлом комментарии логические формулы не имеют прямого отношения к определению этих множеств, хотя их и можно получить после упрощения, но β-эквивалентность — это не синтаксическое равенство). Но, конечно, в школьной (и прикладной вузовской) математике никто не вспоминает про ZF или другие основания математики, поэтому там это всё неважно, и можно интуитивно считать эти множества одинаковыми.
В теоркате, кстати, декартовых произведений может быть (бесконечно) много (например, в Set A×B — это и множество пар вместе с двумя очевидными проекциями, и множество с теми же проекциями, но наоборот, и множество с чуть менее очевидными проекциями), поэтому их там тоже обычно рассматривают с точностью до изоморфизма.
Но, разумеется, можно создать более сложную структуру - допустим какое-то "множество с типами" и с ним уже делать различия. Вот интересно как вы это формально определите. В принципе, я уверен, это должно быть уже сделанно в каком-нибудь раннем источнике.
Теория типов, собсна, уже тоже придумана. Что-нибудь в духе Мартина-Лёфа будет выглядеть примерно как:
Постулируем существование конструктора типов ×: A : Type, B : Type ⊢ A × B : Type
Постулируем конструктор термов ⟨⟩: a : A, b : B ⊢ ⟨a, b⟩ : A × B
Постулируем элиминатор. Если не вскрывать тему с зависимыми типами и зависимыми элиминаторами, то проще всего через проекции: A × B : Type ⊢ π₁ : A × B → A A × B : Type ⊢ π₂ : A × B → B
Постулируем операционную семантику: π₁ (⟨ a, b ⟩) ⇝ a π₂ (⟨ a, b ⟩) ⇝ b
В зависимости от конкретной теории типов (экстенсиональная/интенсиональная, есть ли UIP, всякое такое вот) может быть полезно постулировать η-равенство: ∀ p : A × B. ⟨ π₁ p, π₂ p ⟩ ≡ p. Кстати, даже тут уже, если присмотреться, видны намёки на некоторые проблемы с единственностью, пусть и слегка другого рода.
Дальше ещё изоморфизм ∀ X. (X → A × B) ≅ (X → A) × (X → B), который по факту выражает привычное универсальное свойство произведений.
У них там ещё есть пара забавных песен (nigger и the faggot in you), названия которых в давних нулевых цензурились на торрент-трекерах, и в именах файлов, и в тегах.
У моих любимейших Structures есть альбом «Divided By», на котором заключительный трек называется «/», который у меня на ФС называется почему-то 10 - ,.flac. Пожалуй, стоит переименовать в ⁄ по совету комментатора рядом.
Чем плохо?
Я хочу видеть, возвращает ли функция результат сейчас, или её надо подождать, прям в её типах, и хочу, чтобы компилятор мне говорил, если мои ожидания расходятся с реальностью.
Асинхронность — это просто один из эффектов. Эффекты полезно видеть в типах. Особенно в большой кодовой базе.
А плюсы этого больше не дают, всё. Без оптимизаций у вас
std::moveможет быть отдельной функцией (а может и не быть), но без оптимизаций на плюсах на практике никто не пишет (кроме совсем настоящих программистов, пишущих такой код, что глупый оптимизатор его ломает), а с оптимизациями — там такая же магия, как в каком-нибудь JIT-языке.Контейнеры-то легко, и это можно делать на любом языке, а аллокаторы в плюсах — не стоит вскрывать эту тему. Про это на конференциях доклады делают, причём не об алгоритмике и машинных особенностях, а об особенностях языка (типа, как пропагейтить аллокатор
std::vector'а вstd::string'и, которые там лежат).И, кстати, почему настоящий программист должен машинные инструкции и аллокаторы? Почему не категориальную семантику его программы и монадические регионы?
Что значит «новый тип»? Какие типы были, и какой тип — новый?
Когда я открываю реальный промышленный код на хаскеле, то там нормально всё с
newtype.На плюсах, в принципе, тоже. Правда, когда я собеседуюсь на приплюснутого ассенизатора, то при написании кода на интервью я вполне себе говорю (и пишу) о типобезопасности и смотрю на реакцию интервьювера, поэтому у меня тут не совсем репрезентативная выборка.
Это, конечно, отсылка к личному опыту и вообще немного выпендрёж, но по-другому отвечать на тезисы «в реальном продакшен-коде не используются несовместимые алиасы типов / тесты / системы контроля версий» тяжеловато.
Мне как-то (не) везёт писать такой код, где между мной и продом либо несколько слоёв стейджинга, либо это вообще библиотеки и вещи уровня «тайпчекер и интерпретатор для языка смарт-контрактов», где «менять программу при выполнении» не имеет особого прикладного смысла.
Поэтому, короче, я не могу эффективно спорить на этой территории за отсутствием наработанных паттернов. Какой тип добавили? Зачем? В чём конкретно это добавление выражается? Где бы вы упёрлись в выразительном статически типизированном языке? ХЗ.
Если выкинуть из вашей фразы слово «паскалевской», то не соглашусь: приблизит.
В какой версии буста там
STRONG_TYPEDEFпоявилось? Судя по копирайту в хедере (2002-й год) — рано появилось, может, даже раньше boost.lambda и всего такого. Надо, наверное, зачем-то людям разделять типы, чтобы неявных преобразований и ошибочных присваиваний не было.А что с ней?
Я могу скомпилировать модуль, определяющий эту функцию, без знания конкретного типа.
Я могу скомпилировать другой модуль, скажем,
тоже без каких-либо конкретных типов.
Ну отлично. Тогда ML-стайл вывод типов вам норм?
О, здесь мы согласны. Но из этого есть простой вывод: не надо рассматривать паскаль (а не «не надо рассматривать статическую типизацию»).
У меня есть разные знакомые, работающие в веб-экосистеме, причём в компаниях от местных консалтинг-бодишопов на три боди до фаанга, и если судить по их рассказам, то проектов на чистом JS, без тайпскрипта, не встречалось уже очень давно.
Другое дело, что в части проектов на TS половина типов —
any, но это, гм, другое дело.Ну так это ключевой момент.
Я хочу знать, что написал ерунду, ещё до деплоя в прод (в идеале — вот прям когда я пишу конкретно эту строку, прям в IDE), а не в три часа ночи оповещением с прода, что ровно здесь случилась редкая комбинация условий, которая пошла по тому бранчу, который привёл к прибавлению единицы к адресу.
Не понял. Можно пример?
А почему вы смешиваете отсутствие типизации (нет, я никогда не буду в серьёзных разговорах использовать оксюморон «динамическая типизация») и неявную типизацию?
Паскаль у нас теперь образец языка с сильной и выразительной системой типов?
Ну куда уж TS и mypy до Lisp и Scheme, понятное дело.
Когда именно я узна́ю, что я где-то случайно попытался прибавить единицу к почтовому адресу?
Статическая типизация как раз помогает
доказатьубедиться, что на границах слоя сериализация/десериализация была выполнена, и что все части слоя согласны с тем, что именно должно было быть (де)сериализовано.…быть функцией не A → B, а A → 𝒫B.
Вы не подумайте, я не против статической типизации, а очень даже за. Кстати, скажите, если у переменной
xsтипVect n Int(n — число), аys : Vect m Int, то какой тип у конкатенацииxsиys—Vect (n + m) IntилиVect (m + n) Int? В ряде теорий это два разных типа.А ведущесть в области в мире наглядно видна по параметрам переводной версии, да.
Впрочем, найти какие-то наукометрические показатели у исходной русскоязычной версии исключительно тяжело. Какие-то цифры есть только здесь: https://geomag.izmiran.ru/files/jrating-IF2.pdf , и там у русскоязычной версии IF — почти те же 0.62. Журнал в надёжной компании таких именитых и серьёзных изданий, как «Вестник СГУГиТ (Сибирского государственного университета геосистем и технологий)» и «Анналы аритмологии».
Конечно, по IF самому по себе нельзя судить, его нужно нормировать на тему, но квартилей-то нет!
Как вы квартили русскоязычных журналов находите? Поделитесь, пожалуйста, мне для личного интереса.
Впрочем, в списке выше IF, конечно, тоже получше, целых 0.695.
Но ссылок на них нет, читателю предлагается найти их самостоятельно поиском по этой теме.
Вы в библиографии ссылки тоже так делаете — «[7] найдите поиском по этой теме»? Если не секрет, какой bibtex-ключ соответствует этому виду ссылок?
Этим конкретным математиком или в математике вообще? Если первое, то почему?
Переводной, IF 0.6, в математике — Q4 (если верить этому). То есть, мусорный журнал.
Я на четвёртом-пятом курсах опубликовал несколько статей в Q3/Q4-журналах, но это не делает меня математиком, или эффективным, или ещё кем-то там.
Только их не существует (особенно если рассматривать «просто множества»).
По крайней мере, не существует в ZF. В ZF нет ни пар, ни троек, ни других n-туплов как примитивов, там есть только множества. Пары там определяются как, упрощая, синтаксический шорткат: например, можно определить
(и дальше в ZF можно доказать, что это определение ведёт себя как ожидается, вроде 
), или как 
(это эквивалентное определение, но ему ЕМНИП не нужна аксиома регулярности из ZF).
Соответственно, пара
и пара 
— это сильно разные множества. И 
вместе с 
— это тоже сильно разные множества (которые в ZF строятся такими-то костылями, и данные вами в прошлом комментарии логические формулы не имеют прямого отношения к определению этих множеств, хотя их и можно получить после упрощения, но β-эквивалентность — это не синтаксическое равенство). Но, конечно, в школьной (и прикладной вузовской) математике никто не вспоминает про ZF или другие основания математики, поэтому там это всё неважно, и можно интуитивно считать эти множества одинаковыми.
В теоркате, кстати, декартовых произведений может быть (бесконечно) много (например, в Set A×B — это и множество пар
вместе с двумя очевидными проекциями, и множество 
с теми же проекциями, но наоборот, и множество 
с чуть менее очевидными проекциями), поэтому их там тоже обычно рассматривают с точностью до изоморфизма.
Теория типов, собсна, уже тоже придумана. Что-нибудь в духе Мартина-Лёфа будет выглядеть примерно как:
Постулируем существование конструктора типов ×: A : Type, B : Type ⊢ A × B : Type
Постулируем конструктор термов ⟨⟩: a : A, b : B ⊢ ⟨a, b⟩ : A × B
Постулируем элиминатор. Если не вскрывать тему с зависимыми типами и зависимыми элиминаторами, то проще всего через проекции:
A × B : Type ⊢ π₁ : A × B → A
A × B : Type ⊢ π₂ : A × B → B
Постулируем операционную семантику:
π₁ (⟨ a, b ⟩) ⇝ a
π₂ (⟨ a, b ⟩) ⇝ b
В зависимости от конкретной теории типов (экстенсиональная/интенсиональная, есть ли UIP, всякое такое вот) может быть полезно постулировать η-равенство: ∀ p : A × B. ⟨ π₁ p, π₂ p ⟩ ≡ p.
Кстати, даже тут уже, если присмотреться, видны намёки на некоторые проблемы с единственностью, пусть и слегка другого рода.
Дальше ещё изоморфизм ∀ X. (X → A × B) ≅ (X → A) × (X → B), который по факту выражает привычное универсальное свойство произведений.
О, Clawfinger… Верните мне мой 2007-й.
У них там ещё есть пара забавных песен (nigger и the faggot in you), названия которых в давних нулевых цензурились на торрент-трекерах, и в именах файлов, и в тегах.
У моих любимейших Structures есть альбом «Divided By», на котором заключительный трек называется «/», который у меня на ФС называется почему-то
10 - ,.flac. Пожалуй, стоит переименовать в ⁄ по совету комментатора рядом.