Обсуждение:Тип данных (KQvr';yuny&Mnh ;guud])

Структура статьи

Перенёс материал из ответвления типы данных, но структура данной статьи весьма странная по части примеров типов. Есть как минимум два варианта изложения темы типов данных, а также приведения наиболее выразительных примеров: исходя из популярных на практике или исходя из теоретических основ. По идее, одно другому даже не мешает, но если хочется следовать принципу от простого к сложному, то точки зрения теории и практики расходятся: скажем, указатель — довольно примитивен с точки зрения практики, но проблематичен с точки зрения теории. Тоже самое с полиморфными объектами. С другой стороны, то, что теория рассматривает как очень близкие типы (перечисления и вариантные типы), на практике весьма далеки. Может быть, со временем будет возможность изложить оба подхода? РоманСузи 14:04, 25 января 2015 (UTC)

• Я и сам давно думал как бы доработать. Есть два варианта - таблица из двух столбцов, где по вертикали перечислены "практические" типы и каждому сопоставлено его теоретическое обоснование (которые повторяются); и дерево, примерно как сейчас, где на верхнем уровне теория, а чем глубже, тем проблемнее. Ну есть ещё вариант разнести на два раздела, никак не пересекающихся (возможно, попытаться их слегка подружить уже после разработки). Лично я предпочёл бы второй. P.S. А откуда перенесли, я что-то не понял? Arachnelis 14:42, 25 января 2015 (UTC)

• Была статья (сюрприз!) Типы данных. В АИ нигде не видел попыток создать подобные таблицы (боюсь, снесут за орисс). Обычно каждый со своей колокольни начинает. Может, начать с низкоуровневых языков/типов (бит, байт, слово) к высокоуровневым и сверхвысокоуровневым с параллельным введением теоретико-типовых понятий? С этими первыми теория вообще нулевая, а дальше прогресс исторически шёл параллельно. А вообще говоря, в случае нескольких иерархий лучше всего плоская структура подразделов в разделе «Типы», а внутри — и конкретные типы, и их семейства (вроде АТД). И, конечно, нужно будет объединить просто иерархический список с описаниями (что я перенёс). РоманСузи 15:17, 25 января 2015 (UTC)

• А есть способ обнаруживать подобные "сироты" (если они не 100% сироты)? А то это уже второй пойманный беспризорник, мало ли сколько их ещё. Arachnelis 19:28, 25 января 2015 (UTC)
• Ну тогда просто последовательно рассказываем о каждом практическом, рассказывая вольном текстом о его месте в теории типов. Перечисление типов может служить а-ля содержанием статьи, внутренней навигацией. Клик - текст. upd: Ещё вариант (хотя и не верю, что его кто-то одобрит) сделать разделы сворачиваемыми. Тогда во-первых, эта часть статьи будет само себе содержанием, во-вторых, можно таки выстроить иерархию: раздел теоретического типа, у него дочерние практические со ссылкой на родителя. Arachnelis 19:16, 25 января 2015 (UTC)

запрос источника

В упор не пойму, зачем вывешен запрос АИ на фразу "Теория типов формально изучает типы и результаты от их назначения". Это по сути интервики. В целевой статье (а их получается ажно пучок) ссылки свои будут. С каких пор на утверждение о существовании теории, исследующей предмет, требуется источник? И что ожидается увидеть? Ссылку на работу начала XX века с цитатой вроде "к концу XX века типы будут аццки популярны, поэтому в данной работе предлагается набросок простейшей теории, чтобы на неё можно было сослаться с энциклопедии будущего"? Arachnelis 19:33, 13 февраля 2015 (UTC)

• "Теория типов формально изучает типы" — да, это банально, но вот "и результаты от их назначения" — какой-то бессмысленный набор слов. Ко второй части претензия. Евгений Мирошниченко 06:29, 14 февраля 2015 (UTC)

• Ну тогда надо отослать к Пирсу - у него вообще не проводится разграничения между "системами типов" и "теориями типов". Фишка в том, что типы являются едва ли не самой практичным и прикладным разделом математики - они не являются абстрактным обоснованием чего-то более прикладного, а используются непосредственно как есть. Даже существует эпатажное высказывание, что вся математика есть приложение теории типов. Arachnelis 18:32, 15 февраля 2015 (UTC)

  Я не знаю, кто такой Пирс. Кроме того, данный ваш текст никак не могу связать со своим. Я вам про красное, вы мне про солёное, типа того. Евгений Мирошниченко 03:16, 16 февраля 2015 (UTC)

• А вот определение "тип - это множество значений", пусть даже с АИ, очень узкое. Оно отбрасывает науку лет на 40 назад. Правильнее говорить (и несложно подтвердить), что тип - это атрибут, характеризующий ОДНОВРЕМЕННО множество значений и множество операций над ними. Весь параметрический полиморфизм опирается на "тип-как-поведение" (если вы, конечно, знаете о чём речь). А ещё предлагаю отметить, что многие авторы скользко обходят стороной определение и сразу переходят к классификации, анализу и пр. Как тенденция, это достойно внимания в энциклопедии. Пример - Cardelli, typeful systems. Arachnelis 18:37, 15 февраля 2015 (UTC)

  Ну, хотя дискуссии здесь оффтопик, не могу не прокомментировать.

  Во-первых, даже если предлагаемое определение не идеально, оно-таки дано по АИ. До него был написан какой-то орисс, непонятно откуда взятый.

  Во-вторых, определять тип данных как атрибут неправильно по двум причинам. Первая причина, понятие атрибут само по себе требует определения, и не факт, что эти определения будут одинаковы в математике, теории БД и программировании. Скажем, в теории реляционных БД «атрибут» сам по себе определяется в конечном итоге через тип данных, то есть получится рекурсия. Вторая причина, типичные высказывания «значение принадлежит типу данных», «значение относится к типу данных» никак нельзя прочитать как «значение принадлежит атрибуту», «значение относится к атрибуту».

  В-третьих, если включать в понятие «тип данных» операции, как это чаще всего делается, мы немедленно упираемся в кучу логически неразрешимых проблем. Например, получаем рекурсию определения. Определение операции как правило требует определения типа данных операндов и типа данных результата. Для многих операций эти ограничения очень важны. Например, при определении некоторой алгебры мы обязаны обеспечить замкнутость: операции определены на значениях типа T и результатом имеют значения того же типа T. Есть и вторая проблема: как только мы определяем новую операцию с типом данных, мы формально порождаем совершенно другой тип. Это прямо следует из включения операций в понятие типа данных. И если это новый тип, у него должно быть новое обозначение и название. Но по факту никто так не делает. Ни в теории БД, ни в математике, ни в программировании. Получается, что по факту тип данных первичен и самодостаточен, поскольку может быть определён и без операций, а вот операции с типом (или над типом) данных — вторичны, поскольку без типа данных не могут быть определены. Даже когда в случае генерализации (шаблонов) в ООП мы определяем операцию над неизвестными типами <T1>, <T2> и т. д., обратите внимание, что даже такие типы для определения операции первичны: невозможно задать операцию, не задавая сначала типы.

  Поэтому, с моей точки зрения, определять тип данных через операции — не достижение науки, а бесполезная вещь, которая на практике как раз и не используется. Евгений Мирошниченко 03:16, 16 февраля 2015 (UTC)

  Возражаю. Только очень простые типы можно определить как множество значений. Есть ещё индуктивно определяемые типы, рекурсивные типы и так далее. И операции даются уже в определении типов. Скажем, в определении абстрактных типов данных, иначе как в определении и не получится, так как в дальнейшем тип используется как черный ящик. В общем случае при определении как раз останавливаться на теории множеств нельзя, используют более тонкие теории, вроде Гомотопическая теория типов. Конечно, с точки зрения теории типов что попало непрактично брать в качестве системы типов конкретного языка, но сегодня именно такие соображения используются при работе с типами, какие я описал в преамбуле. И операции входят в определение типа, хотя бы чисто синтаксически, причем в разных ипостасях: как операции над типами, над типопеременными, а также и над значениями величин, принадлежащим типам. И за примером идти дальше типизированного лямбда-исчисления не нужно. Опять-таки, да результатом в большинстве случаев, конечно, в условиях конечной вычислительной машины в рантайме будет множество значений, но на этапе проверки типов, а её мы не можем выкинуть из определения, так как ради таких проверок вся возня с типами и происходит, и в теории типов касаются и упомянутых аспектов, именно в отношении типа. РоманСузи 04:34, 16 февраля 2015 (UTC)

• Роман, возражая, неплохо бы бы приводить контраргументы. Я привёл аргументы, а вы контраргументы на них не привели, ни одного. Кроме того, я не сторонник винегрета в данном случае из математики, ООП и теории БД, где подходы к определению и использованию понятия «тип данных» не идентичны, а у вас всё вместе. Давайте чётко указывать контекст. Классический пример, показывающий несовместимость математики и ООП таков: «объект» в ООП это и не значение, и не переменная, а «класс» — это не тип данных (а вообще непонятно что). Евгений Мирошниченко 06:22, 16 февраля 2015 (UTC)
• P.S. Не укажете, почему это наличие гомотопической теории типов приводит вас к следствию, что «останавливаться на теории множеств нельзя»? Все существующие определения типа данных, даже те, которые включают в тип операции, ссылаются на множество значений. Гомотопическая теория типов — интересная игра мысли, но не более, как и, к примеру, модальные логики. Ну есть они, и давно есть, и куча учёных вокруг крутится и пишет всякое. И что? На практике-то всё равно никому это пока нафиг не надо. Евгений Мирошниченко 06:35, 16 февраля 2015 (UTC)
• P.P.S. Да, забыл прокомментировать про якобы «только очень простые типы можно определить как множество значений» и прочее. Вы, мне кажется, не учитываете, что множество тоже может задаваться не только перечислением, но и описательно, в том числе индуктивно и рекурсивно. Поэтому данные рассуждения мне у вас не очень понятны. Евгений Мирошниченко 06:46, 16 февраля 2015 (UTC)

• Тут пока что не в аргументах дело. Аргументом будет являться соответствующий АИ. Я просто хотел сказать, что сводить тип к множеству значений — это только первое приближение, которое, может конечно, быть и в учебниках, и на практике вероятно удобно, но для теории неверно. Полагаю, что коллега Arachnelis что-то найдёт. С описательным же перечислением множества как раз есть трудности, иначе в математике не стали бы заниматься теорией категорий и тому подобным, где в качестве примитива вместо множества взяты отношения. Наверное, действительно, требуется некий компромисс между практическим определением типа и теоретическими разработками. Что касается аргументов, то я вижу, что Ваши рассуждения о трудности описания типа вместе с операциями дают только один аргумент: «но по факту никто так не делает.» Тем не менее, это вовсе не перечёркивает теоретического понимания типа, а только даёт повод дополнить статью более приближенным понимания типа (разумеется, избегая "винегрета"). Я вижу данный спор именно в этой плоскости. Считаю, что для статьи Тип данных необходимо дать и теоретическое введение. Хотя бы намёк на то, что всё не так просто. Несовместимости ООП и математики нет. Все эти объекты и классы и даже классы как объекты на самом деле ещё в 1990-х были активно обоснованы в трудах теоретиков (а там как раз математика). Что касается связи типа с логиками, то тут Вам Соответствие Карри — Ховарда в руку. «Гомотопическая теория типов — интересная игра мысли» — к счастью или сожалению, вся математика такая. Что, правда, не мешает ей отлично обслуживать инженерные науки. РоманСузи 07:15, 16 февраля 2015 (UTC)

• РоманСузи, да, я неплохо разобрался с литературой, но сейчас очень занят, не знаю когда смогу всерьёз заняться данной статьёй. Текущий вариант был наброском за неимением лучшего. Arachnelis 19:04, 16 февраля 2015 (UTC)

• Евгений Мирошниченко, сразу ясно, что с такими понятиями как параметрический полиморфизм (он же «полиморфизм типов»), Система F, конструктор типов, type variable, type kind, type class, функциональный тип (не путать с типом возвращаемого значения функции) вы не знакомы даже приблизительно. Ссылки можете считать за аргументы. Эти понятия - абстракции более высокого порядка, чем то примитивное понятие о типе, в отношении которого в принципе можно говорить о значении. У полиморфного типа значений быть не может. Значение может характеризоваться только мономорфным типом. А вот функция может иметь аргументы и результат полиморфного типа (и сама быть значением). Разумеется, авторы, пишущие о данных (в том числе о базах данных), другого понимания типа не видят. Для них полиморфизм типов — это как радуга для дальтоника. Однако, полиморфная типизация — это не аморфная теория, а прикладная вещь, которой присущ кратный прирост показателей качества программирования (производительности труда программистов, верифицируемости программ, коэффициента повторного использования кода и т. д.). Что же касается определения понятия «класс», то вы заблуждаетесь. Уже построена обобщённая теория ОО, выявляющая недоработки многих ОО-языков, читать работы Луки Карделли, но сперва полиморфизм подтипов. Arachnelis 18:58, 16 февраля 2015 (UTC)

• Сделать шаг в новую вселенную, на которую я тут указал, поможет следующая брошюрка: "Харпер - Введение в Стандартный ML (рус)". Материал краткий и доступный, но достаточно ёмкий для уверенного понимания первой ступени. Arachnelis 20:39, 25 февраля 2015 (UTC)

• @Евгений Мирошниченко: А вы сразу на предлоги и знаки препинания запросы АИ вешайте, чего уж мелочиться. Arachnelis 20:33, 25 февраля 2015 (UTC)

определение

• Это понятно. Но мы говорим о типе данных. Зачем здесь вообще о теории типов говорить: достаточно как-то связать тип данных с теорией типов, объектом изучения он является. У теории типов есть своя статья. Кстати, в англовики более развёрнутая преамбула. У нас тоже можно было бы добавить об операциях, благо, что ниже это раскрывается. РоманСузи 18:58, 15 февраля 2015 (UTC) Собственно, немного переписал преамбулу по англовики. Посмотрите, если так лучше. РоманСузи 19:06, 15 февраля 2015 (UTC)
• Мда, война пошла не на жизнь, а на смерть... Хорошо, хоть активность на проекте появилась. :) Arachnelis 18:46, 18 февраля 2015 (UTC)

• На безрыбье и определения из стандартов сойдут. Смущает только, что определения настолько разношёрстные, что с развитием статьи нужно будет их привести к общему знаменателю. Кстати, Пирс не приводит определения типа, а только системы типов (хотя из того, что он пишет понятно, что тема непростая). Карделли же говорит (в Type systems) о «Type — a collection of values». Но точно не множество. РоманСузи 19:09, 18 февраля 2015 (UTC)

• Здесь очень важно отметить, что Карделли под "values" понимает в том числе и первоклассные функции, а это другая вселенная. В typeful programming он тоже уходит от вопроса "что такое тип". Arachnelis 20:33, 25 февраля 2015 (UTC)
• Поясню:

datatype number =
   Number of {
               !+! : number -> number -> number,
               !-! : number -> number -> number,
               !/! : number -> number -> number,
               !*! : number -> number -> number
             }
infix 6 !+! !-!
infix 7 !/! !*!

• (Я тут не стремился к полноценной реализации, просто набросок для демонстрации.) Да, тип number представляет собой коллекцию значений, но только значений не в том смысле, в каком это привык понимать Евгений Мирошниченко, а в смысле «экземпляров классов» (так что класс в ООП — это таки тип). Тип int является значением типа number. То есть, чтобы получить всё множество целочисленных значений, можно описать лишь их поведение, создав одно значение типа number (заметим, что этот тип рекурсивен). Примерно так делает Brainfuck, а подробнее эта методика описана в SICP. Таким образом, данный тип, с одной стороны, представляет собой коллекцию значений, а с другой — описывает поведение (так как этими значениями являются коллекции функций). Такие типы язык поддерживает только в том случае, если он одновременно поддерживает функциональные значения, что немедленно вводит понятие «функциональный тип». Вы тут посовещайтесь насчёт сделать именно такое введение в статью. И есть на что сослаться (кроме Карделли ещё предложу Паулсона, с.176, да хоть вообще вся пятая глава), и сразу показывает узость некоторых языков, что естественным образом даёт понять причину дальнейших самотёрок в статье. Arachnelis 21:40, 25 февраля 2015 (UTC)

• Между прочим, в свете сказанного есть смысл переименовать статью в Тип (информатика). Arachnelis 15:51, 10 марта 2015 (UTC)

• В общем, конечно, да. Надо только посмотреть, нет ли «более простого" («наивного») понимания типа, чем в теоретической информатике. Ведь там же до безобразия может доходить, когда экземпляр типа — это доказательство верности программы, а из него решатель автоматически получает программу (наличие экзепляра типа в этом контексте равносильно наличию доказательства). Причём тип задаёт поведение программы так, что неверно выполниться она не может. Вот (пример из книги Адама Чипала) на Coq:

 Program Definition pred_strong6 (n : nat) (_ : n > 0) : {m : nat | n = S m} :=
   match n with
     | O => _
     | S n' => n'
   end.

• даёт при extraction программу на OCaml (типы отброшены, так как компилятор и так их вычислит):

 let pred_strong6 = function
   | O -> assert false (* absurd case *)
   | S n' -> n'

• И как в одной статье описывать этот высший пилотаж вместе с более приземлённым, практическим пониманием? РоманСузи 17:20, 10 марта 2015 (UTC)

• Не, ну в матан лезть незачем, просто понятие обобщить. Arachnelis 16:05, 12 марта 2015 (UTC)

• Вы предлагаете начать с частного и обобщить или дать общее определение, а потом упрощённое? РоманСузи 16:29, 12 марта 2015 (UTC)

• Надо сначала написать красиво, а потом переименовать уже. Лучше, конечно же, начать с простого и доступного, а потом разложить. Пока, начерно, видится такая схема: сперва определение Карделли (оно достаточно интуитивно, и у большинства читателей не вызовет нареканий - максимум удивление, что не "множество"), затем что "это означает одновременно два свойства" - это всё в голове. А уже после содержания раздел "Определение", и там понеслось. Ну вот мой вариант такой. Arachnelis 18:45, 13 марта 2015 (UTC)
• Смотрите, что нашёл: «Polymorphic types are types whose operations are applicable to values of more than one type» (Карделли, "On Understanding Types", готовая карточка на статью есть в статье "полиморфизм"). Всё давно систематизировано, а мы тут всё велосипеды изобретаем. Arachnelis 20:07, 19 марта 2015 (UTC)

• Кстати, Википедия:Правила и указания#Последовательность изложения: рекомендуется от общего к частному, от простого к сложному. А велосипедов мы не изобретаем. Мы неспеша думаем над тем, в каком порядке желательно изложить тему, чтобы большинство читателей смогли получить максимум, исходя из того, что даже о сложном предмете можно написать просто без потери для смысла. Типотеоретические работы без подготовки не понять как следует, так как на практике складываются несколько иные понятия (достаточные для «выживания», если, конечно, не сажаешь аппарат на Марс). Между тем, именно раскрытие теоретической сущности понятий придаёт глубину и существенно увеличивает квалификацию. Поэтому мне нравится изложенное Вами выше (18:45, 13 марта 2015). К Карделли нужно бы работы поновее (основы, конечно, не изменились, но воды много утекло). Вот тут некий ответ: [1], еще обзор в главе 2: [2]. РоманСузи 08:47, 21 марта 2015 (UTC)

Плавающая запятая

Насколько я понимаю, за пределами информатики целые и дробные числа обрабатываются одной и той же алгеброй, а значит по определению «Тип данных — множество значений и операций на этих значениях» — одним и тем же «множеством операций». Значит, целые и дробные числа это один тип данных. Разумеется в информатике это разделение важно, но это связано с современной архитектурой процессоров, а не с принципиальным различием типов данных. Я бы сделал числа с плавающей запятой подтипом целых чисел, или сделать общий тип «Числа» и у его два подтипа. В информатике так не делают, чтобы приучить программистов не путать целые и дробные числа, но повторюсь, это издержки современной архитектуры, а не различие набора операций над числами.— Михаил Ягих (обс.) 07:52, 18 августа 2019 (UTC)

"Насколько я понимаю": вы неправильно понимаете. Соответственно, всё остальное после этих слов не имеет смысла. Евгений Мирошниченко 10:35, 18 августа 2019 (UTC)

А ничего, что в английской версии типы данных сгруппированы в классы? В том числе и те, что я упомянул.— Михаил Ягих (обс.) 18:19, 18 августа 2019 (UTC)

Вернёмся к началу. За пределами информатики, а именно, в математике, целые и дробные числа обрабатываются разными алгебрами. Например, целочисленное деление — совершенно не то же, что деление дробных чисел. Следовательно, все ваши рассуждения ложные. Каким образом то, что «в в английской версии типы данных сгруппированы в классы» это меняет, я не вижу. Евгений Мирошниченко 14:53, 19 августа 2019 (UTC)

Дайте мне, пожалуйста, точное название разных алгебр для целых и дробных чисел.— Михаил Ягих (обс.) 15:44, 19 августа 2019 (UTC)

Извините, что такое «дробное число»? В статье об этом ничего нет. И даже в Википедии нет статьи на эту тему (не считая дробное числительное) РоманСузи (обс.) 17:51, 19 августа 2019 (UTC)

Роман, я думаю, что коллега Михаил Ягих таким образом называет рациональные числа. Так вот, алгебры называются: алгебра над полем целых чисел (или алгеброй над кольцом целых чисел), алгебра над полем рациональных чисел и т.д. В целочисленной алгебре, в отличие от алгебры над полем рациональных чисел, операция деления, вообще говоря, строго не определена, так как деление большинства целый чисел не даёт целое число. Поэтому используются приближения, а именно деление с остатком и деление нацело. В первом случае деление 9 на 2 даёт 4 и 1 в остатке, во втором случае — просто 4. А вот в алгебре над полем рациональных чисел деление 9 на 2 даёт прекрасное число ${\frac {9}{2}}$. Евгений Мирошниченко 04:02, 20 августа 2019 (UTC)

Плюс все это «накладывается» на конечность машинного представления. В любом случае здесь как раз самое место стандартам-источникам. Тем более, что классификация по нижележащей алгебре может быть не самым популярным видом классификации типов данных. РоманСузи (обс.) 14:50, 22 августа 2019 (UTC)

Структурированный тип данных

Есть ли определение такому понятию. Совпадает ли данный термин с термином «составной тип данных» или нет?

Структурный и структурированный типы

Структурный и структурированный типы это синонимы или разные понятия?