Статическая проверка типов в эрланге
Я медленно влюбляюсь в Эрланга, и у меня только одна большая, БОЛЬШАЯ проблема.
Я большой поклонник таких языков, как Standart ML и ocaml с их сильной статической проверкой типов.
Есть ли хороший и чистый способ ввести некоторую статическую проверку типов в erlang. Я смотрю на -type а также -spec аннотаций.
У кого-нибудь есть хорошее решение?
5 ответов
Я был там! Я люблю OCaml и Erlang и регулярно их использую.
К тому времени, когда я начал использовать Erlang, у меня был многолетний опыт работы с OCaml. Мне потребовалось несколько недель, чтобы приспособиться к тому факту, что в компиляторе нет статического средства проверки типов. Но после этого боль полностью прошла.
В определенной степени обходиться без проверки типов - стоящее занятие. Для меня это был поучительный опыт и действительно сделал меня лучшим программистом.
Однако для Эрланга существует внешняя статическая проверка типов, называемая Dializer. Я нахожу это очень полезным. Проблема в том, что вам нужно звонить отдельно, и это медленно. Запуск его время от времени (например, перед фиксацией кода или как часть автоматизированной сборки) прекрасно работает. Я никогда не пробовал запускать его после каждой компиляции, так как было бы слишком отвлекаться, чтобы ждать, пока он не завершится.
Проверьте инструмент Dialyzer
Dialyzer - это инструмент статического анализа, который выявляет несоответствия программного обеспечения, такие как ошибки определенного типа, код, который стал мертвым или недоступным из-за некоторых ошибок программирования, ненужных тестов и т. Д. В отдельных модулях Erlang или целых (наборах) приложений.
На протяжении многих лет было несколько попыток построить системы типов поверх Erlang. Одна из таких попыток произошла еще в 1997 году, проведенная Саймоном Марлоу, одним из ведущих разработчиков компилятора Glasgow Haskell, и Филипом Уодлером, который работал над дизайном Haskell и внес вклад в теорию монад (см. Статью о системе типов)., Джо Армстронг позже прокомментировал статью:
Однажды Фил позвонил мне и объявил, что а) Эрлангу нужна система типов, б) он написал небольшой прототип системы типов и в) у него был годичный отпуск, и он собирался написать систему типов для Эрланга и " мы были заинтересованы? "Ответ -" Да ".
Фил Уодлер и Саймон Марлоу работали над системой типов более года, и результаты были опубликованы в [20]. Результаты проекта были несколько разочаровывающими. Начнем с того, что только подмножество языка было проверяемым по типу, главное упущение - отсутствие типов процессов и межпроцессных сообщений проверки типов.
Я в основном использую -spec а также -type для документации: вы пишете спецификации с -spec, затем проверьте его с помощью TypEr и затем (после добавления дополнительной информации в формате edoc) сгенерируйте документацию
С некоторых пор появился еще и . Отказ от ответственности: я один из участников.
Gradualizer — средство проверки статического типа для Erlang с поддержкой постепенной типизации . Он может определить некоторые типы, но в основном опирается на спецификации функций. Он проверяет соответствие тела функции ее объявленной спецификации, а также согласованность спецификации вызываемого объекта с переданными аргументами. Он поддерживает эквирекурсивные типы (пользовательские типы, которые расширяются до пользовательских типов), типы объединения, ограниченную форму типов пересечений (многопредложенные спецификации, т.е. перегруженные функции).
Gradualizer написан на Erlang, поэтому вклад сообщества должен быть возможен. С недавнего времени он может самопроверяться, не сообщая об ошибках. Эта работа еще не завершена, но она находится на продвинутой стадии и охватывает практически весь синтаксис Erlang (кортежи, записи, карты и т. д.). Благодаря тестированию его на самом себе, мы знаем, насколько он уже удобен (или неудобен) по сравнению с написанием нетипизированного Erlang, и можем сосредоточиться на наиболее важных вещах, которые необходимо улучшить в дальнейшем. Он поставляется с плагином Rebar3 и интерфейсом CLI.
Проверьте это Gradualizerна GitHub или HexDocs!