Правильно ли я понимаю системы типов?

Question

Следующие утверждения представляют мое понимание систем типов (которое страдает от слишком небольшого практического опыта вне мира Java); пожалуйста исправьте все ошибки.

Статическое / динамическое различие кажется довольно четким:

• Статически типизированные языки присваивают каждой переменной, полю и параметру тип, а компилятор предотвращает присваивания между несовместимыми типами. Примеры: C, Java, Pascal.
• Языки с динамической типизацией рассматривают переменные как универсальные ячейки, которые могут содержать все, что вы хотите - типы проверяются (если вообще) только во время выполнения, когда вы фактически выполняете операции со значениями, а не когда вы присваиваете их. Примеры: Smalltalk, Python, JavaScript.
• Вывод типа позволяет статически типизированным языкам выглядеть (и иметь некоторые преимущества) динамически типизированных, выводя типы из контекста, так что вам не нужно объявлять их в большинстве случаев. время - но в отличие от динамических языков, вы не можете, например, используйте переменную для первоначального хранения строки, а затем присвойте ей целое число. Примеры: Haskell, Scala

Я гораздо менее уверен в сильном / слабом различении и подозреваю, что оно не очень четко определено:

• Строго типизированные языки присваивают каждому значению среды выполнения тип и разрешают выполнять только операции, определенные для этого типа, в противном случае существует явная ошибка типа.
• Слабо типизированные языки не имеют проверок типов во время выполнения - если вы попытаетесь выполнить операцию со значением, которое оно не поддерживает, результаты непредсказуемы. Это может на самом деле сделать что-то полезное, но, скорее всего, вы получите поврежденные данные, сбой или некоторую нешифруемую вторичную ошибку.
• Кажется, есть как минимум два разных типа слабо типизированных языков (или, возможно, континуум):
  • В C и ассемблере значения в основном представляют собой наборы битов, так что все возможно, и если вы заставите компилятор разыменовать первые 4 байта строки с нулевым символом в конце, вам лучше надеяться, что он приведет куда-то, что не содержит легальной машины код.
  • PHP и JavaScript также обычно считаются слабо типизированными, но не рассматривают значения как непрозрачные битовые сегменты; однако они будут выполнять неявные преобразования типов.
• Но эти неявные преобразования, кажется, применимы в основном к строковым / целочисленным / переменным числам - действительно ли это оправдывает классификацию как слабо типизированных? Или есть другие проблемы, в которых система типов этих языков может скрывать ошибки?

Answer 1

Я гораздо менее уверен в сильном / слабом различении и подозреваю, что оно не очень четко определено.

Вы правы: это не так.

Это то, что Бенджамин С. Пирс, автор Типы и языки программирования и Расширенные типы и языки программирования должен сказать:

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

Лука Карделли в своей статье Typeful Programming определяет это как отсутствие непроверенных ошибок типов во время выполнения. Тони Хоар называет это точно таким же свойством "безопасностью". Другие газеты называют это «безопасность типов» или просто «безопасность».

Марк-Джейсон Доминус написал классическую рутину об этом пару лет назад в группе новостей comp.lang.perl.moderated, в дискуссии о том, был ли Perl строго типизирован. В этой статье он заявляет, что всего за несколько часов исследований ему удалось найти 8 различных, порой противоречивых определений, в основном из уважаемых источников, таких как учебники для колледжей или рецензируемые статьи. В частности, эти тексты содержали примеры, которые предназначались для того, чтобы помочь учащимся отличать языки со строгой и слабой типизацией, и в соответствии с этими примерами, C строго типизирован, C слабо типизирован, C ++ строго типизирован, C ++ слабо типизирован, Lisp - строго типизированный, Lisp слабо типизированный, Perl строго типизированный, Perl слабо типизированный. (Это устраняет путаницу?)

Определение only , которое я видел последовательно применяемым:

• строго типизированный : мой язык программирования
• слабый тип : ваш язык программирования

Answer 2

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

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

Хотя я думаю, что вы поняли концепцию, ваши маркеры не дают понять, что вывод типа - это просто особый случай статической типизации . В большинстве языков с выводом типа аннотации типов являются необязательными, но не обязательно во всех контекстах. (Пример: подписи в ML.) Усовершенствованные системы статических типов часто дают вам компромисс между аннотациями и логическим выводом; например, в Haskell вы можете вводить полиморфные функции более высокого ранга (слева от стрелки), но только с аннотациями. Таким образом, если вы хотите добавить аннотацию, вы можете заставить компилятор принять программу, которая будет отклонена без аннотации. Я думаю, что это волна будущего в выводе типа.

Идеи «сильной» и «слабой» типизации я бы охарактеризовал как , бесполезные , потому что они не имеют общепризнанного технического значения. Строгая типизация обычно означает, что в системе типов нет лазеек, в то время как слабая типизация означает, что система типов может быть подорвана (аннулируя любые гарантии). Термины часто используются неправильно для обозначения статической и динамической типизации. Чтобы увидеть разницу, подумайте о C: язык проверяется на тип во время компиляции (статическая типизация), но существует множество лазеек; вы можете в значительной степени привести значение любого типа к другому типу того же размера - в частности, вы можете свободно приводить типы указателей. Паскаль был языком, который предназначался для строгой типизации, но, как известно, имел непредвиденную лазейку: вариант записи без тега.

Реализации строго типизированных языков часто приобретают лазейки со временем, обычно, так что часть системы времени выполнения может быть реализована на языке высокого уровня. Например, в Objective Caml есть функция с именем Obj.magic, которая во время выполнения просто возвращает свой аргумент, но во время компиляции преобразует значение любого типа в значение любого другого типа. Мой любимый пример - это Modula-3, дизайнеры которого назвали свою конструкцию литья типов LOOPHOLE.

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

Answer 3

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

В таких языках, как TCL и Bourne Shell, «основным» типом значения является строка. Доступны числовые операторы, которые неявно приводят входные значения из строкового представления и результирующие значения к строковому представлению. Их можно считать примерами динамических слабо типизированных языков.

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

Answer 4

Я считаю сильным / слабым концепцию неявного преобразования, и хорошим примером является добавление строки и числа. В строго типизированном языке преобразование не произойдет (по крайней мере, во всех языках, которые я могу придумать), и вы получите ошибку. Языки со слабой типизацией, такие как VB (с выключенным Option Explicit) и Javascript, будут пытаться привести один из операндов к другому типу.

В VB.Net с опцией «Строгое выключено»:

    Dim A As String = "5"
    Dim B As Integer = 5
    Trace.WriteLine(A + B) 'returns 10

С Option Strict On (превращая VB в строго типизированный язык) вы получите ошибку компилятора.

В JavaScript:

    var A = '5';
    var B = 5;
    alert(A + B);//returns 55

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

Answer 5

По-видимому, существует как минимум два разных типа слабо типизированных языков (или, возможно, континуум):

• В C и ассемблере значения в основном представляют собой наборы битов, так что все возможно, и если вы заставите компилятор разыменовать первые 4 байта строки с нулевым символом в конце, вам лучше надеяться, что он приведет куда-то, что не содержит легальной машины код.

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

Answer 6

Может быть эта книга может помочь. Будьте готовы к математике. Если я правильно помню, «нематематическим» утверждением было: «Строго набран: язык, на котором я чувствую себя безопасным для программирования».

Answer 7

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

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

Answer 8

Хм, тоже не знаю больше, но я хотел упомянуть C ++ и его неявные разговоры (неявные конструкторы). Это может быть также примером слабой типизации.