или Когда побеждает статическая типизация
Статическая типизация — это прекрасное обещание того, что автоматизированная статическая проверка правильности типов может сделать программы более простыми в написании, чтении, сопровождении и более правильными. Для тех, кто испытал прозрение «если компилируется, значит работает» в Haskell, это кажется выполненным обещанием.
Тем не менее, все, кроме самых догматичных сторонников, признают, что статическая типизация — это не только единороги и радуги. И все же когда-нибудь это может быть. Вот видение возможного будущего, в котором статическая типизация безоговорочно победила и отправила динамические языки в древность.
- Статические системы типов теперь достаточно развиты, чтобы любая полезная программа могла быть проверена статически. Кроме того, любая концептуально простая программа может быть представлена с использованием таких же простых типов.
- Ошибки от проверки типов содержательны и понятны.
- Больше нет класса программ, которые можно было бы написать более ясно и просто на динамическом языке, чем программы со статическими типами.
- Междисциплинарные программисты (статистики, ученые, инженеры, художники, музыканты, любители) постоянно выбирают статические языки из-за их непревзойденной простоты использования и производительности во всех дисциплинах.
- Команды, использующие языки со статической типизацией, лишили работы команды, использующие языки с динамической типизацией, постоянно предоставляя продукты более высокого качества за меньшее время.
- Все достижения в области программного обеспечения за последние несколько десятилетий были связаны с исследованиями систем статических типов.
- Более того, за последние несколько десятилетий ни одна интересная программа не была написана на динамическом языке.
- Все, что было, хотя их и не было, вскоре после этого было переписано более элегантно и правильно с использованием статически типизированного языка.
- В настоящее время общепризнанно и общепризнано, что время, потраченное на изучение тонкостей современных систем типов, объективно тратится лучше, чем время, посвященное любому другому занятию, связанному с программным обеспечением.
- Учебники по монадам — это решаемая проблема.
- Теперь программисты выбирают языки (и принимают все решения по этому вопросу), используя рациональные аргументы, основанные на эмпирически проверенных фактах, или, альтернативно, результаты соответствующих, хорошо спланированных, рецензируемых, крупномасштабных исследований, которые точно отражают сложную и динамичную реальность. мировые условия разработки программного обеспечения.
- Emacs был переписан в Idris. Во время перезаписи обнаружено несколько ошибок типов, в том числе одна, ответственная за мизинец Emacs, и одна, ответственная за Эрика С. Рэймонда.
- Развитая инопланетная цивилизация установила первый контакт и предоставила человечеству исходный код ядра искусственного интеллекта своего космического корабля. Подсказка: это не написано на JavaScript.
- Обнаружено доказательство существования Бога с помощью Кока. Понимая, что, возможно, он знает обо всем не лучше всех, Ричард Докинз приносит формальные, искренние извинения за все, что он когда-либо сказал за пределами сферы эволюционной биологии.
