Означает ли нетипизированный также динамически типизированный в академическом мире CS?

Да, это стандартная практика в академической литературе. Чтобы понять это, полезно знать, что понятие «тип» было изобретено в 1930-х годах в контексте лямбда-исчисления (на самом деле, даже раньше, в контексте теории множеств). С тех пор возникла целая ветвь вычислительной логики, известная как «теория типов». Теория языков программирования основана на этих основах. И во всех этих математических контекстах «тип» имеет особое, устоявшееся значение.

Терминология «динамическая типизация» была изобретена намного позже - и это противоречие в терминах общего математического использования слова «тип».

Например, вот определение «системы типов», которое Бенджамин Пирс использует в своем стандартном учебнике Типы и языки программирования:

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

Он также отмечает:

Слово «статический» иногда добавляется явно - например, мы говорим о «статически типизированном языке программирования» - чтобы отличить виды анализа времени компиляции, которые мы рассматриваем здесь, от динамической или скрытой типизации, присутствующей в таких языках, как Scheme (Sussman and Steele, 1975; Kelsey, Clinger, and Rees, 1998; Dybvig, 1996), где теги типа времени выполнения используются для различения различных типов структур в куче. Такие термины, как «динамически типизированный», возможно, неверны и, вероятно, должны быть заменены на «динамически проверяется», но использование стандартное.

Похоже, что большинство людей, работающих в этой области, разделяют эту точку зрения.

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

PS: И, FWIW, я одновременно являюсь академическим исследователем систем типов и неакадемическим разработчиком JavaScript, поэтому мне приходится жить с расколом. :)

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

Боб Харпер любит говорить, что такие языки, как Scheme, Javascript и т. Д., Следует считать типизированными языками только с одним типом: значением. Я склоняюсь к этой точке зрения, поскольку она позволяет построить последовательное мировоззрение, используя только один типовой формализм.

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

P.P.S. К оригинальному плакату: когда дело касается языков программирования и особенно систем типов, информация в Википедии некачественная. Не верь этому.

Я изучил это и обнаружил, что ответ на ваш вопрос простой и удивительно «да»: академические типы CS или, по крайней мере, некоторые из них, действительно используют «нетипизированный» для обозначения «динамически типизированный». Например, в третьем издании Programming Languages: Principles and Practices (Кеннет С. Лауден и Кеннет А. Ламберт, опубликовано 2012 г.) говорится следующее:

Языки без систем статического типа обычно называются нетипизированными языками (или языками с динамической типизацией). К таким языкам относятся Scheme и другие диалекты Lisp, Smalltalk и большинство языков сценариев, таких как Perl, Python и Ruby. Обратите внимание, однако, что нетипизированный язык не обязательно позволяет программам повреждать данные - это просто означает, что все проверки безопасности выполняются во время выполнения. []

[ссылка] (примечание: в оригинале выделено жирным шрифтом) и далее используется «нетипизированный» именно так.

Я нахожу это удивительным (почти по тем же причинам, что и Афришке и Адам Михалцин), но вот вы где. :-)

Отредактировано для добавления: вы можете найти больше примеров, подключив "untyped languages" к Поиску книг Google. Например:

[] Это основной механизм сокрытия информации во многих нетипизированных языках. Например, схема PLT [4] использует генеративные structs, []

Джейкоб Мэтьюз и Амаль Ахмед, 2008 г. [ссылка]

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

Чарльз Консель, 1990 г. [ссылка]

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

Разумеется, поиск не говорит о том, есть ли исследователи, которые отвергают эту идентификацию и не считают эти языки "нетипизированными". Что ж, я нашел это:

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

кто-то (не могу сказать кто), 1998 год [ссылка]

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

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

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

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

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

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

Хотя верно, что большинство исследователей CS, которые пишут о типах, по существу рассматривают только языки с синтаксически производными типами как типизированные языки, гораздо больше из нас, использующих динамически / латентно типизированные языки, недовольны таким использованием.

Я считаю, что существует 3 типа [SIC] языков:

Нетипизированный - только оператор определяет интерпретацию значения - и он обычно работает с чем угодно. Примеры: Ассемблер, BCPL.

Статически типизированный - выражения / переменные имеют связанные с ними типы, и этот тип определяет интерпретацию / валидность оператора во время компиляции. Примеры: C, Java, C ++, ML, Haskell.

Динамически типизированные - значения имеют связанные с ними типы, и этот тип определяет интерпретацию / действительность оператора во время выполнения. Примеры: LISP, Scheme, Smalltalk, Ruby, Python, Javascript.

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

Все это приводит к абсурдным заявлениям, например, что C ++ безопаснее Python, потому что он (статически типизирован), тогда как правда в том, что Python искробезопасен, в то время как с C ++ можно оторваться.

Этот вопрос касается семантики

Если я дам вам эти данные: 12 какой это тип? У вас нет возможности узнать наверняка. Может быть целым числом - может быть числом с плавающей запятой - может быть строкой. В этом смысле это очень "нетипизированные" данные.

Если я дам вам воображаемый язык, который позволяет вам использовать такие операторы, как «добавить», «вычесть» и «объединить» с этими данными и некоторыми другими произвольными частями данных, «тип» будет несколько неактуальным (для моего воображаемого языка) (пример : возможно, add(12, a) дает 109, что 12 плюс значение ascii a).

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

Однако - и переходя к точке зрения Брендана - если я скажу вам, что «Мой возраст 12» - тогда 12 имеет тип - по крайней мере, мы знаем, что это числовой. С контекстом все имеет тип - независимо от языка.

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

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

Javascript может позволить вам делать самые разные безумные вещи, не считая их «ошибками». Это не значит, что то, что вы делаете, логично. Это разработчик должен работать.

Является ли система / язык, которые не обеспечивают безопасность типов во время компиляции / сборки / интерпретации, «нетипизированными» или «динамически типизированными»?

Семантика.

ИЗМЕНИТЬ

Я хотел добавить сюда кое-что, потому что некоторые люди, кажется, зацикливаются на том, что «да, но в Javascript есть некоторые« типы »».

В своем комментарии к чужому ответу я сказал:

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

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

Например, чтобы выполнить ту же операцию с C #, мне НУЖЕН интерфейс с именем ICreatureWithArms или что-то подобное. Не так в Javascript - не так в C или ASM.

Очевидно, не имеет значения, имеет ли Javascript какое-либо представление о «типах».

Я не компьютерный ученый, но я был бы довольно удивлен, если бы «нетипизированный» действительно использовался как синоним «динамически типизированный» в сообществе CS (по крайней мере, в научных публикациях), поскольку, как мне кажется, эти два термина описывают разные концепции. В динамически типизированном языке есть понятие типов, и он обеспечивает соблюдение ограничений типа во время выполнения (вы не можете, например, разделить целое число на строку в Лиспе без получения ошибки), в то время как нетипизированный язык не имеет понятия типов в все (например, ассемблер). Даже статья в Википедии о языках программирования (http://en.m.wikipedia.org/wiki/Programming_language#Typed_versus_untyped_languages) делает это различие.

Обновление: возможно, путаница возникает из-за того, что в некоторых текстах говорится о том, что «переменные не типизированы» в Javascript (что верно). Но это не означает автоматически, что язык нетипизирован (что было бы неверно).

Согласитесь с Бренданом - контекст решает все.

Мое мнение:

Я помню, что примерно в 2004 году я был сбит с толку, потому что вспыхивали споры о том, является ли Ruby нетипизированным или динамически типизированным. Люди старой школы C / C ++ (в том числе и я) думали о компиляторе и говорили, что Ruby нетипизирован.

Помните, что в C нет типов времени выполнения, есть только адреса, и если выполняемый код решает рассматривать все, что находится по этому адресу, как то, чем оно не является, упс. Это определенно нетипизировано и сильно отличается от динамически типизированного.

В этом мире «типизация» - это все, что нужно для компилятора. В C ++ была «строгая типизация», потому что проверки компилятора были более строгими. Java и C были более «слабо типизированными» (были даже споры о том, является ли Java строго или слабо типизированным). В этом континууме динамические языки были «нетипизированными», потому что в них не было проверки типов компилятором.

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

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