Является ли Haskell строго типизированным языком программирования?

Ответ 1

Статические - типы известны во время компиляции. Java и Haskell имеют статическую типизацию. Также C/C++, С#, Go, Scala, Rust, чтобы перечислить еще несколько.

Статически типизированный язык может иметь или не иметь вывод типа. В Java почти полностью отсутствует вывод типа (но он очень медленно меняется, чуть-чуть); Haskell имеет полный вывод типа (за исключением некоторых очень продвинутых расширений).

(Вывод типов - это когда вам нужно только объявить минимальное количество типов вручную, например, var isFoo = true и var person = new Person(), а не bool isFoo = ... и Person person = ....)

Динамический - Python, JavaScript, Ruby, PHP, Clojure (и Lisps в целом), Prolog, Erlang и т.д. Можно также назвать "unityped"; Динамическая типизация может быть "эмулирована" в статических настройках, но обратное неверно, за исключением использования внешних инструментов статического анализа. Некоторые языки позволяют смешивать динамический и статический (см. постепенный ввод).

Некоторые языки включают статическую типизацию для одного или нескольких модулей, применяемых во время импорта, например: Python + Mypy, Typed Clojure, JavaScript + Flow, PHP + Hack, чтобы назвать несколько.

Сильные - значения, которые должны рассматриваться как Cat, всегда таковы; попытка обращаться с ними как с Dog приведет к громкому meeewww... Я имею в виду ошибку.

Слабый - это фактически сводится к 2 подобным, но отличным вещам: приведение типов (например, "5"+3 равно 8 в PHP - или делает это!) И реинтерпретация памяти (например, (int) someCharValue или (bool) somePtr в C, и C++, но C++ хочет, чтобы вы прямо сказали reinterpret_cast). Так что на самом деле слабое принуждение и слабая реинтерпретация, и разные языки слабы одним или обоими этими способами.

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

Существуют языки со всеми 4 возможными комбинациями и их вариациями/градациями.

Haskell статичен + сильный; конечно, у него есть unsafeCoerce, поэтому он может быть статичным + иногда немного слабым для интерпретации, но unsafeCoerce очень недоволен, за исключением экстремальных ситуаций, когда вы уверены, что что-то происходит, но просто не можете убедить компилятор, не возвращаясь назад и не пересказывая всю историю по-другому.

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

Python является динамическим + почти полностью надежным - нет никаких типов, известных по какой-либо строке кода до достижения этой строки во время выполнения, однако значения, которые существуют во время выполнения, действительно имеют типы, связанные с ними, и невозможно переосмыслить память. Неявные принуждения также сведены к значимому минимуму, поэтому можно сказать, что Python имеет силу 99,9% и силу принуждения 0,01%.

PHP и JavaScript являются динамическими + в основном слабыми - динамическими, в которых ничего не имеет типа, пока вы не выполните и не проанализируете его содержимое, а также слабыми в том, что принуждения происходят постоянно и с вещами, которые вы никогда не ожидаете принуждения, если только вы не вызываете методы и функции и не используете встроенные операции. Эти принуждения являются источником большого юмора в Интернете. Нет никаких реинтерпретаций памяти, поэтому PHP и JS слабо принудительны.

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

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

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

Одна последняя иллюстрация

При динамической типизации все кошки, собаки и даже слоны (на самом деле целые зоопарки!) Упакованы в коробки одинакового размера.

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

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

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

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

Благодаря меткам и четким правилам работы с коробками с разными метками можно использовать автоматические/механизированные логические рассуждения, чтобы делать выводы о том, что система логистики не будет делать или будет делать наверняка (статическая проверка, формальное подтверждение или наименьшее количество псевдо-доказательств (например, QuickCheck). Некоторые аспекты логистики все еще должны быть проверены с помощью пробных запусков, например, правильно ли клиент по логистике выбрал клиента. (интеграционное тестирование, приемочное тестирование, проверка работоспособности конечного пользователя).

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

Но если вы добавите ярлыки к коробкам, все равно важно, чтобы кошки Франкенштейна помещались в кошачьи коробки. (статическая + слабая типизация)

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

Ответ 2

Кажется, вы смешиваете динамическую/статическую и слабую/сильную типизацию.

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

Слабая или сильная типизация - это возможность предсказать ошибки типа только из сигнатур функций.

Haskell как статически, так и строго типизирован.

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

EDIT: Но, как сказал goldenbull, эти типизирующие понятия четко не определены.

Ответ 3

Он строго типизирован. См. Раздел 2.3 здесь: Почему Haskell имеет значение

Ответ 4

Я думаю, вы говорите о двух разных вещах.

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

Сильная типизация - это еще одна тема. Да, haskell строго типизирован, и поэтому большинство языков FP. Сильная типизация дает FP возможность "вывода типа", которая является мощной для устранения скрытых ошибок во время компиляции и помогает уменьшить размер исходного кода.

Может быть, вы сравниваете haskell с python? Python также строго типизирован. Разница между haskell и python - "статическая типизация" и "динамическая типизация". Фактическое значение термина "Сильный тип" и "Слабый тип" неоднозначно и нечетко. Это еще одна длинная история...