Комментарии 1975

Задвиньте эту статью в черновики, автор явно провоцирует холивар.

А вы посмотрите на остальные статьи этого эпатажного автора. Вы думаете, он опомнится на 27-ой разжигающей статье?)

Мне особенно нравится трезвая оценка с опозданием —
Пару лет назад я уже писал о типизации, но тогда я был молодой, глупый и трусливый

Остается немного подождать для оценки уже этой статьи.

Афигенно! Автор, жги! * обновляет страницу, дабы насладится холиваром *

Холивар, вроде не пятница.
Динамическую типизацию зачем то придумал и мало того она жива до сих пор, обычно то что никому не нужно умирает на задворках истории.
Но удивительное дело в динамических появляются типы, а в типизированных val.
Такие дела.
Истина где-то рядом, наверно по середине.
И наверно не всех надо по одну гребенку.

Удивительный у автора талант писать статьи, которые вызывают эмоции от полного принятия до лютой неприязни.

val это не динамическая типизация, а лишь вывод типов. Вот почему то многие не понимают принципиальной разницы

Думаю просто смешиваются в голове все варианты: статическая/динамическая, сильная/слабая, явная/неявная.
Динамическую типизацию зачем то придумал и мало того она жива до сих пор, обычно то что никому не нужно умирает на задворках истории.

Как говорил один мой знакомый:


Так ведь значит же. Динамика это просто атавизм из 90-х, когда языки с нормальными системами типов делать не умели, а писать на вербозном говне не хотелось.

А ЯП с нормальными системами типов начали появляться относительно недавно.

А можете привести примеры ЯП с нормальными системами типов?

Ни в коем случае не троллинг, действительно интересно.

Haskell (хотя 0xd34df00d щас опять будет ворчать, что выразительности не хватает), Idris, вроде бы Scala (хотя точно сказать не могу), с некоторой натяжкой — Rust.

Странно (про Haskell), там ведь и Хиндли-Милнер, и алгебраические типы…

Зависимых типов нет, линейных типов нет, row polymoprhism нет. Ещё говорят, что модульная система так себе, но я же не окамлист, чтобы так считать.

Первые два скоро подвезут. Только-только появилось понимание как это сделать чтобы потом компилятор не треснул.
Третье доступно в виде библиотек.

Первое (особенно с консистентностью) подвезут очень нескоро. Про второе (пропозал от tweag, по крайней мере) я слышал ещё три года назад — как там с ним прогресс?


Заменять row polymorphism библиотеками (уж не classy lenses ли и им подобное?) — это костыли, хоть и не такие, как делать вид, что у нас есть зависимые типы через синглтоны.

Мне ещё регулярно (в чужом коде) встречается Vinyl. Но конечно это всё полимеры...

  1. Динамика это просто атавизм из 90-х, когда языки с нормальными системами типов делать не умели
  2. Haskell, 1990 год.
  3. Python, 1991 год.

Как эти три вещи могут одновременно укладываться в голове? Видимо ваш знакомый не знает одной из них.


Не получится убедить, что Haskell — это подходящий язык для разработки, а Python — не подходящий.


Лучшее, что может быть — это типизация по требованию. Когда нужно, беру и использую. Когда не нужно — избегаю кучи бойлерплейта.

Все таки Haskell это полигон для экспериментов, который тем не менее дорос до прода, а активно вывод типов начал проникать в индустрию только в 10ых годах.

Ну так хаскель 90-го года и хаскель совеременный — это очень разные языки.

Не получится убедить, что Haskell — это подходящий язык для разработки

Почему?


а Python — не подходящий.

Зависит от проекта. Как тонкий слой клея между уже готовыми библиотеками он прекрасен, да.

Лучшее, что может быть — это типизация по требованию. Когда нужно, беру и использую. Когда не нужно — избегаю кучи бойлерплейта.

Если бы она ещё работала… Потому что когда тебе нужно, а в апстриме не нужно — вылезай, приехали.

Но ведь в статике бойлерплэйта, как правило, меньше. Можно одновременно получить и безопасность, и читаемость.

Как правило больше, на мой взгляд. По крайней мере если брать языки типа C++, C#, Java, TypeScript

Чтобы прочитать ваш комментарий, мне пришлось загрузить всю статью и около двух тысяч других комментариев. Вы не могли бы более аргументированно отвечать? Ну, чтобы не зря атмосферу греть.

чтобы вам ответить приходится набирать тест вслепую, что не совсем удобно

Структуры и классы никак не делят типы и не мешают. Это лишь определяет reference type/value type и системе типов до этого нет никакого дела.

Есть дело мне при написании программ, потому что мне надо думать, где будет глубокое копирование, а где — поверхностное, где меняется аргумент, а где — его копия. И в дженериках подобное разделение обычно аукается.

В C# тоже самое. По факту, структуры придуманы не от хорошей жизни, а ради перфоманса. И мутабельные структуры — это дорога в ад (во всяком случае в C#). А если структура не мутирует, то думать про копирование особо не надо.

Ну скорее всего придётся об этом думать, язык все-таки позиционируется как более менее быстрый и нежручий.

За мутабельные структуры компилятор всегда подскажет. Если один раз понять как работают reference type/value type в свифте и использовать их где нужно и как нужно, то никаких проблем не будет возникать, а компилятор в случае чего все-равно заботливо предостережет. Все четко и явно в этом плане. И не придется переживать за глубокое/поверхностное копирование.
А что не так с дженериками?
В самом простом варианте все по-умолчанию imutable, потому что компилятор не будет знать что именно туда придет, а для мутабельности можно и inout или var в нужном месте указать.
В случаях посложнее (generic constraints) у вас в протоколе все ограничения описываются, вплоть до указания что этот протокол только для классов.
Не знаю с какими проблемами вы сталкивались, но по этому поводу у меня голова ни разу не болела.

К сожалению он существует только в яблочной экосистеме.

К счастью, его можно поставить и использовать практически на все, кроме винды. На малинку вот поставил недавно.

87% это в целом по миру или в сфере разработки? Я видел винду только у тех разработчиков, которым по каким-то причинам было лень ставить линукс. Возможно страх перед неизведанным.

На самом деле почти у всех знакомых мне разработчиков в экосистеме .NET и 1С винда — основная ось для этой разработки. Линуксы — только для кроссплатформенных задач.

На самом деле у 100% разрабочтиков в экосистеме Яббле стоят XCode и MacOS — основная ось для этой разработки. Винды — только для задач HR/серкретарш и бухгалтерии.

Можно, но на практике я его видел меньше, чем перла в новых проектах или чего ещё. Даже в резюме у людей не видел свифт, наверное, ни разу (зато видел даже пролог, не говоря о хаскелях с растами).

Так исторически сложилось, что на свифт перешли все кто писал на ObjC, а он существовал в рамках эппловских операционок, поэтому большинство пишущих на нем — маководы. А так как язык молодой, то пока еще не успел выбиться из нативной разработки под MacOS/iOS (в плане популярности), хоть эппл и делает многое, чтобы он мог быть универсальным. Бекенды эти ваши давно уже можно писать, с ардуинками играться, TensorFlow переходит на него как на основной язык. Дайте малышу время)

Бекенды эти ваши давно уже можно писать

Можно, но зачем? Для высокой производительности у меня есть плюсы или раст, а когда производительность не составляет 99% от всех критериев, то можно и на хаскеле.

хоть эппл и делает многое, чтобы он мог быть универсальным.
А что именно он делает? Мне просто интересно. Компилятор предоставил? Так Objective C всегда был под разные платформы (стараниями Столлмана, правда, вопреке желанию Джобса… но был).

Каких-либо попыток сделать разумную среду, которую можно использовать вне экосистемы Apple я не наблюдаю… да неясно какой в ней мог бы быть смысл: Apple же нужно сделать так, всё-таки, чтобы «хомячки» не разбежались с его платформы, а не чтобы кто-то вне её творил…

TensorFlow переходит на него как на основной язык
Кто сказал? Откуда уверенность, что из этого не получится очередная стелла на известном сайте?
Fullstack-разработка на swift вполне себе цель. В смысле — клиент под ios + серверсайд под линукс.

Про TensorFlow Google сказал, мол уходят с питона на свифт. Потому что быстрый, безопасный и: https://en.wikipedia.org/wiki/Differentiable_programming


Если появится очередная стелла, свифт от этого никак не пострадает. Но это не отменяет факта, что свифт уже не только язык для “хомячков” с платформ Apple.

Про TensorFlow Google сказал, мол уходят с питона на свифт
Где, когда, а главное, кто? Те, кто его разработал? Там им свою разработку и внутри Гугла надо как-то продавать — ещё бы они не излучали оптимизм.

Если появится очередная стелла, свифт от этого никак не пострадает.
Пострадает, конечно. Причём уже похоже, что не «если», а «когда». Итересно только — релиз успеют сделать или прямо из беты в небытиё?

Но это не отменяет факта, что свифт уже не только язык для “хомячков” с платформ Apple.
Та же самая история, что и с Objective C, на самом деле: когда Objective C только появился — народ разработал GNUstep и были даже попытки куда-то это всё приспособить. Однако со временем всё заглохло и, насколько я знаю, Cocoa уже никто никуда портировать особо не пытался — так, кой-какие обрезки для игрушек.

То же самое и здесь: каждая неудача применить Swift куда-нибудь, кроме iOS и macOS будет подчёркивать «неразрывную связь»: Swift == Apple, Apple == Swift.

Слабо себе понимаю причину захоронения S4TF. Ребята из Google просто искали наиболее подходящий язык и выбрали Swift. Cделали форк языка и на его основе допиливают под нужды. В Colab уже добавили. FastAI, курсы начали переводить. Единственная проблема, крайне сыроват еще, но светлое будущее :).

По-моему вы сами всё прекрасно описали:
Ребята из Google просто искали наиболее подходящий язык и выбрали Swift.
Именно так: не «Google искал», а «ребята из Google искали».

В Colab уже добавили. FastAI, курсы начали переводить. Единственная проблема, крайне сыроват еще, но светлое будущее :).
Где-то я это уже слышал… Chrome Apps, NaCl… Да собственно половина проектов из Google Graveyard когда-то были «сыроватыми, но со светлым будущим».

Слабо себе понимаю причину захоронения S4TF.
То же самое, что и всегда: не оправдал надежд, не набрал критической массы… Посмотрим. Самый важный вопрос не в том, смогут ли они в Colab что-то добавить, а смогут ли они хотя бы один «большой» проект этим увлечь… и то может не помочь: NaCl использовался в App Engine, но ему это не очень помогло…

Вот это самое "кроме" такой немаленький минус. И подозреваю в обозримом будущем оно не войдет в Tier1 поддерживаемых ОС. Rust вполне неплохая альтернатива в данной ситуации.

Есть язык D. Благодаря удобно сделанным шаблонам, утиной типизации, возможности ограничивать типы в шаблонных параметрах (часто используются обобщения для структур данных, например, чтобы условный тип массива и условный тип списка могли приниматься функцией поиска). Ну и плюс обычные Си-подобные типы данных и С++-подобное ООП (но без лютого трэшака). Нормальные массивы, хранящие и указатель на себя, и свой размер. Там много хорошего, выводящего на другой уровень программирование на Си-подобных языках. Как раз тот язык, благодаря которому никак мне не удаётся полюбить динамическую типизацию, хоть я и много времени программирую на Python'е, JavaScript'е и bash'е по долгу службы.
Динамическая типизация переносит ряд возможных ошибок на время исполнения программы вместо времени компиляции.
На самом деле очень прокачивает скиллы кардинальная смена стека. Я всю жизнь (лет 15 я думаю) писал на PHP, пару лет назад понадобилось прочно влезть в яву (более строго-типизированного языка я в жизни не видел), дак я вам скажу что именно после того, как я вернулся обратно на PHP я полностью оценил все преимущества статической типизации, ибо мне не нужно боятся что по какой-то причине я загоню аргументом строку, хотя должен был массив (например, изменил возвращаемое значение какой-то другой функции), представляете что произойдет при этом, особенно когда эта функция должна будет пройти этот массив и сделать несколько запросов в БД или сконвертить его в JSON и отправить его на сервер? Теперь начиная с 7 версии PHP тоже имеет строгую типизацию и заругается если аргумент имеет другой тип данных или функция возвращает другое значение, а не то, которое от нее ожидается.

Как по мне оптимальна гибридная типизация, ибо иногда просто хочется расслабиться и что-то наклепать на коленке, не задумываясь о типах, но в серьезных проектах на том же PHP строгая типизация просто необходима по причинам, которые я описал выше. Причем я понял что словами это не объяснить, с этим нужно сталкиваться чтобы оценить все преимущества.

P. S. Это еще ладно, я еще и после этого с MySQL на PostgreSQL перешел (который тоже строготипизирован), теперь он меня обругивает каждый раз если по какой-то причине в строку суется число (а это может быть следствием какой-то очень серьезной проблемы, ибо почему возвращается число там, где должна возвратиться строка, например, array_search не нашел какое-то значение в массиве, хотя должно, что означает что этот массив сформирован неверно). Очень сильно выручало уже, хотя я не так давно пользуюсь всеми ее преимуществами.
писал на PHP, пару лет назад понадобилось прочно влезть в яву (более строго-типизированного языка я в жизни не видел)
Это не та ли система типов, которая считает null объектом любого типа?
В РНР эту «особенность» умудрились не повторить, кстати.

Наверное, просто потому что null в PHP появился чуть ли не раньше чем сама Java появилась (шутка, она старше на пару месяцев) и изначально был отдельным скалярным типом, когда объектов ещё даже в проекте не было

это круто, конечно, что умудрились не повторить ошибку системы типов, которую проектировали четверть века назад. Дженерики тоже сразу сделали, а не как в джаве?
Ну да, всю систему типов на помойку, и сам язык туда же, у него же тип null есть!

Ну так-то вот эта концепция с null самим её изобретателем признана "ошибкой на миллиард долларов".

заругается если аргумент имеет другой тип данных

Нуда, только его ругание попробуй еще перехвати, приходится статический анализатор гонять

ЗЫ на самом деле Php начинает нервировать, ятоже много лет на нем пишу, и у меня все более отчетливое желание писать на jsp или на чистой Java

TypeError обычное исключение. Обычно его и особо перехватывать не нужно, так же как любое необработанное.

Как правила это — ошибка в коде и ловить такие вещи в рантайме — странная идея.
На рантайме вообще ничего тестить нельзя, учитывая его специфику, все делается на локальном сервере, и просто через Гитхаб обновляются бранчи. Но PHP тем и хорош, что иногда хочется расслабиться и накидать что-то для себя на коленке, не заботясь о типах, как раз таки именно Java в этом плане начинает напрягать, когда ты только и занимаешься тем, что приводишь все к типам. Но в крупных и серьезных проектах это необходимость, да, и очень полезная необходимость.

Хороший пример: когда тон чего-то сказанного в начале убивает желание вообще продолжать смотреть на дальнейшие какие-то рассуждения или аргументы, не важно правильные или неправильные.


Приблизительно как начать общение в таком духе: "слыш, ты, послушай что я тебе сейчас скажу об этом говне...",
что там дальше уже не особо важно.

Пример того, когда автор может честно говорить, что думает. Да, грубовато. Но большинство статей про js намного токсичнее, хотя автор будет обращаться на «вы».
Эта статья скорее развлекательная. Честность и эпатаж в стиле камеди клаб — немножко разные вещи. Честным было бы показать особенности подхода на примере своих работ с примерами кода и анализом выбранных решений.
** Прыгая в комменты с клавиатурой **
-А холивар то где???
P.S. После фразы «адское говнище» не читал.
Наконец то кто то осмелился это сказать! Я уж думал со мной что то не так
Не зря во многие ЯП добавляют статическую типизацию(PHP, Python, Javascript)
В PHP нет ни строгой, ни статической типизации. Нет и не будет.
Тот, кому первому пришла в голову идея назвать рантаймовый контроль типов «типизацией» — будет вечно гореть в аду за обман джуниоров.

Контроль, конечно.


Просто типы — это не рантайм-метки рядом с другими ячейками в памяти, а что-то, что проверяется компилятором статически. Например, Пирс в TAPL это именно так и определяет, и прямо говорит, что dynamic typing is arguably a misnomer.

Не согласен. Типы — информация о том, как интерпретировать то или иное значение. А где она хранится и как и когда проверяется — детали реализации.

Во время выполнения, когда вы уже задеплоили свой код на прод, уже поздно проверять, что вы не складываете число со строкой.


Таки приведу цитату, аж в форме скриншота для важности:

Как по мне, то если контроль типов есть, то это типизация.

То есть, если я в ассемблере буду везде хранить в памяти рядом с объектами их метки и проверять в рантайме, ассемблер станет типизированным?

Если эта проверка встроена в язык и её нельзя обойти — то конечно язык типизированный. По крайней мере, такое понимание типов согласуется и с википедией, и с официальными документациями языков программирования, и с литературой по программированию. То, что это не идеально совпадает с теорией типов в математике — ну так в разных областях одно и то же слово может использоваться в разных значениях.
и с литературой по программированию.

Нет, не согласуется. На несколько комментов вверх прямая цитата.


По крайней мере, такое понимание типов согласуется и с википедией

На википедии и прочих википодобных источниках чего только не написано.

Не знаю, из какой именно книги ваша цитата выше — но даже в ней написано, что такое использование термина является стандартным. То есть, именно так понимается «динамическая типизация» применительно к языкам программирования. Так зачем спорить о терминах?

Из TAPL.


«Является некорректным названием» (или как там misnomer правильно перевести) в первую очередь.

Большинство источников используют "динамическая типизация" без подобных огооврок.

Понятие вроде «динамически типизированный» есть по логике вещей неверное наименование и должно быть вероятно заменено на «динамически проверяемый» (или «проверяемый во время выполнения» — прим. пер.), но использование этого понятия уже устоялось.
Очень странный подход к определению типов данных. Вот есть языки, которые позиционируются, как языки со стогой статической типизацией. При этом практика диктует наличие в таких языках механизмов позднего связывания (по факту элементов строгой динамической типизации). Получается все данные и структуры, для которых использованно позднее связывание не имеют типов вообще? Это как-то выбивает основу из-под строгой типизации, не находите?
Читать про алгебраический тип данных. Много думать.

Строго говоря можно даже говорить о том, что все языки с динамической типизацией — суть языки со статической типизацией, в которых есть ровно один тип (и других создать невозможно). Ну или (как в JavaScript) — их несколько, но их фиксированное число и они все описаны в документации.

Однако в виду полной абсурдности такого подхода обычно от языков со строгой типизацией требуется, чтобы свои типы в них, всё-таки, можно было создавать.

Но нет, позднее связывание не делает язык нетипизированным. Даже если в каким-то месте про тип и нельзя ничего сказать (как в Java, когда вы получаете Object), но в других-то можно!

Есть, кстати, более интересный способ размыть границу.


Есть такая штука в теории типов, как сигма-тип — это пара из значения одного типа и значения другого типа, где второй тип зависит от первого значения. Например, (n : Nat ** Vect n Int) — натуральное число и вектор соответствующей длины.


Так вот, никто не мешает вам написать тип (a : Type ** a) — это сигма-пара из типа (а типы — first-class citizen, как мы помним) и значения этого типа. То есть, у вас по факту есть метка типа и объект этого типа — всё как в питонах, JS и так далее. И вы даже можете написать [(_ ** "yay string"), (_ ** 42), (_ ** MkSomethingElse)] — почти динамически типизированный список, можно даже типы не писать, а оставить подчёркивания, чтобы компилятор их вывел!


Однако, есть проблема: подавляющее большинство имеющихся языков вроде агды, кока или первого идриса очень не любят паттерн-матчинг по типам из-за parametricity, поэтому создать объект такого типа вы сможете, а вот использовать его — нет.


К счастью, есть и решение: в Idris 2 завезли новую теорию, интегрирующию завтипы и некоторую форму линейных типов, и теперь вы вполне сможете написать что-то вроде


type Dyna = (a : 1 Type ** a)

stupidAdd : Dyna -> Dyna -> Maybe Dyna
stupidAdd (String ** s1) (_ ** s2) = Just (s1 <> s2)
stupidAdd (Nat ** n1) (_ ** n2) = Just (n1 + n2)
stupidAdd _ _ = Nothing

То есть, тайпчекер всё равно проверяет, что код имеет смысл, статически (и написать stupidAdd (String ** s1) (Nat ** n2) = s1 + n2 у вас не получится), но теперь вы можете делать что-то, что очень сильно пахнет тем же питоном.

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


Тогда нет, не выбивает основу, если рантайм даёт соответствующие гарантии. Условно, если dlsym не возвращает указатель на что угодно, а возвращает указатель на функцию, проверяя, что эта функция при компиляции имела тот тип, который от неё ожидается в данном конкретном месте.

К сожалению dlsym даёт просто указатель на функцию, которую можно вызывать. А уж как её вызывать — не его дело.
Были архитектуры, где именно так и сделано — железо само следит за типами аргументов. Можно ли считать такой ассемблер типизированным?

В том смысле, о котором я говорю — нет. Он же не проверяет типы при ассемблировании?

Вы определили «типы» как нечто, проверяемое при компиляции. Но это ведь не единственное определение.

Определять, понятное дело, можно как угодно, главное об этом договориться. Но у типов давно (ещё до программирования) есть вполне конкретное определение, которое на программирование отображается как статические проверки. Зачем эти вещи путать?


Никому же не приходит в голову назвать типизацией наличие проверок на корректный доступ к элементу массива в рантайме, который нельзя обойти.

Применительно к программированию я, например, встречал определение типа как набора значений и операций над ними. Когда именно проверять, что объекты удовлетворяют такому типу, там не уточнялось.

назвать типизацией наличие проверок на корректный доступ к элементу массива


Тем не менее в Паскале длина массива именно что входила в определение типа.

(ещё до программирования)


Если вы имеете в виду математические типы в стиле введенных Расселом, то он ведь тоже не уточнял, в какое время их надо проверять.

Поэтому ваше утверждение

которое на программирование отображается как статические проверки


достаточно спорно.

Если уж на то пошло, то и статическая, и динамическая проверка типов вообще не относятся к типам, как таковым — типы просто существуют, а является скорее помощью человеку, который не может не делать ошибок и не путать данные разные типов в процессе программирования или выведения логических формул.
Применительно к программированию я, например, встречал определение типа как набора значений и операций над ними. Когда именно проверять, что объекты удовлетворяют такому типу, там не уточнялось.

Дико неконструктивное определение.


Должна ли операция «удалить первые N символов» быть в определении строки? Если у вас питон с типа строгой динамической типизацией, то, получается, "abcde" и "" — разные типы?


Тем не менее в Паскале длина массива именно что входила в определение типа.

А там можно получить число по сети или считать из файла и выделить массив ровно такой длины, да чтобы его длина осталась в типе?


Если вы имеете в виду математические типы в стиле введенных Расселом, то он ведь тоже не уточнял, в какое время их надо проверять.

Тамошняя ramified theory of types как раз позволяет сказать, что некоторые выражения не имеют смысла, не «вычисляя» (то есть, не анализируя семантику) эти выражения.

> Дико неконструктивное определение.

Не только конструктивное, но даже конструктивистское. Т.е. вполне пригодное для практического построения системы типов и ее использования.

Типы в ЯП до формализации примерно так и строились.

Нет. Оно ведь не определяет даже рассматриваемый набор операций, а их синтаксически счётно бесконечное число, что делает задачу неразрешимой.

На практике просто выбирают удобные и легко реализуемые. Для целых чисел, например, знакомые арифметические действия с поправкой на двоичность и ограниченность.

Я окончательно запутался в предложенном определении. То есть, тип — это не про совокупность операций, а про такие несомненно объективные критерии, как удобство и реализуемость.


Научно и инженерно, ничего не скажешь.

Вы путаете инженерию с математикой. Инженерия — это как раз о том, что удобно и реализуемо, а не то, что аксиоматично и строго формализуемо. Математика всего лишь шьет пиджаки для осьминогов.
Должна ли операция «удалить первые N символов» быть в определении строки?


Может быть, но не обязательно. Она не слишком аксиоматическая, что ли.

Если у вас питон с типа строгой динамической типизацией, то, получается, «abcde» и "" — разные типы?


Непонятно, почему вы пришли к такому выводу. Операция эта будет определена как функция отображения строки в строку, т.е. тип объекта не изменится.
Может быть, но не обязательно. Она не слишком аксиоматическая, что ли.

Ну окей, «удалить один первый символ».


Операция эта будет определена как функция отображения строки в строку, т.е. тип объекта не изменится.

Но операция «удалить первые 5 символов» неприменима к пустой строке.

Значит, это частично определенная функция. Ничего особенного.

Так почему операцию деления не сделать определённой вообще на всех объектах? Просто на некоторых (на числах, например) она тоже будет частично определённой.

Иногда так и делают. Например, добавляют к множеству «действительных чисел» NaN и доопределяют деление.
Может быть, но не обязательно. Она не слишком аксиоматическая, что ли.

То есть вместо строгого определения имеем: "Вроде как нет, но если надо, почему бы и не да".

Отнюдь. Просто задачу выделения элементарных операций над типом (и определить тем самым тип) можно решить разными способами. Как только мы зафиксировали один из них, дальше все строго.

И если у вас из разных элементарных операций получается разное множество реализуемых операций, то что-то в вашей теории сильно не так.

Боюсь, что это не столько теория, сколько практика. И не моя, а универсальная.

Та же практика показывает, что чем более математизированы основания под языком, тем проще и адекватнее с ним работать.

ХЗ. После некоторой границы популярность языка меня не особо волнует, так как все эти миллионы программистов на нём вряд ли будут писать код вместо меня.

Несомненно. Порядок и логика всегда лучше хаоса и конструкций из палок. Но практика еще и показывает, что математизации поддаются только самые простые части мира, и программирования в частности.

У меня лично ощущение, что "полная" математизация основ языка (теория типов, теория категорий) негативно сказываются на его популярности.

Я думаю, что у нас пока недостаточно статистики, чтобы отделить это от прочих факторов.

некоторые выражения не имеют смысла, не «вычисляя»


Вы все равно вычисляете — ведь это знание не дано свыше, а требует тех же символьных манипуляций. Просто в данном случае есть более короткий способ вычисления — как некоторые интегралы можно посчитать в символьной форме, а не численно. Но в общем случае вычисления все равно придется проводить полностью.

Но я не вычисляю ответ. Когда я проверяю, что A : Set, мне совершенно неважно, какие элементы будут в A, пока оно удовлетворяет некоторым синтаксическим (и разрешимым!) правилам.

В частных случаях. Это просто shortcut — как и вся математика, собственно.

Нет, это не шорткат. Это ответ на другой вопрос.


Мне не нужно знать, что такое на самом деле A или P, чтобы понять, что { x ∊ A | P(x) } — корректное выражение. Достаточно A : Set и P : A → Bool. Мне не нужно ничего знать вообще ни о чём, кроме типа sin, чтобы понять, что { x ∊ sin x } некорректно. И вычислять его не надо.

выделить массив ровно такой длины


Насколько я помню исходный виртовский Паскаль — нет. Массивы там были вообще не динамические, а в их тип входили тип элементов, тип индексов и диапазон индексов.

А для передачи массива в процедуру приходилось определять формальный аргумент, прибегая к чему-то вроде any: ARRAY OF INTEGER, например, вместо полного типа ARRAY[1..10] OF INTEGER.
Конечно ассемблер типизированная вещь. Типов, правда, не так много: «нечто размера 32 биты», «нечто размера 128 бит»… ну и всё.

Хотя бывают разные ассемблеры. Почитайте документацию на TASM. У них там объекты были.
Не нечто, а вполне определённые форматы, для которых нужны свои инструкции.
Целочисленный add, применённый к float значению, выдаст хурму на выходе.
елочисленный add, применённый к float значению, выдаст хурму на выходе.
Недоумённо смотрит на свой код из релизнутого продукта. А вы точно в этом уверены?

А вот эту статью вы когда-нибудь видели?
На ассемблере add вполне себе выполнится, вот только результат будет весьма прикольный.
Почему прикольный? Всё будет зависеть о того, что вы складываете с чем и зачем.

В моём случае речь шла об округлении мантиссы — это делается как раз использованием целочисленных операций с float.
В этом случае да, но не следует забывать того, что какраз у самого процессора(x86, сопроцессор и прочее не учитываем!) понятия типов вообще нет, и ему глубоко пофигу что с чем складывать. Поэтому 1.1f + 43 вполне себе может вылиться в любой треш.
Тут код специально рассчитан на такое поведение и работает со специально подобранными константами.
Разумеется, какие-то целочисленные операции можно применять к float зная формат и ожидаемый результат.

Я же говорил, что сложив 1+1 вы получите не 2, а 1.7014118346e+38

Точно так же, перепутав знаковое и беззнаковое деление результат может быть неверным.
Я же говорил что сложив 1+1 вы получите не 2
А почему вы, собственно, должны получить 2? Вы и без всяких floatов можете получить чушь, если в одной переменной у вас 1 и в другой 1, только в одной — это метр, а в другой дюйм.

Проверено экспериментально.
Хоспаде. Я написал банальную мысль о том, что при программировании на ассемблере нужно следить за типами инструкций и операндов. Типы отличаются не только размером, но и форматом данных.
Процессор не сделает преобразование типов за вас. К чему вот было это ваше «а можно плавать и со штангой»?

>> А почему вы, собственно, должны получить 2?
Потому что я хочу получить 2, наверное?
Потому что я хочу получить 2, наверное?

Интересный аргумент. А если я хочу получить 3, то должно получаться 3?
Нет, конечно. Лицензия на «хотение», очевидно принадлежит beeruser — и потому только он имеет право чего-то хотеть. Вы опоздали.
А если я хочу получить 3, то должно получаться 3?
1+1=3? Cтранное желание, но как хотите.
Хотя бывают разные ассемблеры. Почитайте документацию на TASM. У них там объекты были.

Лучше на TAL-0 тогда уж.

Проверка выхода за границу массива это не проверка типа? Или защита от выполнения данных?
Ещё, слышал, бывали процессоры, у которых переменные содержали поле с типом.
Проверка выхода за границу массива это не проверка типа?

В рантайме? Нет.


Или защита от выполнения данных?

Нет. У типа есть очень формально определённое значение, и даже если кто-то использует этот термин неправильно, это не значит, что этому надо способствовать (примерно как с «ться»/«тся»).

У типа есть очень формально определённое значение

Много определений типа в программировании. Некоторые ещё тянут в программировании определения типов из математики.

"У типа есть очень формально определённое значение".


Я знаю про несколько определений типа из нескольких разных теорий типов. Не считая определений из прикладных языков программирования, который возникли раньше тапла и из других предпосылок. Какое же из них верное?

Не считая определений из прикладных языков программирования, который возникли раньше тапла и из других предпосылок.

Понятие типа в контексте STLC возникло до любого из прикладных языков программирования. Да и уже automath какой-нибудь возник сильно до любого из ныне существующих языков программирования.


Какое же из них верное?

Откуда мне знать? Вы ж их не назвали.

Понятие типа в контексте STLC


1. Система типов из «лямбда-исчисления с типами» не единственная система типов, а только одна из.
2. Системы типов в современных мейнстримных языках (как со статической типизацией, так и с динамической) — это очень далеко не STLC и я подозреваю, что их авторы строили их на несколько других основаниях (и не только формальных).
3. Да, можно натянуть сову на глобус (что и делает тапл) и вывести одно из другого, но это вообще не означает, что определение типа из STCL единственно верное или валидное для языков программирования.
4. То что система типов красиво формализуема еще не означает, что она хорошо подходит для промышленной разработки людьми, которым важно получить результат здесь и сейчас, а не формально верифицировать корректность программы.
Система типов из «лямбда-исчисления с типами» не единственная система типов, а только одна из.

Естественно. А в каких других теориях типов это не статическая классификация?


Уточню на всякий, что стоит рассматривать теории с разрешимым тайпчекингом, хотя и там есть разница между вычислениями для тайпчекинга и между вычислениями для получения финального значения.


По остальным пунктам — а о чём мы спорим-то? Вы хотите сказать, что «динамическая типизация» — настолько же корректный термин, как «динамические проверки»?

А в каких других теориях типов это не статическая классификация?


Ну есть, например, такая «Gradual Type Theory». Правда я с ней недостаточно знаком, чтобы внятно ее обсуждать.

По остальным пунктам — а о чём мы спорим-то?


Я спорю с утверждением, что «типы — это не рантайм-метки рядом с другими ячейками в памяти, а что-то, что проверяется компилятором статически», и утверждаю, что если «статическая типизация = типы проверяются компилятором статически», то так же правомерно говорить «типы проверяются рантаймом динамически = динамическая типизация».

Но проверяются не типы, потому что в рантайме у вас не тип.


В хорошей системе типов для того, чтобы получить тип терма, вам не нужно решать Тьюринг-полную задачу. А если вы переносите проверки на рантайм — то нужно.

А если система типов есть, но она плохая по этому критерию?

Я не знаю языков с Тьюринг-полной системой типов, при разработке которых при этом всерьёз думали бы о системе типов, и где эта полнота была бы желаемой (а не как в темплейтах C++, где Тьюринг-полнота была открыта, или в дженериках Java, где надо сильно изворачиваться, и на практике это не парит).


Да, если вы возьмёте ту же теорию типов Мартина-Лёфа и добавите туда экстенсиональное равенство, то у вас получится неразрешимая система типов, но на практике именно поэтому так никто не делает.

automath какой-нибудь возник сильно до любого из ныне существующих языков программирования.


Я думал, что тут разговор о языках программирования, а не доказателях теорем.
Разве пыха компилируется в принципе? Я сто лет не пышник и не в курсе новостей этого вашего пшп 7, хотя про типы и слышал. Просто обывательский подход — если ты не сидишь и не ждешь конца компиляции — оно не компилируется, а выполняется.

В 8 обещают JIT компиляцию в нативный код, а пока только в опкоды

А как называются рантайм метки более коротко? И какое название у описания того, что можно делать с некоторой штукой вне зависимости от того, рантайм это или дизайн тайм?


Мне кажется, такой подход к терминологии менее ортогонален.

А как называются рантайм метки более коротко?

Ну так и называются, метки.


Впрочем, чем реже вам о них надо вспоминать, тем лучше.


И какое название у описания того, что можно делать с некоторой штукой вне зависимости от того, рантайм это или дизайн тайм?

Ээ, не знаю, это какой-то слишком общий термин для меня.

Ну так и называются, метки.

А кем они так называются? Есть ли какая-то реализация которая называет их не типом?


Например, в вашей любимой IDE при отладке тип переменной и тип значения переменной называются по разному? Один тип, другой метка?


Ээ, не знаю, это какой-то слишком общий термин для меня.

Ну вы в обычной речи слово тип не употребляете?


С моей точки зрения в книжке терминология интересна но неудобна, все говорят "тип" для общего, никто не использует выражения "рантайм метка" а статика тесно связана с динамикой.

Например, в вашей любимой IDE при отладке тип переменной и тип значения переменной называются по разному? Один тип, другой метка?

В моей IDE для хаскеля вообще нет рантайм-меток (да, я за всю практику пользовался Typeable в своём коде ровно один раз). Да и дебаггером я там не пользуюсь.


В моей IDE для плюсов их тоже не особо много для рантайм-поведения. Максимум — по vtbl можно определить, какой класс-наследник доступен по указателю на базовый класс, но какими бы то не было проверками типов там и не пахнет.


Ну вы в обычной речи слово тип не употребляете?

Зависит от контекста. Ещё употребляю «класс», «множество» и прочие подобные слова.


С моей точки зрения в книжке терминология интересна но неудобна, все говорят "тип" для общего, никто не использует выражения "рантайм метка"

А зря. На мой взгляд, создаёт неправильные ожидания.


а статика тесно связана с динамикой.

Не обязательно. В том же хаскеле в общем случае после того, как вы проверили типы, вы можете их стереть и не иметь вообще ни намёка на них в рантайме.

С моей точки зрения в книжке терминология интересна но неудобна, все говорят «тип» для общего, никто не использует выражения «рантайм метка»

А зря. На мой взгляд, создаёт неправильные ожидания.

Зря или не зря — это уже больше философский вопрос. Факт в том, что «динамическая типизация» по отношению к языкам программирования используется именно в таком смысле, и причины, по которым так сложилось, здесь не важны.

Факт, однако, и в том, что куча людей пользуеться «ться»/«тся» некорректно, и даже несмотря на то, что язык — живой и подвижный предмет, который формируеться тем, чем предпочитают пользоватся люди, это почему-то не мешает старатся блюсти чистоту использования этих частей слов.


И если мы обсуждаем преимущества разных видов типизации, то, ИМХО, лишний раз указать на принципиальное различие между типизацией и рантайм-проверками, которое по-хорошему должно быть определено даже в терминологии, вполне себе стоит.

В языке «ться» и «тся» не различаются, они различаются лишь на письме, которое представляет собой условность. Потому, собственно, их и путают на письме.

лишний раз указать на принципиальное различие между типизацией и рантайм-проверками


То, что вы называете типизацией, — всего лишь проверки до рантайма.
То, что вы называете типизацией, — всего лишь проверки до рантайма.

Где им, когда есть такая возможность, самое место.

Так можно на что угодно ответить. Ну вот, например, важность популярности языка — это лишь ваше убеждение :)

От задач зависит. Популярность языка, стэка обеспечивает масштабируемость разработки для бизнеса и наличие рабочих мест для программистов.

И объективность важности этого ровно такая же, как объективность важности как можно более раннего отлова ошибок.

Титанический труд проделал 0xd34df00d по вводу правильной терминологии, но увы так и не убедил любителей упасть во время выполнения(на миллионе юзерских девайсов) что лучше упасть во время компиляции(на единственном девайсе разработчика).
Вам экологии то не жалко ребята?
Триллионы триллионов раз, миллиарды юзеров будут гонять какие то там рантайм псевдропроверки, тратить ресурсы железа впустую, только потому что в вашем «типизированном»(в кавычках) языке нельзя их проверить во время компиляции.
НЛО прилетело и опубликовало эту надпись здесь

Извините, но вы соответствие Карри-Говарда проигнорировали. Избирательное зрение?

НЛО прилетело и опубликовало эту надпись здесь
НЛО прилетело и опубликовало эту надпись здесь

Так в том споре мы же выяснили, что проблемы с пониманием сути были у вас, даже после того, как вам на них указали несколько раз?

Что вы собрались выяснять и в каком споре? Если человек не умеет в логику? В принципе?

Я собрался выяснять методы взаимодействия с людьми, которые не умеют в логику. Это, к сожалению, полезный на практике навык.

А… ну это, успехов. Я умею сделать так, чтобы их уволили (что, обычно не так и сложно), а большего мне и не нужно обычно.

Ну, я в свою очередь в политику и подобное не умею, так что выживаем как можем.

В политику и я не умею. Но с людьми, не умеющиеми в логику, обычно бесполезно спорить. Нужно просто пользоваться тем, что они не умеют просчитывать результаты своих шагов и «делать их крайними».

Они, впрочем, обычно обладают крайне развитым навыком «переноса ворот» (как вы это уже тут видите), потому важно им всячески помогать, но ни в коем случае не брать на себя никаких обязательсв, если они не скрплены «подписями и печатями».

Даже если вам за выполнение чего-то сказанного мимоходом и нигде не зафиксированного обещают кучу плюшек и всяких благ. Лучше прослыть «ничего не понимающим в бизнесе», чем оказаться крайним, когда очередной такой персонаж будет на вас пытаться повесить свои косяки.
Типы же первичны? Ошибся в типе, описал функцию как минус. Когда писал реализацию функции, IDE мне сказала, чувак тут надо "-" судя по типу, ну я и исправил на "-", хотя по тз там плюс.

но ведь ты тоже проигнорировал, как соответствие карри говарда поможет от неправильно поставленной/понятой/решенной задачи?
Почему ты допускаешь что в функции ошибиться можно, Но в тоже время уверен что в типах ошибиться нельзя, перенеся потом эту ошибку в реализацию?

От неправильно поставленной или понятой задачи не поможет вообще ничего. Вообще. Если у вас попросили автопилот для машины, а вы сделали автопилот для самолёта (лучший среди всех автопилотов), то это не поймают ни тесты, ни типы, ничего.


Но это не логическая ошибка.

или понятой задачи не поможет вообще ничего. Вообще

Я так и сказал.
Едиственно в чем мы расходимся это
Но это не логическая ошибка.

Особенно если не доводить до абсурда, типа
вас попросили автопилот для машины, а вы сделали автопилот для самолёта


Что ж тогда логическая ошибка, функция хочет число, а мы даем ей строку?
Проверить входит ли в диапазон доступных значений номер кредитной карты, типы допустим могут. Но кому от этого проще, если программист неверно вбил этот диапазон в определение типа, а не в рантайм проверку в функции?
Что ж тогда логическая ошибка, функция хочет число, а мы даем ей строку?

Это когда вы спеку поняли правильно, но то, что вы написали, расходится со спекой.


И получается, что спека у вас кодифицирована в типах, и компилятор просто проверяет, что реализации на самом деле ей удовлетворяет.


А если мне сказали закодить биржевого бота, который будет торговать на какой-нибудь азиатской бирже только в рабочие дни, то, например, если я неправильно скопирую список праздников (или нагуглю список не для той страны), то типы едва ли это помогут отловить, конечно. Но как это отлавливать — вообще непонятно.

А если мне сказали закодить биржевого бота, который будет торговать на какой-нибудь азиатской бирже только в рабочие дни, то, например, если я неправильно скопирую список праздников (или нагуглю список не для той страны), то типы едва ли это помогут отловить, конечно. Но как это отлавливать — вообще непонятно.

Хуже. Список рабочих дней может как в России определяться в предыдущем году по решению Правительства. Или как с "нерабочими" днями. По ходу дела.
Вообще удивительно, что только 0xd34df00d реально вернулся к истокам. Все это программирование — это не код ради кода, а код обработки данных. А все данные типизируются. А код — это просто функции превращения одного в другое.

у него большая проблема: многое из того что он говорит базируется не на научном подходе, а на религиозных предпочтениях/взглядах
Ну хоть с тем, что ЯП со статической типизацией убирают множество проблем с ошибками типов вы согласны?
НЛО прилетело и опубликовало эту надпись здесь
однако надо помнить (и это исследовал ещё Ларри Уолл), что большинство проблем с ошибками типов связаны с тем, что в языках некорректно сдизайнены операторы сравнения и математические операции.
А ещё нужно помнить, что когда эта «глыба», эта «гора», этот «гений» решил создаить что-то на основе своих идей… то получился высер такого микроскопического размера, что о нём даже как о мыши-то говорить смешно.

и чем крута динамическая типизация: что программист больше думает об алгоритме, нежели занимается обрядами вокруг его реализации
Серьёзно? И потому как только вам требуются реально серьёзные алгоритмы (распределённые базы данных или хотя бы SQL-базы, компиляторы, операционные системы и всё такое прочее) — так прям все на динимических языках начинают программировать? Вы это сейчас серьёзно?

Знаете — весь этот ваш пафос был бы слегка более уместен если бы подверждался опытом. И вы могли назвать хотя бы одну систему, где динамически типизированный язык — это не «пенка» на базисе из модулей на статически типизированных языках, а что-то, что сущесвует само по себе. Хотя бы.

Уж не говоря о том, что если бы динамически типизированные языки были бы так круты, как вы описываете, то именно они должны были бы формировать базис, а на статически типизированных языках люди бы писали что-то, ошибки в чём были бы не так опасны.

и это путь решения тех же проблем но на дороге динамической типизации
Это махание руками. Давайте ближе к практике:
1. Реализация динамически типизиванного языка на динамически типизованном языке же: ___
2. Операционная система на этом самом динамически типизованном языке: ___
3. База данных на таком же языке: ___
4. Процент рынка, который вот всё это заняло в ___ году: ___

Вот как заполните пропуски — так сможете лить в уши сказки про преимущество динамической типизации в деле реализации алгоритмов. А до тех пор — это всё рассказы условного «таджика» умеющего неплохо строть туалеты и двухтажные домишки дендрофекальным метордом о том, что у оного метода есть масса преимуществ перед сталью и бетоном, а что какие-то идиоты из говна и палок даже не пытаются строить мосты и небоскрёбы — так это потому что у архитекторов и инжинеров-строителей умишко слабенький и нет того опыта строительства туалетов, что «таджика»…
НЛО прилетело и опубликовало эту надпись здесь
назовите три полезных программы на Расте/Хацкеле стоящие на большинстве компьютеров
Назовите хоть одну такую на Raku для начала. Или вам можно выбирать языки, а мне нельзя? Вы же сами тут поёте песни про крутизну Ларри — ну вот покажите… на практике.

динамически типизированные языки — это скриптовые языки, прежде всего.
Внезапно как, а. А почему так, не расскажите? Почему языки, в которых «программист больше думает об алгоритме, нежели занимается обрядами вокруг его реализации» не применяются там, где алгоритмы сложны и о них действительно приходится думать — но всё больше там, где алгоритмы тривиальны и думать о них не нужно?

затем попробуйте удалить Perl и Bash. и посмотрите на результат
И много вы алгоримов на Bash написали? Я как-то писал топологическую сортировку банальную — то ещё равлечение было. В Android, кстатати, нет ни Perl, ни Bash. И ничего — работает как-то.

А вот попробуйте оттуда удалить модули, написанные на C…
НЛО прилетело и опубликовало эту надпись здесь
Вы хотите сказать что языки со строгой/статической типизацией все находятся в стадии «бета» (== «ещё не доделан»)?
Я хочу сказать, что с идиотами, записывающими в языки с динамической типизацией C и Java разговаривать бессмысленно. Хотя вас я идиотом не считал, но… теперь вижу._
НЛО прилетело и опубликовало эту надпись здесь

Ну и в итоге в написанном на С системном ПО регулярно находятся дыры из серии висячих указателей, выхода за границы, какой-то наркомании с uid'ами, и так далее.

Эти все доводы работают в каком-то выдуманном виде. Где «венец творения» это не "рюмка коньяка с ломтиком лимона документооборот", а какие-то дурацкие вещи типа смартфонов и космических кораблей.
Типизация слабая, да. Но даже при всём при этом в OpenSSL уязвимостей куда меньше, чем в каком-нибудь Drupal. А уж если выкинуть всякие «module that can only be compiled by the HP-UX assembler, so that only HP-UX PA-RISC targets are affected»…

Да, предствьте себе — даже такая слабая типизация, как в C, и даже при такой ужасной культуре кода, как в openSSL (поговорите с теми, кто внутрь смотрел) всё равно снижает количество уязвимостей. В каком-нибудь NGINX — их меньше на порядок. В Chrome — да, побольше будет… но вы когда-нибудь сраванивали по объёму Drupal и Chrome? Сравните как-нибудь на досуге.
поэтому языки вроде C, C++, Java (и прочие языки традиционно ориентированные) — это языки, которые я противопоставляю высказываниям сектантов.
У… как всё запущено. Что такое вообще «традиционно ориентированный язык»?

именно строгую типизацию сектанты вроде 0xd34df00d противопоставляют тестам.
Серьёзно? У вас всё с логикой настолько плохо?

Извините, но я нигде и никогда не слышал, чтобы 0xd34df00d говорил о том, что типами нужно заменять тесты. Он всегда говорит о том, что можно — и да в Idris это попроще, а в C++… ну на спор, наверное, тоже можно, но в реальной программе — не получится.

Вопрос того, что нужно выражать ограничениями на типах, а что лучше оставить в виде тестов — он совершенно отдельный от вопросов принципиальной реализуемости того или иного подхода.
НЛО прилетело и опубликовало эту надпись здесь
А какое вообще вопрос «кто кого любит и как» оказался связан с языками програмирования?

И, кстати, как вы вообще выясняете ориентацию программистов на Haskell или C++?
НЛО прилетело и опубликовало эту надпись здесь
назовите три полезных программы на Расте/Хацкеле стоящие на большинстве компьютеров

После трёх полезных программ на питоне/шелле/перле, стоящих на большинстве компьютеров.

НЛО прилетело и опубликовало эту надпись здесь
Давайте теперь Вы назовите пару монополистов, имеющих аудиторию в миллиард людей, чтобы их основной язык был со строгой/статической типизацией
Вы издеваетесь или как? Ну пусть будет Google и Microsoft, если уж так хотите. Только не рассказывайте сказок про то, что Microsoft меньшая монополия, чем какой-нибудь Facebook: в китае без Facebook отлично живут, а без Window — таки не обходятся. Ну или Apple возьмите — да, это не монополия… но денег она зарабатывают больше, чем Facebook и Mail.Ru вместе взятые.

то FaceBook — это PHP.
Нет. PHP такую махину не потянет. Facebook — это Hack. И да — он статически типизирован.
то FaceBook — это PHP

Лол. Это не PHP. Это HVVM и Hack. И в Hack есть опциональная поддержка статической типизации (gradual typing). Общался с чуваками, пилящими Hack — они бы рады сделать полную static typing, но легаси, увы, мешает.


А ещё Facebook — это, кстати, хаскель. Широко известный в узких кругах Саймон Марлоу работает в FB и пилит там на хаскеле антиспам и ещё пару систем, например. Где ваш динамически типизированный бог теперь?


В Касперском что-то пилили на хаскеле. По крайней мере, когда тамошние рекрутёры общались со мной N лет назад.


Давайте теперь Вы назовите пару монополистов, имеющих аудиторию в миллиард людей, чтобы их основной язык был со строгой/статической типизацией

Микрософт? Гугл? Яббл?


В Боинге юзают Coq (уж статичнее некуда) для верификации некоторых систем.

В Касперском что-то пилили на хаскеле. По крайней мере, когда тамошние рекрутёры общались со мной N лет назад.

поговаривают, что там лоно адептов крестов и Раста

Да-да. Нанимают сишников-системщиков и заставляют их монадки моноидировать.

> Booking.com — это Perl (сейчас мигрируют на Python, просто Python'щики готовы работать за еду, поэтому)

На Java. Какой смысл уходить на Python для такой нагруженной задачи?
(распределённые базы данных или хотя бы SQL-базы, компиляторы, операционные системы и всё такое прочее) — так прям все на динимических языках начинают программировать?


Однако же поверх всех этих замечательных программ тут же возникают динамические языки — шеллы или тот же SQL. SQL сильно типизирован?

Совпадение? Не думаю.

Так никто вроде бы и не спорит, что в качестве glue code для одноразовых задач динамические языки вполне себе работают.

Некоторые SQL запросы переживают несколько смен языка арр-сервера

Совпадение? Не думаю.
Нет, конечно. Как только вы решаете, что вам не нужен качественный код, но нужны дешёвые программисты — так динамические языки становятся, вдруг, резко осмысленными.

Программисты на PHP получают меньше, чем программисты на C++, а администраторы («программисты на bash») — ещё меньше.

В некоторых случаях возможна и обратная ситуация (финансовый аналитик, пишущий только программы на каком-то простеньком язычке, но никак не на C++ — может получать и больше программиста на C++), но в этом случае они получают столько не за то, что умеют лихо писать программы на Python, а за что-то совсем другое.

Где-то тут уже приводил: в Киеве разница между PHP и Javaсеньорами порядка 5% всего. Это во столько бизнес оценивает надежность статической типизации (забудем про то, что часто Java и быстрее)?

Опять бред несете. Вы живое доказательство того что динамика а особенно PHP разжижает мозг.

Поищите — это публичная статистика, я ссылки приводил в топике

Ох уже эти предрассудки. Во многих организациях платят одинаково что фронтам что беками независимо от языка программирования. Дело вообще не в том кому больше платят. Сколько платят больше от организации конкретной зависит. Дело вообще в другом.
Вооб вон PsyHaSTe говорил что он фронтов нанимал дороже чем беков. Я бы все равно из-за этого не перешел бы во фронты.

к чему тогда пассажи про "нужны дешёвые программисты — так динамические языки становятся, вдруг, резко осмысленными. Программисты на PHP получают меньше, чем программисты на C++"


У меня есть цифры, что эти "дешевые" лишь на 5% дешевле, а разница в качестве, вроде как, качественная, если верить адептам статики.

У меня есть цифры, что эти «дешевые» лишь на 5% дешевле
Нет у вас таких цифр, извините. У вас есть информация про кое-что другое.

Разница между дешёвыми и дорогими программистами лишь слегка кореллирует с зарплатой.

Более того — в некоторых случаях программист, получающий более высокую зарплату может оказаться дешевле.

Подумайте над этим.

а разница в качестве, вроде как, качественная, если верить адептам статики.
Разница качественная — но не между динамикой и статикой.

А между продукцией «дешёвых» и «дорогих» программистов.

Я это уже показывал на примере CVE.

И да, разница между зарплатами — гораздо меньше, тут вы, что забавно, тоже правы.
однако надо помнить (и это исследовал ещё Ларри Уолл), что большинство проблем с ошибками типов связаны с тем, что в языках некорректно сдизайнены операторы сравнения и математические операции.

Я, к сожалению, не Ларри Уолл, и решаю не Ларри Уолловские задачи. Большинство проблем с ошибками типов оказывается связано не с операторами сравнения и не с математическими операциями.


Может, потому, что языки, которые я использую, уже от этого защищают. Даже C++ защищает (да, там тоже можно прибавить int к char*, но голый char* скорее не встречается, чем встречается).


и чем крута динамическая типизация: что программист больше думает об алгоритме, нежели занимается обрядами вокруг его реализации

А вот в этом основная проблема в вашей логике: вы это воспринимаете как обряды, а это не обряды (хотя после некоторых языков иначе это воспринимать действительно трудно, спору нет). Типы помогают, типы ограничивают, типы направляют.

Не в возражение основному, но:

> В языке «ться» и «тся» не различаются, они различаются лишь на письме, которое представляет собой условность. Потому, собственно, их и путают на письме.

В языке у них разная роль, что можно увидеть, например, по тому, что для некоторых глаголов вместо "-ться" получается "-тись": нестись, пастись…
(это как раз о типизации;))

В фонетике, да, они сливаются — но уже после этого.
Они не различаются на слух, следовательно, со временем это будет один и тот же грамматический элемент, исторически произошедший из двух разных.
1. Это не грамматический элемент.
2. С чего это бы им становиться одним элементом? У большинства глаголов таки тут нет совпадения, случаи типа «храниться»:«хранится» — малая часть.
И если мы обсуждаем преимущества разных видов типизации, то, ИМХО, лишний раз указать на принципиальное различие между типизацией и рантайм-проверками, которое по-хорошему должно быть определено даже в терминологии, вполне себе стоит.

Так никто не против указывать на различия статической и динамической типизации. Более того, никто вроде не отрицает, что с некоторой точки зрения правильнее эти две альтернативы называть по-другому. Но для того, чтобы как можно больше людей, связанных с программированием, вас сразу без дополнительных пояснений правильно понимало, нужно использовать именно «статическая типизация» и «динамической типизация» — это устоявиеся названия классов языков. Можно для себя их называть как угодно, но все (?) официальные документы по динамически типизированным языкам программирования используют слова «тип» и «динамическая типизация»/«динамическая проверка типов» — например python, js. То же верно и для обсуждений этих языков на практике. Поэтому смена терминологии привнесёт только путаницу на этом этапе.
Но для того, чтобы как можно больше людей, связанных с программированием, вас сразу без дополнительных пояснений правильно понимало, нужно использовать именно «статическая типизация» и «динамической типизация» — это устоявиеся названия классов языков.

Это один вариант, безусловно.


Но есть и другой вариант — это когда в интернете кто-то неправ можно попытаться повлиять на устоявшуюся терминологию и немножко её причесать. Почему бы и не попробовать, в конце концов?

В моей IDE для хаскеля вообще нет рантайм-меток (да, я за всю практику пользовался Typeable в своём коде ровно один раз). Да и дебаггером я там не пользуюсь.

Если вы им не пользуетесь это не значит что его нет. Я посмотрел — оно умеет как-то определять тип в рантайме.


Кстати, определите до конца термин "рантайм метка" он не отражает метка чего именно.


В моей IDE для плюсов их тоже не особо много для рантайм-поведения.

А что у вас за IDE для плюсов? У вас там нет cимволов и RTTI? в окне watch нет колонки type для переменных? Или там написано что-то типа "рантайм метка относящаяся к набору операций которое можно совершать со значением"?


А зря. На мой взгляд, создаёт неправильные ожидания.

Какие и у кого?


Не обязательно. В том же хаскеле в общем случае после того, как вы проверили типы, вы можете их стереть и не иметь вообще ни намёка на них в рантайме.

Я хаскель знаю очень поверхностно. Мне трудно с этим поспорить.


С моей точки зрения, терминология, которую вы предлагаете требует введения разных слов для одного и того же и необщепринята, т.е. никакой выгоды от нее нет.

Если вы им не пользуетесь это не значит что его нет. Я посмотрел — оно умеет как-то определять тип в рантайме.

Кто именно? Typeable? Нет, не умеет. Он умеет выдать рантайм-представление статического типа, да и то, если компилятор попросить. А просьба эта сводится к тому, что, если упрощать и переводить на привычный псевдосинтаксис, компилятор меняет


@derive(Typeable)
class Foo {};

на


class Foo : public Typeable
{
    public string getType() { return "я Foo!"; }
};

дописывая туда getType().


Если вы @derive(Typeable) там не написали, то компилятор ничего не допишет (и хорошо, потому что таскать рядом указатель на функцию в каждом инте — так себе идея для производительности).


Кстати, определите до конца термин "рантайм метка" он не отражает метка чего именно.

Любого куска данных. Короче, то, что вы называете типом.


А что у вас за IDE для плюсов?

clion, но для дебага я пользуюсь чистым gdb.


У вас там нет cимволов и RTTI? в окне watch нет колонки type для переменных?

Именно символы говорят дебаггеру, что вот эта переменная — указатель на int, поэтому результат его разыменования надо представить пользователю как int. В рантайме тут снова нет никаких типов (и хорошо, см. выше про производительность).


RTTI зависит от генерации vtbl по большому счёту. И оно в плюсах очень бедное именно потому, что больше никакой информации толком и не генерится. Вы даже не можете проверить в рантайме, является ли тип одного класса наследником типа другого класса (например, если у вас есть Base, где-то в другом месте D1 : Base и D2 : Base, и даны два указателя на Base, то вы не можете сказать, наследуется ли тип объекта по первому указателю от типа объекта по второму указателю).


С моей точки зрения, терминология, которую вы предлагаете требует введения разных слов для одного и того же и необщепринята, т.е. никакой выгоды от нее нет.

Наоборот! Понятия как раз предельно разные! Типизация помогает узнать, что программа имеет (или не имеет) определённые свойства, не запуская её. Рантайм-проверки этого не позволяют и позволить не могут.

В архитектуре «Эльбрус» такие аппаратные метки назывались тегами.
Думаю в PHP, как и в питоне можно проверять линтерами не в рантайме.

Скорее не линтерами, а статанализаторами. Да, если использовать все возможности языка на полную, не помогая анализатору тайпхинтами и аннотациями, то много ошибок типов будет как ложно положительных, так и ложно отрицательных, но тем не менее как современные IDE, так и отдельные статанализаторы широко используют информацию о типах из исходников.

Разве только чтоб обмануть работодателя (которого примерно бесконечно проще найти для PHP, чем для Idris).
Тот, кому первому пришла в голову идея назвать рантаймовый контроль типов «типизацией» — будет вечно гореть в аду за обман джуниоров.


А как по вашему это нужно называть?
Контролем типов, как и указано в мануале.

Типизация в PHP как была динамической и слабой, так и осталась. И нет никаких предпосылок к изменению этого положения.
Контролем типов
Вроде это по определению делается во всех системах с проверками типов. Ну там Rust, Haskell. На другом этапе, конечно.
Я не понимаю отчаянного сопротивления применению определенного уважаемого термина к РНР и попыток его замены на какой-нибудь другой, не такой уважаемый.
Типизация в PHP как была динамической и слабой, так и осталась
Кстати, вы будете гореть в аду
Тот, кому первому пришла в голову идея назвать рантаймовый контроль типов «типизацией» — будет вечно гореть в аду за обман джуниоров.
Если это не type (тип). Каким словом обобщить свойство поведения «строка», «число», «интерфейс» в ЯП? Чтобы можно было корректно спросить «Какой blabla у этой переменной?» и другой разработчик понял вопрос.
Если это не typing (типизация), то как сообщить другому человеку «Я придумал ЯП с динамическим blabla» и остаться понятым?
Чтобы можно было корректно спросить «Какой blabla у этой переменной?» и другой разработчик понял вопрос.

«Можно ли на этой переменной дёрнуть эту функцию?»


В языках с утиной типизацией (гкхм) у вас всё равно по-другому спросить и не получится по факту.


Если это не typing (типизация), то как сообщить другому человеку «Я придумал ЯП с динамическим blabla» и остаться понятым?

Можно просто сказать, что вы придумали язык без статической типизации.

«Можно ли на этой переменной дёрнуть эту функцию?»
Но если мы хотим донести, что эта переменная ведёт себя как string ибо помечена таковой средой выполнения, то нам придётся долго перечислять список функций (и всё равно можем не попасть, потому что у другого типа может быть такой же, но он к примеру несовместим со string). Нам же нужны обобщения.
вы придумали язык без статической типизации.
Это можно, да. Термин взаимоисключающий.

Проблема в том, что всё это противоречит естественному языку как средству коммуникации. Лучше было бы придумать для формальных понятий другие слова, например «типоид» и «типоизация». Тогда можно было бы смело поправлять других «Вот это ни в коем случае нельзя называть типоидом по определению», «в этом ЯП не может быть никакой типоизации» и никто бы и слова против не сказал.

Я не знаю, как это было с исторической перспективы, но сейчас частичное пересечение узкоспециального термина с широким общим играет отрицательную роль для первого.
Но если мы хотим донести, что эта переменная ведёт себя как string ибо помечена таковой средой выполнения, то нам придётся долго перечислять список функций (и всё равно можем не попасть, потому что у другого типа может быть такой же, но он к примеру несовместим со string).

Наверное, я не очень понимаю, какая практика работы в языках без статической типизации, да и потребности спрашивать про рантайм-поведение какого-то объекта у меня как-то особо не было, но разве в питоне не ровно так? Что вас не волнует то, что питон называет типом, а волнует только то, можно ли применить к нему какую-то функцию.


А в том же жс с неявными приведениями вообще всё сложно, как я понимаю.

Понятие типа — хоть в номинативном, хоть в структурном смысле — вполне может пригодиться в динамическом языке. Например, для перегрузки функций: перемножить две плотные матрицы — один метод, плотную и разреженную — другой, разреженную и диагональную — третий; сложить элементы с i-го по j-й — один метод для типа, который имеет доступ по индексу, другой для типа который позволяет только итерироваться. И т.п.
Но да, это не про питон.
Можно просто сказать, что вы придумали язык без статической типизации.

Это может быть и безтиповый язык типа популярных ассемблеров.

А еще смешнее, что нет контроля за этим контролем.
А джунам тем стоит взять JSP если уж на то пошло)

В "компайл-тайме" в клиентской коде мы не можем знать что загрузит автолоалер или какая имплементации интерфейса придёт. Вообще проверки не будет?

Компайл тайма нет. Проверка будет только при статическом анализе и канеш в рантайме. Поэтому индустрия пыха требует монструозного техпроцесса на нескольких стадиях.

Ну какой-то компайл тайм есть: преобразование в опкоды. В рамках одного класса можно было бы в нём что-то по минимум проверить, но вот весь проект проверить нереально, по крайней мере с доминирующей моделью автолоадинг классов.

Java на JIT, насчёт C# не могу сказать ничего. А 8 с JIT ещё только в альфе, первый релиз-кандидат вроде как только осенью будет, а сам релиз в декабре.
В пыхе компиляция пока что относится только к сборке самого бинарника руками) А наш с вами код интерпретируется, это сильно другой процесс.

В альфе, но есть :)


Тут о терминах можно спорить долго. javac запускает компиляцию в байт-код, который отдаётся виртуальной машине. Раньше она его просто интерпретировала, сейчас JIT везде или почти везде. php запускает компиляцию в байт-код, который отдаётся вирткальной машине. раньше она его просто интерпретировала, сейчас JIT в мастере. В чём качественная разница? В отсутствии файла с байт-кодом?

Вопрос ведь не в терминах, ну и не спорю, если грубо — то можно свести к фразе компилится.
Для меня лично компиляция — строго вне рантайма. Если код попадает в кучу когда пришли данные на обработку — интерпретация. Отсутствие файлика — огромная разница в процессе.
Ну и ещё у меня стойкое чувство, что вы меня стебете)
/ пошто пыхоиндуса обижаете? :( /

Ну вот JIT тогда не компиляция? Файлика нет же. :)


А если серьёзно, то в современной разработке грань между компиляторами и интерпретаторами размылась — слишком многое под капотом, на что программист никак повлиять не может обычно.

В динамических языках (и Форте) компилятор всегда присутствует в системе и может быть вызван в любой момент, в том числе и во время исполнения.

У вас слишком узкое представление.

Форт я ещё в самом начале 90-х затруднялся к чему отнести, настолько у него режимы интерпретации и компиляции перпелетены.


P.S. Точнее — сшиты :)

Не во время компоновки/загрузки?

PS На всякий случай подчеркну, это вопрос, а не утверждение.
Если кратко:
Проверка типов происходит точно на рантайме, когда данные переданы в поток (то есть код уже в куче)

Если развернуто:
1. В зависимости от версии пыха и правил типизации (strict_types) проекта на этапе разработки (локально) доступны:
1.1. Анализ самого IDE в режиме реального времени
Картинка
image

1.2 Встраиваемые пакеты для статического анализа codestyle
Картинка
image

1.3 Встраиваемые пакеты для стат анализа codequality
Картинка
image


2. Дальше в крупных проектах CI/CD, со стендами для предварительных тестов регрессии, интеграции, фича тестов и вероятнее всего 1.2 и 1.3 повторные.
Картинка
image


3. Дальше, в зависимости от критичности проекта, может быть ряд canary продакшн серверов, на которых крутятся «свои» юзеры, которые выступают в роли кроликов-тестировщиков.

4. Ну и сам прод собственно. Тут вызывается код, интерпретируется в псевдокод для виртуальной машины (например нгинкс), выполняется до определенного адреса, там происходит ошибка и бросается исключение (от нотиса до фатала) — вот последнее это рантайм.

А так, по топику могу сказать одно.
Типизация нисколько не спасает от багов на проде.
Чаще всего прод на пыхе страдает от кривой логики реализации бизнес-процесса или не до конца протестированных юзкейсов.
Орут о величии строгой типизации над динамически типизированными языками в основном фронтендеры, которые пересели с js на ts и решили, что они не верстальщики, а программисты =)
Нет. Вы очень глубоко ошибаетесь. «Статическая» — это на этапе компиляции. В PHP же любой контроль типов, даже контроль типов свойств классов и объектов — рантаймовый.

Для полей классов таки да.


private string $a = 10;

отлупит на этапе компиляции

тут скорее идет разговор не о компиляции как о таковой, а о самом моменте.
Компиляция всех файлов происходит в одно время или в разное. В PHP в момент обращения к файлу.
В Python не добавляют статическую типизацию, вы заблуждаетесь.
Хинты с mypy всё больше используется, по-моему. Как бы становясь best practice и правилом хорошего вкуса. Субъективно, конечно, потому что Python сообщество — тот еще (un)pythonic пузырь.

Не так плоха динамическая типизация, как ее сочетание со слабой, js, php привет вам.
Вот это уже взрывная смесь по производству багов.

«Сила» типизации Python преувеличена:
print((not None) + 7)
Сначала None автоматически преобразуется в bool, потом bool автоматически преобразуется в int.
Типичная слабая типизация.

Да, у Python отсутствует автоматическое преобразование число<->строка и возможности преобразования None ограничены. Но в остальном PHP может обеспечить более строгий контроль типов. Аннотации типов аргументов подпрограмм в Python не обеспечивают контроль типов — в отличие от PHP, в котором реализуется реальный контроль и типов аргументов (с возможностью отключения преобразования число<->строка), и типа возвращаемого значения.
Сначала None автоматически преобразуется в bool, потом bool автоматически преобразуется в int.
Типичная слабая типизация.

Оператор not возвращает True или False. Тип bool унаследован от int, поэтому в арифматическом смысле True всегда равен 1, а False всегда равен 0. У вас не получится сделать None + 1.

gaal@catalina monitoring % python3
Python 3.7.6 (default, Dec 30 2019, 19:38:26) 
[Clang 11.0.0 (clang-1100.0.33.16)] on darwin
Type "help", "copyright", "credits" or "license" for more information.
>>> 
>>> print((not None) + 7)
8
>>> print(None + 7)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: unsupported operand type(s) for +: 'NoneType' and 'int'
Главная фишка вот:
Python 3.7.5rc1 (default, Oct  8 2019, 16:47:45) 
[GCC 9.2.1 20190909] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> not []
True
>>> not "Oops"
False

Операция «not» применима к чему угодно. То есть там «None» не преобразуется в Bool. А что True/False — разновидности целых… это странно, но это Python унаследовал от C. Он ещё парочку странностей от него унаследовал…
То есть там «None» не преобразуется в Bool.

Спасибо за разъяснение, но я этого и не утверждал. Из моего сниппета четко видно, что None — это инстанс NoneType. А не Bool. А особенности работы not… ну, спасибо.

У вас не получится сделать None + 1.

>>> not (not None) + 1
False

В моих книжках написано, что not (not x) = x для всех допустимых x, значит, None эквивалентно not (not None).


Да, это всего лишь ещё один способ указать на unsoundness языка.


Edit: Кстати, почему False, а не 1 какой-нибудь, который я бы ожидал в С?


Edit2: А, потому что это не хаскель, и not не функция, поэтому надо больше скобочек


>>> (not (not None)) + 1
1

Но суть не меняется.

В моих книжках написано, что not (not x) = x для всех допустимых x, значит, None эквивалентно not (not None).

Ещё раз. У вас не получится сложить None и 1. Оператор not это логический оператор отрицания, который возвращает строго True/False. Двойное инвертирование True вернёт True и наоборот, эта цепочка из not not not [...] может быть бесконечной. Не понимаю, что мы обсуждаем?

Да, это всего лишь ещё один способ указать на unsoundness языка.

Ну, назовите это консистентностью языка. В целом проблемы нет, согласен.

Все языки делятся на два непересекающихся класса, к сожалению: неконсистентные и мёртые. В Haskell, скажем, Monad это не Applicative именно по той причине что лучше быть неконсистентным, чем мёртвым.

Да, это уже давно не так. Applicative/Monoid Proposal'у уже лет пять, если не больше. Semigroup сделали базовым классом для Monoid пару релизов ghc назад, MonadFail выделяют отдельно, и так далее.


Да, есть unsound-элементы, но они связаны с изначальными ошибками (или компромиссами) в дизайне системы типов, и о них думают, как бы их устранить.

Да, есть unsound-элементы, но они связаны с изначальными ошибками (или компромиссами) в дизайне системы типов, и о них думают, как бы их устранить.
Лучше бы они подумали как «людям снаружи» дать доступ ко всему этому.

Либо объявите GHC «единственной правильной версией» (и тогда версии языка будут соответствовать резлизам GHC), либо сделайте уж, как в C++, регулярные релизы. А то официальной версии 10 лет, а что из бесконечного количества расширений и дополнений, доступных после этого, считать «официальной частью языка» — «снаружи» понять невозможно.

Далеко не у всех есть возможность следить за всей «движухой», если они хотят попробовать Haskell на примере задачи генерации какого-нибудь отчёта.

А с устранением косяков вопрос сложный, на самом деле: в Python считается идеоматичным не писать в if всякие "== 0" или "== []" (хотя лично я это считают некрасивым как раз) из чего, как бы, очевидно следует, что и not должен работать со всеми типами — иначе будет нелогично.
Либо объявите GHC «единственной правильной версией» (и тогда версии языка будут соответствовать резлизам GHC)

Де-факто это уже давно так.


А с устранением косяков вопрос сложный

Особенно когда на них уже построена куча вещей.


Либо мне стоило бы ожидать меньшего и не требовать от хаскеля формальной soundness системы типов, но это как-то нечестно и непоследовательно.

Де-факто это уже давно так.
А как до этого догадаться? Захожу я на www.haskell.org (а куда надо было зайти?), открываю раздел с документацией — первым делом, первой ссылкой, меня отправляют на Learn You a Haskell for Great Good!, где есть прям целаю душешипательная история про то что Монада — это не Applicative. Ладно, это тьюториал, они часто не поспевают за развитием языка. Ищем описание языка… единственное, что там есть — это Haskell 2010. Если погуглить — можно на wiki найти информацию про Haskell'… ссылка ведёт на сайт, который не отвечает, а страничка на archive.org радостно сообщает, что Haskell Prime 2020 committee has formed — «свежая» новость от 2016го года.

Ну и куда мне идти, чтобы что-то узнать, а главное, как до этого догадаться?

Сравните с C++. Wikipedia отправляет на isocpp.org. Там есть анносы GCC 10.1 (релиз от 11 мая 2020го), есть ссылка на Core Guidelines, можно добраться до драфта (хотя было бы полезнее, если бы ссылка была бы поближе к корню isocpp.org, а так туда приходится идти через cppreference).

А где у Haskell-community что-то подобное?

P.S. У C++-комьюнити есть, правда, своя, особая фишка: бесконечные draftы. Попытка найти хоть чего-нибудь отрелизнутое — обречена на неудачу. Нужно некоторое время «повариться», чтобы понять, что это — следствие бюрократии ISO, которое привело к тому, что все и всегда используют draftы. Релиз, типа-вроде-как окончательная версия, никого не интересует настолько, что если draft будет говорить одно, а релиз — другое, то реализуют именно draft: их используют разработчики компиляторов, программисты и вообще все, кто мало-мальски интересуется C++. А релизы? Ну их ISO за деньги продаёт, можно купить и положить на полочку. Всё. Больше в них никакого смысла нету. Да, этот «секрет Полишинеля» сходу, на web-сайте не найти…

С discoverability всё очень плохо, я согласен. Плюс, часть коммьюнити старательно делает вид, что хаскель не скатывается в язык с единственной реализацией, и, кажется, кто-то даже до сих пор верит, что Haskell 2020 быть. А для того, чтобы решить описанные вами проблемы, надо, наконец, признать, что Haskell 2020 зафейлился, компиляторы кроме ghc по большому счёту мертвы, и так далее.

А я говорю, что описание типов — и есть описание процесса
Э? Вообще-то описание _процессов_ — это функции/процедуры.
и у функции есть интерфейс, а именно аргументы и возвращаемое значение, чьи типы хорошо бы знать
Обе системы типов (статическая и динамическая) имеют преимущества.
Код на динамических языках не только пишется легче, но и легче читается. Поэтому многие ошибки видны невооруженным глазом.
Но с определенного размера кодовой базы все связи уследить уже просто не возможно, и вот тут на помощь приходит статическая типизация.
В общем, для каждой задачи — свой инструмент.

Не совсем так. Динамически-типизированный код может вообще не отличаться от статически-типизированного, просто автоматический вывод.

Вывод типов — это хорошо, но работает он не всегда. Так или иначе компилятор все равно хочет «подсказок». По крайней мере в тех языках, с которыми работал я.

Или на статических легче читается. Прочитали сигнатуру функции — и все понятно, даже тело читать может быть не нужно.

TypeScript предлагает не самый удобный синтаксис, где декларация типов и имплементация смешиваются в одном предложении. Подход за который топит автор — сначала пишем типы, потом все остальное — не работает чисто синтаксически.
function foo (string) : string { } // error 

В хаскеле сделано удобнее. Но это имхо и вкусовщина, не буду спорить если у кого-то другое мнение.
Потому что имена аргументов, это так же часть сигнатуры и она важна для понимания, что функция делает.
В Вашем варианте foo я понятия не имею, что за строку она от меня хочет, но стоит написать вот так:
function foo(userName: string): string;
и все стало гораздо понятнее, хотя foo по прежнему не очень удачное имя…

И да, по-нормальному было бы вообще так:
function foo(userName: UserName): string;
но убогая структурная система типов тайпскрипта не дает это выразить нормально
Знаю я про них, но они все равно не работают нормально, ибо структурная типизация…

Всё прекрасно работает.


import {
  $mol_data_nominal as Unit,
  $mol_data_integer as Int,
} from "mol_data_all";

const Weight = Unit({ Weight : Int })
const Length = Unit({ Length : Int })

let len = Length(10)
len = Length(20) // Validate

len = 20 // Compile time error
len = Weight(20) // Compile time error
len = Length(20.1) // Run time error

let mass: typeof Weight.Value
mass = len // Compile time error
Вы плохо знаете историю. Это всё ALGOL.

А Delpha/Pascal — это уже «закат эпохи». Когда теоретики заизолировались у себя в башне, а практики начали делать «удивительные открытия», известные теоретикам в середине прошлого века.

Буду знать, что когда я пишу


lteCongRight : { l, r1, r2 : Nat } -> (prf : r1 = r2) -> l `LTE` r1 -> l `LTE` r2

то это на самом деле паскаль.

Буквально вчера делал у себя на проекте похожую штуку. Работает :)

type UserName = string & { readonly tag: unique symbol };
type Password = string & { readonly tag: unique symbol };

const nameOf = (name: string) => name as UserName;

function stringOf(name: UserName): string {
  return name;
}

stringOf(nameOf("bingo347")) // OK
stringOf("bohdan-shulha") // Argument of type '"bohdan-shulha"' is not assignable to parameter of type 'UserName'.
stringOf("hellowrld" as Password) // Argument of type 'Password' is not assignable to parameter of type 'UserName'.

const nameOf = (name: string) => name as UserName;
Вот я и говорю, что это не работает, любую строку можно просто привести к типу UserName без доказательства последнего
А как доказать, что строка, которая пришла с сервера, это действительно UserName, а не что-то иное? Предполагается, что приведение типов будет использоваться в фабриках, а по приложению будут ползти уже Value Object. Этот способ, как минимум, гарантирует, что нельзя будет случайно передать рандомную строку вместо UserName.

Я могу ошибаться, но вы именно о таком поведении писали в комментарии выше.
А как доказать, что строка, которая пришла с сервера, это действительно UserName, а не что-то иное?
Проверить, что она соответствует всем ограничениям на тип UserName, если проверка успешна — я получу тип UserName, иначе получу ошибку. Другого способа получить тип UserName в программе нет, поэтому ему можно доверять. А вот типу, в который можно просто кастануть любую строку я доверять не могу, он для меня бесполезен.

Вот чего мне в TypeScript не хватает так таких проверок в рантайме. Писать их руками может быть очень утомительно, хорошо если хоть базовую проверку сделаешь перед тем как в гварде true вернешь.

Конечно динамическая типизация может иметь свои преимущества у определённых ситуациях. Например когда пишешь какие-нибудь матмодели или что-то в этом роде.

Но я согласен с автором что «в продакшене» всё-таки лучше использовать языки со статической типизацией.

Когда пишешь матмодели, очень желательно не сложить случайно метры с секундами.

К сожалению, не видел еще удобных средств в менйстримных ЯП, позволявших легко избежать складывания условных int и int (где первый — метры, второй — секунды). Надо оборачивать, а всем влом. И библиотеки всякие все равно будут принимать и отдавать int-ы.

К счастью, не всегда нужно ограничивать себя мейнстримными ЯП в смысле джавы и C++.

Что Вам там больно? «4s + 500ms» сработает и даст четыре с половиной секунды, а «4s + 500m» не скомпилится, поскольку секунды с метрами не складываются.
Так вот же и статья об этом: либо мы описываем все типы и получаем типобезопасность, либо мы складываем футы с метрами и наш марсоход пролетает мимо Марса (true story).

Ну и, кроме того, всё уже сделано до нас: Boost.Unit

Писать много много оберток над тривиальными математическими операциями и сравнениями. Фактически копипаст. Нельзя просто сказать что вот этот int будет метры, этот секунды, а этот тугрики. Плюс взаимодействие сложных типов вышеупомянутое.

Например, написать литерал/тип для результата операции 4s * 5kg. Ну и да, много копипаста.

Там ограничения есть, например, для целого это всегда long long int, а зачем мне это, если я метры хочу только int32.
Другое дело, что можно все в классы обернуть… тогда точно, одно с другим не сложишь. Но это конечно дополнительно писать придется кода...

В C++ как раз сложишь, если оператор + переопределишь :)

И как так просто метры с миллиметрами сложить? Переопределить то можно… придется делать столько этих операторов, сколько типов собираетесь складывать.

Вообще не проблема: Фаренгейты с Цельсиями складывать в принципе нельзя (даже в физике), но и то и другое можно перевести в Кельвины или Ранкины. И там уже складывать.

Кто запретил? Фаренгейты и Цельсии изоморфны, можно перевести одно в другое и сложить. Да, тут есть неоднозначность, каким должен быть тип результата, но это вполне может зависеть от вызывающего кода, и какой тип он там ожидает.

Именно что аналогично — то есть неизвестно что получится в результате. Кельвины и Ранкины скаладывать можно, а Цельсии, Фаренгейты и Реомюры — только если знать что они означают: собственно температуру или разницу температур. При этом температуру с температурой складывать нельзя.
температуру с температурой складывать нельзя
Вот у меня литр воды 20 градусов и 5 литров 50 градусов, как мне посчитать температуру смеси (пренебрегая теплопередачей посуде и воздуху)? Всегда думал что для этого нужно средневзвешенное значение находить (в кельвинах), а для этого множить на скаляры и складывать.
Научный коммунизм вами усвоен на отлично, цитаты вы дёргать научились. А если хотите увидеть ответ — то прочитайте все пять строчек. Это не так много.
Вам нужно описывать операцию среднего взвешенного. Чтобы библиотека (условно) через unsafe получала скаляры, делала математику и возвращала усредненную температуру. Складывать температуру нельзя, можно усреднять. Т.е. можно складывать только при условии последующего деления, например.
Самое простое — это сделать такие операции:
[цельсий] — [цельсий] = [кельвин]
[кельвин] + [цельсий] = [цельсий]
ну и для кельвина всякие сложения друг с другом и умножения на число.
И (хоть я настолько и не люблю доведение до такого) поэтому в VHDL надо вообще всё полностью описывать, включая преобразования.
Фаренгейты и Цельсии изоморфны, можно перевести одно в другое и сложить.
В том-то и дело, что они нифига не изомрфны. Сколько будет 1°C + 1°F? А фиг его знает: может быть 159°C, может быть -3049°C. И без дополнительной информации вы это не узнаете.

Да, тут есть неоднозначность, каким должен быть тип результата, но это вполне может зависеть от вызывающего кода, и какой тип он там ожидает.
Если бы речь шла только о типе результата — беды бы не было. К сожалению меняется ещё и значение этого самого результата.
В том-то и дело, что они нифига не изомрфны. Сколько будет 1°C + 1°F? А фиг его знает: может быть 15⁄9°C, может быть -304⁄9°C. И без дополнительной информации вы это не узнаете.

Не понял, как так получилось?