Я хочу понять теорию типов, но сначала я должен знать, как ее применять. Могут ли быть более неочевидные применения теории типов помимо систем типов в программировании? Могут ли быть другие приложения, скажем, в профилировании личности и тому подобное?
type-theory
applied-theory
Тамад Ланг
источник
источник
Ответы:
Вы можете быть заинтересованы в работе над Ceptre , в результате исследования доктора философии из Криса Martens , который использует теорию типа для интерактивного повествования. Ниже приводится реферат диссертации :
источник
Там были интересные применения теории типов в лингвистике. См., Например, лингвистические труды Чунг-Цзе Шаня или Кристиана Реторе .
Цитируется ниже описание Rétoré в книге о категориальных грамматик:
Следующая цитата во введении главы книги « Языковые побочные эффекты» Шана :
источник
Из-за соответствия Карри-Говарда типы могут интерпретироваться как предложения, а предложения - как типы.
В результате этого теория типов применима буквально к любой области, которая использует формальную логику для своих доказательств. Это может быть проверка схемы, реальный анализ, символическая логика, геометрия и т. Д.
Например, некоторые инструменты автоматической проверки доказательств работают по этому принципу: они проверяют достоверность доказательства путем проверки типа определенного термина в некоторой системе типов. LF proof checker основан на этом подходе, как и HOL Light . В качестве примера приложения код для проверки корректности использовал LF для проверки доказательств безопасности ненадежного кода в памяти. Преимущество использования такого рода средства проверки правописания состоит в том, что реализация может быть очень простой, и, таким образом, мы можем получить высокую уверенность в том, что реализация является правильной. Смотри, например, следующую статью:
Основополагающие проверки с маленькими свидетелями . Динхао Ву, Эндрю В. Аппель, Аарон Стамп. PPDP 2003.
источник
Интересной статьей, которая объясняет приложения зависимых типов, является The Power of Pi , которая показывает, как Agda может использоваться для решения интересных задач.
Другим хорошим примером является использование зависимых типов для управления ресурсами. Хорошим примером является API управления файлами из Effects of Idris . Например, функция для чтения строки из файла имеет следующий тип
который указывает, что эта функция применима, только если открыт файл. Список в скобках указывает, какие эффекты доступны. В этом случае мы имеем, что для этой функции требуется открыть файл для чтения.
Более подробную информацию о библиотеке эффектов можно найти здесь .
Еще одно приложение - это использование зависимых типов для параллелизма, как описано в следующей статье создателя Idris.
источник
как упоминалось в ответе jmite, логика / теория более высокого порядка в верификации схем / аппаратных средств / электроники существовала уже несколько десятилетий и в настоящее время настолько рутинна, что ее даже не замечают / не рассматривают так часто, как «приложение» после явно большого усилия по переносу в ~ 1990-е годы, хотя это все еще активная область исследований. Coq и его типовая логика также широко применяются, в частности, для проверки схем / аппаратного обеспечения / электроники на всем пути от логики логического элемента низкого уровня до структур / подсистем гораздо более высокого уровня / порядка. вот несколько ключевых ссылок
Проверка логики и аппаратного обеспечения более высокого порядка / Melham (1993!)
Доказательство логической теоремы высшего порядка и ее приложения / Класон, Гордон
Построение правильных цепей: проверка функциональных аспектов спецификаций аппаратных средств с зависимыми типами / Брейди, Маккинна, Хаммонд
Сертификация цепей в теории типов / Grimal
Coquet: библиотека Coq для проверки оборудования / Braibant
источник