Обобщенный алгебраический тип данных
В функциональном программировании — обобщенный алгебраический тип данных ( GADT , также первоклассный фантомный тип , [1] защищенный рекурсивный тип данных , [2] или тип с указанием равенства [3] ) является обобщением параметрических алгебраических типов данных .
Обзор [ править ]
В GADT конструкторы продуктов (называемые конструкторами данных в Haskell ) могут обеспечить явное создание экземпляра ADT в качестве экземпляра типа возвращаемого значения. Это позволяет определять функции с более продвинутым типом поведения. Для конструктора данных Haskell 2010 возвращаемое значение имеет экземпляр типа, подразумеваемый созданием экземпляра параметров ADT в приложении конструктора.
-- Параметрический ADT, не являющийся
списком данных GADT. List a = Nil | Cons a ( List a )
целые числа :: List Int
целые числа = Cons 12 ( Cons 107 Nil )
строки :: List String
strings = Cons «boat» ( Cons «dock» Nil )
GADT
— данные Expr a, где
EBool :: Bool -> Expr Bool
EInt :: Int -> Expr Int
EEqual :: Expr Int -> Expr Int -> Expr Bool
eval :: Expr a -> a
eval e = случай e из
EBool a -> a
EInt a -> a
EEqual a b -> ( eval a ) == ( eval b )
expr1 :: Expr Bool
expr1 = EEqual ( EInt 2 ) ( EInt 3 )
ret = eval expr1 -- False
В настоящее время они реализованы в компиляторе GHC как нестандартное расширение, используемое, в частности, Pugs и Darcs . OCaml изначально поддерживает GADT, начиная с версии 4.00. [4]
Реализация GHC обеспечивает поддержку параметров экзистенциального количественного типа и локальных ограничений.
История [ править ]
Ранняя версия обобщенных алгебраических типов данных была описана Augustsson & Petersson (1994) и основана на сопоставлении с образцом в ALF .
Обобщенные алгебраические типы данных были независимо представлены Чейни и Хинце (2003) , а ранее Си, Ченом и Ченом (2003) как расширения ML и Haskell алгебраических типов данных . [5] Оба по сути эквивалентны друг другу. Они подобны индуктивным семействам типов данных (или индуктивным типам данных ), найденным в Кока « Исчислении индуктивных конструкций» и других зависимо типизированных языках , по модулю зависимых типов и за исключением того, что последние имеют дополнительное ограничение положительности , которое не применяется в GADT. . [6]
Сульцманн, Вазни и Стаки (2006) представили расширенные алгебраические типы данных , которые объединяют GADT вместе с экзистенциальными типами данных и ограничениями классов типов .
Вывод типа в отсутствие каких-либо аннотаций типа , предоставленных программистом, неразрешим . [7] не допускают основных типов . и функции, определенные в GADT, вообще [8] Реконструкция типа требует нескольких конструктивных компромиссов и является областью активных исследований ( Пейтон Джонс, Уошберн и Вейрих, 2004 ; Пейтон Джонс и др., 2006) .
Весной 2021 года выйдет Scala 3.0. [9] В этом крупном обновлении Scala появилась возможность писать GADT. [10] с тем же синтаксисом, что и ADT , чего нет в других языках программирования, по мнению Мартина Одерски . [11]
Приложения [ править ]
Приложения GADT включают общее программирование , моделирование языков программирования ( абстрактный синтаксис высшего порядка ), поддержание инвариантов в структурах данных , выражение ограничений во встроенных предметно-ориентированных языках и моделирование объектов. [12]
Абстрактный синтаксис высшего порядка [ править ]
Важным применением GADT является встраивание абстрактного синтаксиса высшего порядка способом безопасным для типов . Вот встраивание просто типизированного лямбда-исчисления с произвольным набором базовых типов , кортежами и комбинатором с фиксированной точкой :
data Lam :: * -> * где
Lift :: a -> Lam a -- ^ поднятое значение
Pair :: Lam a -> Lam b -> Lam ( a , b ) -- ^ произведение
Lam :: ( Lam a - > Lam b ) -> Lam ( a -> b ) -- ^ лямбда-абстракция
App :: Lam ( a -> b ) -> Lam a -> Lam b -- ^ применение функции
Fix :: Lam ( a -> a ) -> Lam a -- ^ фиксированная точка
И типобезопасная функция оценки:
eval :: Lam t -> t
eval ( Lift v ) = v
eval ( Pair l r ) = ( eval l , eval r )
eval ( Lam f ) = \ x -> eval ( f ( Lift x ))
eval ( App ж x ) = ( eval f ) ( eval x )
eval ( Fix f ) = ( eval f ) ( eval ( Fix f ))
Теперь функцию факториала можно записать так:
факт = Fix ( Lam ( \ f -> Lam ( \ y -> Lift ( если eval y == 0 , то 1 else eval y * ( eval f ) ( eval y - 1 )))))
eval ( факт )( 10 )
Мы бы столкнулись с проблемами при использовании обычных алгебраических типов данных. Удаление параметра типа сделало бы поднятые базовые типы экзистенциально квантифицированными, что сделало бы невозможным написание оценщика. С параметром типа мы все равно будем ограничены одним базовым типом. Кроме того, неправильно сформированные выражения, такие как App (Lam (\x -> Lam (\y -> App x y))) (Lift True)можно было бы построить, хотя они имеют неправильный тип с использованием GADT. Правильно сформированный аналог App (Lam (\x -> Lam (\y -> App x y))) (Lift (\z -> True)). Это связано с тем, что тип x является Lam (a -> b), выведенный из типа Lam конструктор данных.
См. также [ править ]
Примечания [ править ]
- ^ Чейни и Хинце 2003 .
- ^ Си, Чен и Чен 2003 .
- ^ Шеард и Пашалич 2004 .
- ^ «ОКамл 4.00.1» . ocaml.org .
- ^ Чейни и Хинце 2003 , с. 25.
- ^ Чейни и Хинце 2003 , стр. 25–26.
- ^ Пейтон Джонс, Washburn & Weirich 2004 , стр. 7.
- ^ Шрийверс и др. 2009 , с. 1.
- ^ Кметюк, Анатолий. «SCALA 3 ЗДЕСЬ!🎉🎉🎉» . scala-lang.org . Федеральная политехническая школа Лозанны (EPFL), Лозанна, Швейцария . Проверено 19 мая 2021 г.
- ^ «SCALA 3 — КНИГА АЛГЕБРАИЧЕСКИХ ТИПОВ ДАННЫХ» . scala-lang.org . Федеральная политехническая школа Лозанны (EPFL), Лозанна, Швейцария . Проверено 19 мая 2021 г.
- ^ Одерский, Мартин. «Экскурсия по Scala 3 — Мартин Одерски» . youtube.com . Конференции Scala Days. Архивировано из оригинала 19 декабря 2021 г. Проверено 19 мая 2021 г.
- ^ Пейтон Джонс, Washburn & Weirich 2004 , стр. 3.
Дальнейшее чтение [ править ]
- Приложения
- Аугустссон, Леннарт ; Петерссон, Кент (сентябрь 1994 г.). «Семьи глупых типов» (PDF) .
- Чейни, Джеймс ; Хинце, Ральф (2003). «Первоклассные фантомные типы». Технический отчет CUCIS TR2003-1901 . Cornell University. hdl : 1813/5614 .
- Си, Хунвэй ; Чен, Чиян ; Чен, Банда (2003). «Защищенные рекурсивные конструкторы типов данных». Материалы 30-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования . АКМ Пресс. стр. 224–235. CiteSeerX 10.1.1.59.4622 . дои : 10.1145/604131.604150 . ISBN 978-1581136289 . S2CID 15095297 .
- Шеард, Тим ; Пашалич, Эмир (2004). «Метапрограммирование со встроенным равенством типов» . Материалы четвертого международного семинара по логическим структурам и метаязыкам (LFM'04), Корк . 199 : 49–65. дои : 10.1016/j.entcs.2007.11.012 .
- Семантика
- Патрисия Йоханн и Нил Гани (2008). « Основы структурного программирования с GADT ».
- Арье Мидделькооп, Аце Дейкстра и С. Доайтсе Свирстра (2011). « Упрощенная спецификация для GADT: система F с первоклассными доказательствами равенства ». Вычисления высшего порядка и символьные вычисления .
- Тип реконструкции
- Пейтон Джонс, Саймон ; Уошберн, Джеффри ; Вейрих, Стефани (2004). «Шаткие типы: вывод типов для обобщенных алгебраических типов данных» (PDF) . Технический отчет MS-CIS-05-25 . Пенсильванский университет.
- Пейтон Джонс, Саймон ; Витиниотис, Димитриос ; Вейрих, Стефани ; Уошберн, Джеффри (2006). «Простой вывод типов на основе унификации для GADT» (PDF) . Материалы Международной конференции ACM по функциональному программированию (ICFP'06), Портленд .
- Зульцманн, Мартин ; Уазни, Джереми ; Стаки, Питер Дж. (2006). «Структура расширенных алгебраических типов данных». В Хагии, М.; Уодлер, П. (ред.). 8-й Международный симпозиум по функциональному и логическому программированию (FLOPS 2006) . Конспекты лекций по информатике . Том. 3945. стр. 46–64.
- Зульцманн, Мартин ; Шрийверс, Том ; Стаки, Питер Дж. (2006). «Вывод основного типа для многопараметрических классов типов в стиле GHC». В Кобаяши, Наоки (ред.). Языки и системы программирования: 4-й Азиатский симпозиум (APLAS 2006) . Конспекты лекций по информатике. Том. 4279. стр. 26–43.
- Шрийверс, Том ; Пейтон Джонс, Саймон ; Зульцманн, Мартин ; Витиниотис, Димитриос (2009). «Полный и разрешимый вывод типа для GADT» (PDF) . Материалы 14-й международной конференции ACM SIGPLAN по функциональному программированию . стр. 341–352. дои : 10.1145/1596550.1596599 . ISBN 9781605583327 . S2CID 11272015 .
- Линь, Чуан-кай (2010). Практический вывод типов для системы типов GADT (PDF) (докторская диссертация). Портлендский государственный университет. Архивировано из оригинала (PDF) 11 июня 2016 г. Проверено 8 августа 2011 г.
- Другой
- Эндрю Кеннеди и Клаудио В. Руссо. « Обобщенные алгебраические типы данных и объектно-ориентированное программирование ». В материалах 20-й ежегодной конференции ACM SIGPLAN по объектно-ориентированному программированию, системам, языкам и приложениям . АКМ Пресс, 2005.
Внешние ссылки [ править ]
- Страница обобщенных алгебраических типов данных Haskell в вики
- Обобщенные алгебраические типы данных в Руководстве пользователя GHC
- Обобщенные алгебраические типы данных и объектно-ориентированное программирование
- GADT — Haskell Prime — Trac
- Статьи о выводе типов для GADT , библиография Саймона Пейтона Джонса
- Вывод типа с ограничениями , библиография Саймона Пейтона Джонса
- Эмуляция GADT в Java с помощью леммы Йонеды