2023/2024
Теория типов
Статус:
Маго-лего
Когда читается:
1, 2 модуль
Охват аудитории:
для всех кампусов НИУ ВШЭ
Язык:
русский
Кредиты:
6
Контактные часы:
56
Программа дисциплины
Аннотация
Излагаются основные идеи теории типов. Отражены два основных способа типизации выражений. В соответствии с правилами тип приписывается только некоторым из выражений, но не всем. Рассматривается более слабая теория типов, чем сильные полиморфные теории, применяющиеся в логике и программировании. Эта система лежит в основе всех прочих систем типов, а ее свойства играют самостоятельную роль. Пользуясь ею, рассматривается два метода назначения типов объектам: от типов к объектам и от объектов к типам. Вместе с тем рассматривается теория функций, функции в категории, некоторая теория типов и конструкция функтор-как-объект, что восходит к переменным множествам Ф. Ловера. Это позволяет установить связь с аппликативными вычислениями и показать связи бестиповых моделей вычислений с типовыми моделями вычислений, а также строить естественную формализацию систем высших порядков. В качестве приложения рассматривается строение простой теории типов и структуры концептов и ассоциированные модели объектов данных/метаданных. Дополнительно рассматриваются семейства моделей с соотнесениями для Web.