Зависимый тип

Зависимый тип
Типизация данных

Типобезопасность
Вывод типов
Динамическая типизация
Статическая типизация
Строгая типизация
Мягкая типизация
Зависимые типы
Утиная типизация

Зависимый тип, в информатике и логике — тип, который зависит от значения. Зависимые типы играют ключевую роль в интуиционистской теории типов и построении функциональных языков программирования таких как ATS, Agda и Epigram.

К примеру тип описывающий n-кортежей действительных чисел будет является зависимым, потому что он «зависит»' от величины n.

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

Изоморфизм Карри — Ховарда означает, что типы могут быть построены таким образом, что могут выражать сколь угодно сложные математические свойства. Если пользователь предоставит конструктивное доказательство того, что тип «заселён» (то есть значение этого типа существует), то компилятор сможет проверить это доказательство, и превратить его в исполняемый код, который вычисляет значение. Наличие проверки доказательств делает зависимо-типизированные языки схожими с программным обеспечением, предназначенным для помощи в доказательствах (на пример интерактивный доказатель теорем Coq).

Системы лямбда-куба

Хенк Барендрегт разработал лямбда-куб в качестве средства классификации систем типов по трем осям. Каждый из восьми углов кубической диаграммы соответствует системе типов. В наиболее бедной вершине куба находится просто типизированное лямбда исчисление, а в наиболее богатой — исчисление конструкций. Трем осям куба соответствуют три различных дополнения к просто типизированному лямбда-исчислению: дополнение зависимых типов, дополнение полиморфизма и дополнение конструкторов типов высшего порядка.



Wikimedia Foundation. 2010.

Игры ⚽ Нужна курсовая?

Полезное


Смотреть что такое "Зависимый тип" в других словарях:

  • зависимый спрос — Тип спроса, который зависит от намерений организации производить другие изделия. Характерен прежде всего для рынка компонентов, используемых в составе более сложных изделий. [http://tourlib.net/books men/meskon glossary.htm] зависимый спрос В… …   Справочник технического переводчика

  • Зависимый спрос — тип спроса, который зависит от намерений организации производить другие изделия. Характерен прежде всего для рынка компонентов, используемых в составе более сложных изделий …   Словарь терминов антикризисного управления

  • Незрелая личность (immature personality) — Н. л. это родовой термин, охватывающий ряд связанных, но различимых между собой черт личности. Главное его значение связано с понятием психол. зрелости. Психол. созревание можно охарактеризовать как достижение стадии интеллектуального и… …   Психологическая энциклопедия

  • Парадигма — (Paradigm) Определение парадигмы, история возникновения парадигмы Информация об определении парадигмы, история возникновения парадигмы Содержание Содержание История возникновения Частные случаи (лингвистика) Управленческая парадигма Парадигма… …   Энциклопедия инвестора

  • Coq — (фр. coq  петух)  интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования (Gallina) с зависимыми типами. Позволяет записывать математические теоремы и их… …   Википедия

  • Функциональное программирование — Парадигмы программирования Агентно ориентированная Компонентно ориентированная Конкатенативная Декларативная (контрастирует с Императивной) Ограничениями Функциональная Потоком данных Таблично ориентированная (электронные таблицы) Реактивная …   Википедия

  • Иоанн (Береславский) — Эта статья должна быть полностью переписана. На странице обсуждения могут быть пояснения …   Википедия

  • Акромеланизм — (Acromelanism) генетически обусловленный температурно зависимый тип пигментации с полным проявлением только на конечностях, ушах, хвосте и морде и при более светло окрашенной шерсти на корпусе. Встречается у сиамских и гималайских кошек, кроликов …   Википедия

  • атрибутивные (определительные) отношения — Тип синтаксических отношений в словосочетании, при которых господствующий член имеет значение предмета, зависимый член – значение признака. Этому содержанию соответствует вопрос какой?: молодой отец, наш коттедж, прилетевший голубь, лодка с… …   Словарь лингвистических терминов Т.В. Жеребило

  • обстоятельственные отношения — Тип синтаксических отношений в словосочетании, при которых господствующий член имеет значение действия или признака, зависимый член – значение его признака, его характеристики. Это содержание соответствует вопросам к наречиям и к обстоятельствам… …   Словарь лингвистических терминов Т.В. Жеребило


Поделиться ссылкой на выделенное

Прямая ссылка:
Нажмите правой клавишей мыши и выберите «Копировать ссылку»