Обобщенный алгебраический тип данных

В функциональном программировании — обобщенный алгебраический тип данных ( GADT , также первоклассный фантомный тип , защищенный рекурсивный тип данных , или тип с указанием равенства ) является обобщением параметрических алгебраических типов данных .

Обзор

В GADT конструкторы продуктов (называемые конструкторами данных в Haskell ) могут обеспечить явное создание экземпляра ADT в качестве экземпляра типа возвращаемого значения. Это позволяет определять функции с более продвинутым типом поведения. Для конструктора данных Haskell 2010 возвращаемое значение имеет экземпляр типа, подразумеваемый созданием экземпляра параметров ADT в приложении конструктора.

-- A parametric ADT that is not a GADT
data List a = Nil | Cons a (List a)

integers :: List Int
integers = Cons 12 (Cons 107 Nil)

strings :: List String
strings = Cons "boat" (Cons "dock" Nil)

-- A GADT
data Expr a where
    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 -- False

В настоящее время они реализованы в компиляторе GHC как нестандартное расширение, используемое, в частности, Pugs и Darcs . OCaml изначально поддерживает GADT, начиная с версии 4.00.

Реализация GHC обеспечивает поддержку параметров экзистенциального количественного типа и локальных ограничений.

История

Ранняя версия обобщенных алгебраических типов данных была описана Augustsson & Petersson (1994) и основана на сопоставлении с образцом в ALF .

Обобщенные алгебраические типы данных были независимо представлены Чейни и Хинце (2003) , а ранее Си, Ченом и Ченом (2003) как расширения ML и Haskell алгебраических типов данных . Оба по сути эквивалентны друг другу. Они подобны индуктивным семействам типов данных (или индуктивным типам данных ), найденным в и Кока «Исчислении индуктивных конструкций» других зависимо типизированных языках , по модулю зависимых типов и за исключением того, что последние имеют дополнительное ограничение положительности , которое не применяется в GADT. .

Сульцманн, Вазни и Стаки (2006) представили расширенные алгебраические типы данных , которые объединяют GADT вместе с экзистенциальными типами данных и ограничениями классов типов .

Вывод типа в отсутствие каких-либо аннотаций типа , предоставленных программистом, неразрешим . не допускают основных типов . и функции, определенные в GADT, вообще Реконструкция типа требует нескольких конструктивных компромиссов и является областью активных исследований ( Пейтон Джонс, Уошберн и Вейрих, 2004 ; Пейтон Джонс и др., 2006 ).

Весной 2021 года выйдет Scala 3.0. В этом крупном обновлении Scala появилась возможность писать GADT. с тем же синтаксисом, что и ADT , чего нет в других языках программирования, по мнению Мартина Одерски .

Приложения

Приложения GADT включают общее программирование , моделирование языков программирования ( абстрактный синтаксис высшего порядка ), поддержание инвариантов в структурах данных , выражение ограничений во встроенных предметно-ориентированных языках и моделирование объектов.

Абстрактный синтаксис высшего порядка

Дополнительная информация: абстрактный синтаксис высшего порядка.

Важным применением GADT является встраивание абстрактного синтаксиса высшего порядка для безопасным типов способом. Вот встраивание просто типизированного лямбда-исчисления с произвольным набором базовых типов , кортежами и комбинатором с фиксированной точкой :

data Lam :: * -> * where
  Lift :: a                     -> Lam a        -- ^ lifted value
  Pair :: Lam a -> Lam b        -> Lam (a, b)   -- ^ product
  Lam  :: (Lam a -> Lam b)      -> Lam (a -> b) -- ^ lambda abstraction
  App  :: Lam (a -> b) -> Lam a -> Lam b        -- ^ function application
  Fix  :: Lam (a -> a)          -> Lam a        -- ^ fixed point

И типобезопасная функция оценки:

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))

Теперь функцию факториала можно записать так:

fact = Fix (Lam (\f -> Lam (\y -> Lift (if eval y == 0 then 1 else eval y * (eval f) (eval y - 1)))))
eval(fact)(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 конструктор данных.

См. также

• Тип переменной

Дальнейшее чтение

Приложения

• Аугустссон, Леннарт ; Петерссон, Кент (сентябрь 1994 г.). «Семьи глупых типов» (PDF) .
• Чейни, Джеймс ; Хинце, Ральф (2003). «Первоклассные фантомные типы». Технический отчет CUCIS TR2003-1901 . Корнелльский университет. 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 с помощью леммы Йонеды