В функциональном программировании обобщенный алгебраический тип данных ( GADT , также фантомный тип первого класса , [1] защищенный рекурсивный тип данных [ 2] или тип, квалифицированный равенством [3] ) является обобщением параметрического алгебраического типа данных (ADT).
В GADT конструкторы продуктов (называемые конструкторами данных в Haskell ) могут предоставлять явное инстанцирование ADT как инстанцирование типа их возвращаемого значения. Это позволяет определять функции с более продвинутым поведением типа. Для конструктора данных Haskell 2010 возвращаемое значение имеет инстанцирование типа, подразумеваемое инстанцированием параметров ADT в приложении конструктора.
-- Параметрический ADT, который не является данными GADT Список a = Ноль | Минусы a ( Список a ) целые числа :: Список целых чисел = Cons 12 ( Cons 107 Nil ) strings :: Список строк 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 = case e of 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 -- Ложь В настоящее время они реализованы в Glasgow Haskell Compiler (GHC) как нестандартное расширение, используемое, среди прочего, Pugs и Darcs . OCaml поддерживает GADT изначально, начиная с версии 4.00. [4]
Реализация GHC обеспечивает поддержку экзистенциально квантифицированных параметров типа и локальных ограничений.
Ранняя версия обобщенных алгебраических типов данных была описана Аугустссоном и Петерссоном (1994) и основывалась на сопоставлении шаблонов в ALF .
Обобщенные алгебраические типы данных были введены независимо Чейни и Хинце (2003) и ранее Си, Ченом и Ченом (2003) как расширения алгебраических типов данных ML и Haskell . [5] Оба по сути эквивалентны друг другу. Они похожи на индуктивные семейства типов данных (или индуктивные типы данных ) , найденные в исчислении индуктивных конструкций Coq и других зависимо типизированных языках , по модулю зависимых типов и за исключением того, что последние имеют дополнительное ограничение положительности, которое не применяется в GADT. [6]
Сульцман, Вазни и Стаки (2006) ввели расширенные алгебраические типы данных , которые объединяют GADT с экзистенциальными типами данных и ограничениями классов типов .
Вывод типа при отсутствии какой-либо предоставленной программистом аннотации типа неразрешим [7], а функции, определенные в GADT, в общем случае не допускают основных типов . [8] Реконструкция типа требует нескольких компромиссов в проектировании и является областью активных исследований (Peyton Jones, Washburn & Weirich 2004; Peyton Jones et al. 2006.
Весной 2021 года выходит Scala 3.0. [9] Это крупное обновление Scala вводит возможность писать GADT [10] с тем же синтаксисом, что и алгебраические типы данных, чего нет в других языках программирования, по словам Мартина Одерски . [11]
Приложения GADT включают в себя общее программирование , моделирование языков программирования ( абстрактный синтаксис высшего порядка ), поддержание инвариантов в структурах данных , выражение ограничений во встроенных предметно-ориентированных языках и моделирование объектов. [12]
Важным применением GADT является встраивание абстрактного синтаксиса высшего порядка в безопасном для типов режиме. Вот встраивание простого типизированного лямбда-исчисления с произвольным набором базовых типов, типов произведений ( кортежей ) и комбинатора с фиксированной точкой :
данные 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 f x ) = ( eval f ) ( eval x ) eval ( Fix f ) = ( eval f ) ( eval ( Fix f )) Факториальную функцию теперь можно записать как:
факт = Исправить ( Лам ( \ f -> Лам ( \ y -> Поднять ( если eval y == 0 тогда 1 иначе 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конструктора данных.
