| Системы типов |
|---|
| Общие понятия |
| Основные категории |
| Второстепенные категории |
| Смотрите также |
В теории типа , A тип уточнения [1] [2] [3] представляет собой тип , наделенный предикат , который , как предполагается, для удержания любого элемента рафинированного типа. Типы уточнения могут выражать предварительные условия при использовании в качестве аргументов функции или постусловия при использовании в качестве возвращаемых типов : например, тип функции, которая принимает натуральные числа и возвращает натуральные числа больше 5, может быть записан как . Таким образом, типы уточнения связаны с поведенческими подтипами .
История [ править ]
Концепция типов уточнения была впервые введена в Фримен и 1991 Pfenning по типам утонченности для ML , [1] , которая представляет собой систему типа для подмножества Standard ML . Система типов «сохраняет разрешимость вывода типа ML», в то же время «позволяя обнаруживать больше ошибок во время компиляции». В последнее время системы уточняющих типов были разработаны для таких языков, как Haskell , [4] [5] TypeScript [6] и Scala .
См. Также [ править ]
Ссылки [ править ]
- ^ a b Freeman, T .; Пфеннинг, Ф. (1991). «Типы уточнения для ML» (PDF) . Труды конференции ACM по проектированию и реализации языков программирования . С. 268–277. DOI : 10.1145 / 113445.113468 .
- Перейти ↑ Hayashi, S. (1993). «Логика видов уточнения». Материалы семинара по типам для доказательств и программ . С. 157–172. CiteSeerX 10.1.1.38.6346 . DOI : 10.1007 / 3-540-58085-9_74 .
- ^ Денни, Э. (1998). «Виды уточнения по спецификации». Труды Международной конференции ИФИП по концепциям и методам программирования . 125 . Чепмен и Холл. С. 148–166. CiteSeerX 10.1.1.22.4988 .
- ^ Vazou, Niki. Liquid Haskell: типы уточнения для Haskell . 45-й симпозиум ACM SIGPLAN по принципам языков программирования (POPL 2018).
- ↑ Волков, Никита (2015). «Типы уточнения как библиотека Haskell» .
- ^ Панайотис, Vekris; Косман, Бенджамин; Джала, Ранджит (2016). «Типы уточнения для TypeScript». Труды 37-й конференции ACM SIGPLAN по проектированию и реализации языков программирования . С. 310–325. arXiv : 1604.02480 . DOI : 10.1145 / 2908080.2908110 .
| Эта статья по теории языков программирования или теории типов незавершена . Вы можете помочь Википедии, расширив ее . |
