Проект:Информационные технологии/Списки/Статьи по типизации

В информатике типизация — назначение различным информационным сущностям свойства, именуемого типом, идентифицирующего совокупность остальных его свойств, определяющих его место и роль в рамках заданной формальной системы. При всей простоте определения, термин имеет множество сложных контекстов использования:

• Типизация значения — см. Тип данных

— в том числе:

• Приведение типа
• Каламбур типизации
• Тип возвращаемого значения (не путать с Функциональный тип)

• Типизация языка — см. Система типов

— в том числе:

• Статическая типизация
• Динамическая типизация
• Сильная и слабая типизация
• Манифестная типизация (англ. Manifest typing) и Вывод типов
• Бестиповый язык

• Типизация программы — см. типобезопасность и полнотиповое программирование
• Нарушение типизации — см. Каламбур типизации
• Теоретическое обоснование типизации, типизация математической модели — см. Теория типов
• Типизация при полиморфизме или полиморфизм типов — см. Параметрический полиморфизм и Класс типов (англ. Type class)
• Типизация при наследовании в ООП — см. Выделение подтипов данных (англ. Subtyping) и Полиморфизм подтипов

Отдельные разновидности типов

• примитивные типы, в том числе:
  • логический тип
  • целые типы
  • вещественные типы
• ссылочные типы
• опциональные типы
  • обнуляемые типы
• Композитные типы, в том числе:
  • массивы
  • записи
  • кортежи
  • абстрактные типы (АТД, англ. ADT)
• алгебраические типы
  • вариантные типы
• подтипы
• унаследованные типы
• объектные типы, то есть объекты, значением которых являются типы — например, переменные типов
• частичные типы
• рекурсивные типы
• функциональные типы, например бинарные функции
• универсально квантифицированные типы, такие как параметрические типы
• экзистенциально квантифицированные, такие как модули
• зависимые типы — типы, зависящие от термов (значений)
• Тип, определяемый записью (row type)
• уточняющие типы — типы, идентфицирующие подмножества других типов
• Предопределённые типы (являющиеся фактически структурными, но предоставляемые на правах примитивных) для удобства промышленных разработок, такие как «дата», «время», «валюта» и др.

См.также

• Просто типизированное лямбда-исчисление
• Типизированное лямбда-исчисление
• Тип типов — см. Род (теория типов) и Метакласс
• Типизация таблицы в реляционных СУБД — см. Тип-произведение и Исчисление кортежей
• Типизация по Хиндли — Милнеру
• «Формулы-как-типы» (англ. formulae-as-types) — см. Изоморфизм Карри — Ховарда
• «Высказывания-как-типы» (англ. propositions-as-types) и «типы-как-высказывания» (англ. types-as-propositions) — см. Логика высказываний, Логика Хоара, Логика первого порядка, Интуиционистское исчисление высказываний и Аксиоматическая семантика (англ. Axiomatic semantics)