Основные понятия систем языковых типов

Question

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

Я слышал / читал, что существует 3 типа классификации: динамическая и статическая, сильная и слабая, безопасная и небезопасная.

Некоторые вопросы:

• Есть ли другие?
• Что означает каждый из них?
• Если язык позволяет вам изменять тип переменной во время выполнения (например, переменная, которая использовалась для хранения целого, позже используется для хранения строки), к какой категории это относится?
• Как Python вписывается в каждую из этих категорий?
• Что еще я должен знать о системах типов?

Большое спасибо!

Answer 1

1) Видимо, есть и другие: http://en.wikipedia.org/wiki/Type_system

2)

Dynamic => Проверка типа выполняется во время выполнения (выполнения программы), например Python.

Static (в отличие от динамического) => Проверка типа выполняется во время компиляции, например, C ++

Strong => Как только система типов решает, что конкретный объект принадлежит к типу, она не позволяет использовать его в качестве другого типа. например Python

Weak (в отличие от Strong) => Система типов позволяет типам объектов изменяться. например Perl позволяет читать число как строку, а затем снова использовать его как число

Type safety => Я могу лучше всего описать с помощью оператора 'C', например:

x = (int *) malloc (...);

malloc возвращает (void *), и мы просто приводим его к типу (int *). Во время компиляции нет проверки того, что указатель, возвращаемый функцией malloc, на самом деле будет размером целого числа => Некоторые операции C не являются безопасными по типу.

Мне сказали, что некоторые «чисто функциональные» языки по своей природе безопасны по типу, но я не знаю ни одного из этих языков. Я думаю, что Standard ML или Haskell были бы безопасны для типов.

3) «Если язык позволяет вам изменять тип переменной во время выполнения (например, переменная, которая использовалась для хранения целого, позже используется для хранения строки), к какой категории это относится?»:

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

4) Python: он динамически и строго типизирован. Безопасность типов - это что-то Я не знаю Python (и сам тип безопасности) достаточно, чтобы что-то сказать.

5) «Есть ли что-то еще, что я должен знать о системах типов?»: Может быть, читаете книгу, которую предлагает @BasileStarynkevitch?

Answer 2

Вы спрашиваете много здесь :) Система типов - это специальная область информатики!

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

int answer() {
   if(true) { return 42; } else { return "wrong"; }
}

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

Конечно, вы могли бы улучшить систему типов, чтобы фактически обнаружить, что ветвь else никогда не происходит. Вы хотите улучшить систему типов, чтобы отклонить как можно меньше программ. Вот почему система типов на протяжении многих лет обогащалась, чтобы поддерживать все больше и больше уточнений (например, обобщенных и т. Д.)

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

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

Что еще я должен знать о системах типов?

О да! :)

Счастливого погружения в мир систем типов!

Answer 3

Предлагаю прочитать B.Pierce's Типы и языки программирования книгу. И я также предлагаю изучить немного статически типизированного языка с выводом типа, такого как Ocaml или Haskell.

Answer 4

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

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

Ключевая концепция систем типов называется разумность .Система типов является надежной, если она гарантирует, что значение не может быть использовано неуместной функцией.Грубо говоря, система неправильного типа имеет «дыры» и бесполезна.Система типов ISO C89 является надежной, если вы удаляете приведения (и пустые * преобразования), и несостоятельной, если вы разрешаете их.Система типов ISO C ++ несостоятельна.

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

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

Вот ключевой вопрос: объясните, почему типизация ОО слишком слаба, чтобы допускать ООиспользоваться в качестве общей парадигмы развития.[Подсказка: ОО не может обрабатывать отношения]