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

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

История

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

Смотрите также

• Жидкий Хаскелл
• Зависимые типы

Ссылки

1. Freeman, T.; Pfenning, F. (1991). "Типы уточнения для ML" (PDF) . Труды конференции ACM по проектированию и реализации языков программирования . стр. 268–277. doi :10.1145/113445.113468.
2. Хаяши, С. (1993). «Логика типов уточнения». Труды семинара по типам для доказательств и программ . С. 157–172. CiteSeerX 10.1.1.38.6346 . doi :10.1007/3-540-58085-9_74. 
3. Денни, Э. (1998). «Типы уточнения для спецификации». Труды Международной конференции IFIP по концепциям и методам программирования . Том 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 . doi :10.1145/2908080.2908110.
7. Леманн, Нико; Геллер, Адам Т.; Вазу, Ники; Джала, Ранджит (6 июня 2023 г.). «Flux: жидкие типы для Rust». Труды ACM по языкам программирования . 7 (PLDI): 169:1533–169:1557. doi : 10.1145/3591283 .