Нет, Паскаль образец языка с полумерами в отношении системы типов, которые и в смысле контроля ничего особенного не дают, и лишнюю писанину делать заставляют.
О, здесь мы согласны. Но из этого есть простой вывод: не надо рассматривать паскаль (а не «не надо рассматривать статическую типизацию»).
До 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. Пожалуй, стоит переименовать в ⁄ по совету комментатора рядом.
Не ожидал увидеть «вывсёврёти» в этом контексте. Ну и апелляцию к каким-то личным вещам:
которым ты даже не являешься по их меркам, кстати
По чьим — их?
Я живу в красном округе канонично красного штата и периодически бываю там, где можно было бы ожидать максимальные концентрации «альт-райтов» — всякая тактикул тренировочная беготня, например (уж не говорю о простых пострелушках в простом тире). Я совершенно не скрываю, что я из России (мне надо напрягаться, чтобы убирать классический восточноевропейский акцент) и не скрываю, если речь об этом заходит, свои достаточно широкие семитские корни (а речь об этом заходит, например, потому что одна из моих основных пукалок — X95).
И знаете что? Всем пофиг. Russians are cool, even. «I always wanted to visit St. Petersburg.»
Если при этом армии и количество вооружения у бывших государство уменьшились
Почему оно уменьшилось? Как вы убедили туда субъекты-то вступать?
федерация получила легитимацию и возможность предотвращать вооружённые конфликты между субъектами, то войн будет меньше.
Или не будет, потому что федерализованное министерство внутренних разборок живёт на наличии вялых, но постоянных конфликтов, оправдывающих её существование, или на откатах от глобобоинга и глоборэйтеона, которым войнушка крутится — лавеха мутится.
Естественно придётся. Но это как бы принцип федерации.
Нет, конечно, и я вам привёл пример минимум одной федерации, где это не так.
Более того, те федерации (достаточно крупные, по крайней мере), где это так и отдельные штаты не вооружены, почему-то оказываются централизованными помойками. Может, потому что отдельно вооружённые субъекты федерации (от штатов до людей) на самом деле что-то значат в смысле демократической системы сдержек и противовесов.
Бывают. Но я бы сказал что это происходит заметно реже чем обычные войны.
Потому что обычные войны происходят по линиям государств. Если вы переобозначили государства как субъекты единой федерации, то вы автоматически переобозначили войны как гражданские, и всё.
Это просто игра в определения, не более. Вы можете дефиниционально определить запах дерьма как сладкий, но более съедобным оно от этого не станет.
И сколько эти вооружённые силы продержаться против армии США? Ну если два штата решат воевать между собой?
Само название "вооружённый конфликт" подразумевает наличие оружия. А война армий. Которые в федерации есть у федерации как целое и отсутствует у отдельных субъектов федерации.
Для начала вам придётся убедить вступающих в эту федерацию отказаться от собственных армий. Успехов.
Дальше, война ещё бывает гражданской. Вы просто переобозначите термины, и всё.
Дальше, даже в имеющихся федерациях (США, например) у ряда штатов есть свои вооружённые силы, не управляемые централизованно федералами, и 32 USC 109 это явно позволяет.
Фантазии о невооружённых субъектах федерации разбились о суровую реальность, увы.
Ну отлично. Тогда 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. Пожалуй, стоит переименовать в ⁄ по совету комментатора рядом.Интереснее, почему вы не хотите, ведь это ещё более приятная ситуация (это отчасти риторический вопрос, на него не нужно отвечать здесь).
Не ожидал увидеть «вывсёврёти» в этом контексте. Ну и апелляцию к каким-то личным вещам:
По чьим — их?
Я живу в красном округе канонично красного штата и периодически бываю там, где можно было бы ожидать максимальные концентрации «альт-райтов» — всякая тактикул тренировочная беготня, например (уж не говорю о простых пострелушках в простом тире). Я совершенно не скрываю, что я из России (мне надо напрягаться, чтобы убирать классический восточноевропейский акцент) и не скрываю, если речь об этом заходит, свои достаточно широкие семитские корни (а речь об этом заходит, например, потому что одна из моих основных пукалок — X95).
И знаете что? Всем пофиг. Russians are cool, even. «I always wanted to visit St. Petersburg.»
А почему бы не обсудить гипотетическую ситуацию «люди просто перестали хотеть воевать»? Реалистичность примерно такая же (и даже по тем же причинам).
Кажется, вы начинаете до чего-то догадываться (нет).
Почему оно уменьшилось? Как вы убедили туда субъекты-то вступать?
Или не будет, потому что федерализованное министерство внутренних разборок живёт на наличии вялых, но постоянных конфликтов, оправдывающих её существование, или на откатах от глобобоинга и глоборэйтеона, которым войнушка крутится — лавеха мутится.
Как первый день живёте, честное слово.
Нет, конечно, и я вам привёл пример минимум одной федерации, где это не так.
Более того, те федерации (достаточно крупные, по крайней мере), где это так и отдельные штаты не вооружены, почему-то оказываются централизованными помойками. Может, потому что отдельно вооружённые субъекты федерации (от штатов до людей) на самом деле что-то значат в смысле демократической системы сдержек и противовесов.
Потому что обычные войны происходят по линиям государств. Если вы переобозначили государства как субъекты единой федерации, то вы автоматически переобозначили войны как гражданские, и всё.
Это просто игра в определения, не более. Вы можете дефиниционально определить запах дерьма как сладкий, но более съедобным оно от этого не станет.
Двиганье гоалпостов. Это неважно.
С этим, очевидно, не все согласны даже в самих США, что на уровне штатов, что на уровне отдельных людей, тем более.
Для начала вам придётся убедить вступающих в эту федерацию отказаться от собственных армий. Успехов.
Дальше, война ещё бывает гражданской. Вы просто переобозначите термины, и всё.
Дальше, даже в имеющихся федерациях (США, например) у ряда штатов есть свои вооружённые силы, не управляемые централизованно федералами, и 32 USC 109 это явно позволяет.
Фантазии о невооружённых субъектах федерации разбились о суровую реальность, увы.