Тип уточнения

В теории типов тип уточняющий ^[1]^[2]^[3] — это тип, наделенный предикатом, который предполагается справедливым для любого элемента уточненного типа. Уточняющие типы могут выражать предварительные условия при использовании в качестве аргументов функции или постусловия при использовании в качестве возвращаемых типов : например, тип функции, которая принимает натуральные числа и возвращает натуральные числа больше 5, может быть записан как $f:\mathbb {N} \rightarrow \{n\in \mathbb {N} \,|\,n>5\}$ . Типы уточнения, таким образом, связаны с поведенческими подтипами .

История [ править ]

Концепция типов уточнения была впервые представлена в книге Фримена и Пфеннинга « Типы уточнения для машинного обучения» в 1991 году . ^[1] который представляет систему типов для подмножества Standard ML . Система типов «сохраняет разрешимость вывода типа ML», но при этом «позволяет обнаруживать больше ошибок во время компиляции». В последнее время системы уточненных типов были разработаны для таких языков, как Haskell , ^[4]^[5] TypeScript , ^[6] Ржавчина ^[7] и Скала .

См. также [ править ]

Ссылки [ править ]

↑ Перейти обратно: Перейти обратно: ^а ^б Фриман, Т.; Пфеннинг, Ф. (1991). «Типы уточнений для ML» (PDF) . Материалы конференции ACM по проектированию и реализации языков программирования . стр. 268–277. дои : 10.1145/113445.113468 .
^ Хаяши, С. (1993). «Логика типов уточнения». Труды семинара по типам доказательств и программ . стр. 157–172. CiteSeerX 10.1.1.38.6346 . дои : 10.1007/3-540-58085-9_74 .
^ Денни, Э. (1998). «Виды уточнения для спецификации». Материалы Международной конференции ИФИП по концепциям и методам программирования . Том. 125. Чепмен и Холл. стр. 148–166. CiteSeerX 10.1.1.22.4988 .
^ Вазу, Ники. Liquid Haskell: типы уточнений Haskell . 45-й симпозиум ACM SIGPLAN по принципам языков программирования (POPL 2018).
^ Волков, Никита (2015). «Уточнение типов как библиотека Haskell» .
^ Панайотис, Векрис; Косман, Бенджамин; Джала, Ранджит (2016). «Типы уточнения для TypeScript». Материалы 37-й конференции ACM SIGPLAN по проектированию и реализации языков программирования . стр. 310–325. arXiv : 1604.02480 . дои : 10.1145/2908080.2908110 .
^ Леманн, Нико; Геллер, Адам Т.; Вазу, Ники; Джала, Ранджит (6 июня 2023 г.). «Флюсы: жидкости для борьбы с ржавчиной» . Труды ACM по языкам программирования . 7 (PLDI): 169:1533–169:1557. дои : 10.1145/3591283 .

\Gamma \!\vdash

Эта теории языков программирования или теории типов, статья, посвященная незавершена . Вы можете помочь Википедии, расширив ее .

[freeman-pfenning-1] Перейти обратно: Перейти обратно: ^а ^б Фриман, Т.; Пфеннинг, Ф. (1991). «Типы уточнений для ML» (PDF) . Материалы конференции ACM по проектированию и реализации языков программирования . стр. 268–277. дои : 10.1145/113445.113468 .

[2] Хаяши, С. (1993). «Логика типов уточнения». Труды семинара по типам доказательств и программ . стр. 157–172. CiteSeerX 10.1.1.38.6346 . дои : 10.1007/3-540-58085-9_74 .

[3] Денни, Э. (1998). «Виды уточнения для спецификации». Материалы Международной конференции ИФИП по концепциям и методам программирования . Том. 125. Чепмен и Холл. стр. 148–166. CiteSeerX 10.1.1.22.4988 .

[4] Вазу, Ники. Liquid Haskell: типы уточнений Haskell . 45-й симпозиум ACM SIGPLAN по принципам языков программирования (POPL 2018).

[5] Волков, Никита (2015). «Уточнение типов как библиотека Haskell» .

[6] Панайотис, Векрис; Косман, Бенджамин; Джала, Ранджит (2016). «Типы уточнения для TypeScript». Материалы 37-й конференции ACM SIGPLAN по проектированию и реализации языков программирования . стр. 310–325. arXiv : 1604.02480 . дои : 10.1145/2908080.2908110 .

[7] Леманн, Нико; Геллер, Адам Т.; Вазу, Ники; Джала, Ранджит (6 июня 2023 г.). «Флюсы: жидкости для борьбы с ржавчиной» . Труды ACM по языкам программирования . 7 (PLDI): 169:1533–169:1557. дои : 10.1145/3591283 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]