Из Википедии, свободной энциклопедии
  (Перенаправлено из GADT )
Перейти к навигации Перейти к поиску

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

Обзор [ править ]

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

- Параметрический ADT, не являющийся списком данных  GADT a = Nil | Минусы a ( список a )        целые числа  =  Cons  12  ( Cons  107  Nil )  - тип целых чисел - List Int strings  =  Cons  "лодка"  ( Cons  "dock"  Nil )  - тип строк - List String- Данные  GADT Expr  a,  где  EBool  ::  Bool  ->  Expr  Bool  EInt  ::  Int  ->  Expr  Int  EEqual  ::  Expr  Int  ->  Expr  Int  ->  Expr  Booleval  ::  Выражение  а  ->  аeval  e  =  case  e  для  EBool  a  ->  a  EInt  a  ->  a  EEqual  a  b  ->  ( eval  a )  ==  ( eval  b )expr1  =  EEqual  ( EInt  2 )  ( EInt  3 )  - тип expr1 - Expr Bool ret  =  eval  expr1  - ret - False

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

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

История [ править ]

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

Обобщенные алгебраические типы данных были введены независимо друг от друга Чейни и Гинце (2003) и до по Си, Chen & Chen (2003) в качестве расширения для ML «s и Haskell » s алгебраических типов данных . [5] Оба по существу эквивалентны друг другу. Они похожи на индуктивные семейства типов данных (или индуктивных типов данных ) , найденных в Coq «s Исчисление Индуктивного конструкция и других в зависимости типизированных языков , по модулю зависимых типов и за исключение того, что последние имеют дополнительное ограничение позитивности , не вынужденные в GADTs .[6]

Sulzmann, Wazny & Stuckey (2006) представили расширенные алгебраические типы данных, которые объединяют GADT вместе с экзистенциальными типами данных и ограничениями классов типов, введенными Perry (1991) , Läufer & Odersky (1994) и Läufer (1996) .

Тип вывод в отсутствии какой - либо программист поставляется аннотация типа является неразрешимым [7] и функция , определенная над GADTs не допускает основные типов в целом. [8] Реконструкция типа требует нескольких компромиссов в дизайне и является областью активных исследований ( Peyton Jones, Washburn & Weirich 2004 ; Peyton Jones et al. 2006 ; Pottier & Régis-Gianas 2006 ; Sulzmann, Schrijvers & Stuckey 2006 ; Simonet & Pottier 2007 ; Schrijvers et al.2009 ; Lin & Sheard 2010a ; Lin & Sheard 2010b ;Витиниотис, Пейтон Джонс и Шрайверс 2010 ; Vytiniotis et al. 2011 ).

Приложения [ править ]

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

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

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

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

data  Lam  ::  *  ->  *  где  Lift  ::  a  ->  Lam  a  - ^ поднятое значение  Pair  ::  Lam  a  ->  Lam  b  ->  Lam  ( a ,  b )  - ^ product  Lam  ::  ( Lam  a  - >  Lam  b )  ->  Lam  ( a  ->  b )  - ^ лямбда-абстракция  App  ::  Lam  ( a  ->  b ) ->  Lam  a  ->  Lam  b  - ^ function application  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  ( Приложение  f  x )  =  ( eval  f )  ( eval  x) eval  ( Исправить  f )  =  ( eval  f )  ( eval  ( Исправить  f ))

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

fact  =  Fix  ( Lam  ( \ f  ->  Lam  ( \ y  ->  Lift  ( если  eval  y  ==  0,  то  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 is Lam (a -> b)выводится из типа конструктора Lamданных.

См. Также [ править ]

  • Переменная типа

Заметки [ править ]

  1. ^ Чейни и Hinze 2003 .
  2. ^ Си, Чен и Чен 2003 .
  3. ^ Sheard & Pasalic 2004 .
  4. ^ "OCaml 4.00.1" . ocaml.org .
  5. ^ Чейни и Hinze 2003 , стр. 25.
  6. ^ Чейни и Hinze 2003 , стр. 25-26.
  7. Перейти ↑ Peyton Jones, Washburn & Weirich 2004 , p. 7.
  8. ^ Schrijvers et al. 2009 , стр. 1.
  9. Перейти ↑ Peyton Jones, Washburn & Weirich 2004 , p. 3.

Дальнейшее чтение [ править ]

Приложения
  • Аугустссон, Леннарт ; Петерссон, Кент (сентябрь 1994 г.). «Семейства глупых типов» (PDF) . Cite journal requires |journal= (help)
  • Чейни, Джеймс ; Хинце, Ральф (2003). «Первоклассные фантомные типы». Технический отчет CUCIS TR2003-1901 . Корнелл Университет. hdl : 1813/5614 .
  • Си, Хунвэй ; Чен, Чиянь ; Чен, Ганг (2003). Защищенные рекурсивные конструкторы типов данных . Материалы 30-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования (POPL'03) . ACM Press. С. 224–235. CiteSeerX  10.1.1.59.4622 . DOI : 10.1145 / 604131.604150 . ISBN 978-1581136289.
  • Шеард, Тим ; Пашалич, Эмир (2004). «Мета-программирование со встроенным равенством типов» . Труды Четвертого международного семинара по логическим каркасам и метаязыкам (LFM'04), Корк . 199 : 49–65. DOI : 10.1016 / j.entcs.2007.11.012 .
Семантика
  • Патрисия Йоханн и Нил Гани (2008). «Основы структурного программирования с помощью GADT».
  • Ари Мидделкооп, Аце Дейкстра и С. Доаитсе Свиерстра (2011). «Бережливая спецификация для GADT: система F с первоклассными доказательствами равенства». Вычисление высшего порядка и символическое вычисление .
Тип реконструкции
  • Пейтон Джонс, Саймон ; Вашберн, Джеффри ; Вейрих, Стефани (2004). «Шаткие типы: вывод типов для обобщенных алгебраических типов данных» (PDF) . Технический отчет MS-CIS-05-25 . Пенсильванский университет.
  • Пейтон Джонс, Саймон ; Витиниотис, Димитриос ; Вейрих, Стефани ; Уошберн, Джеффри (2006). «Простой вывод типа на основе унификации для GADT» (PDF) . Труды Международной конференции ACM по функциональному программированию (ICFP'06), Портленд .
  • Зульцманн, Мартин ; Wazny, Джереми ; Стаки, Питер Дж. (2006). «Платформа для расширенных алгебраических типов данных». В Hagiya, M .; Wadler, P. (ред.). 8-й Международный симпозиум по функциональному и логическому программированию (FLOPS 2006) . Конспект лекций по информатике . 3945 . С. 46–64.
  • Зульцманн, Мартин ; Шрайверс, Том ; Стаки, Питер Дж. (2006). «Вывод основного типа для классов многопараметрических типов в стиле GHC». В Кобаяси, Наоки (ред.). Языки и системы программирования: 4-й Азиатский симпозиум (APLAS 2006) . Конспект лекций по информатике. 4279 . С. 26–43.
  • Шрайверс, Том ; Пейтон Джонс, Саймон ; Зульцманн, Мартин ; Витиниотис, Димитриос (2009). «Полный и разрешимый вывод типов для GADT» (PDF) . Труды Международной конференции ACM по функциональному программированию (ICFP'09), Эдинбург .
  • Линь, Чуан-кай (2010). Практический вывод типа для системы типов GADT (PDF) (докторская диссертация). Государственный университет Портленда.
Другой
  • Эндрю Кеннеди и Клаудио В. Руссо. «Обобщенные алгебраические типы данных и объектно-ориентированное программирование». В материалах 20-й ежегодной конференции ACM SIGPLAN по объектно-ориентированному программированию, системам, языкам и приложениям . ACM Press, 2005.

Внешние ссылки [ править ]

  • Страница обобщенных алгебраических типов данных в вики по Haskell
  • Обобщенные алгебраические типы данных в Руководстве пользователя GHC
  • Обобщенные алгебраические типы данных и объектно-ориентированное программирование
  • GADT - Haskell Prime - Trac
  • Статьи о выводе типов для GADT , библиография Саймона Пейтона Джонса
  • Вывод типа с ограничениями , библиография Саймона Пейтона Джонса
  • Эмуляция GADT на Java с помощью леммы Йонеды