일반 대수 데이터 유형
Generalized algebraic data type기능 프로그래밍에서 일반화된 대수 데이터 유형(GADT, 또한 1종 팬텀 유형,[1] 보호되는 재귀 데이터 유형 [2]또는 동등 자격 유형[3])은 파라메트릭 대수 데이터 유형의 일반화다.
개요
GADT에서 제품 생성자(Haskell에서 데이터 생성자라고 함)는 수익가치의 유형 인스턴스화로서 ADT의 명시적 인스턴스화를 제공할 수 있다.이를 통해 보다 고급 유형 동작으로 함수를 정의할 수 있다.Haskell 2010의 데이터 생성자의 경우, 반환 값은 생성자의 애플리케이션에서 ADT 매개변수의 인스턴스화에 의해 암시되는 유형의 인스턴스화를 가진다.
- GADT가 아닌 파라메트릭 ADT 자료 리스트 a = 닐 단점 a (리스트 a) 정수 = 단점 12 (단점 107 닐) - 정수의 유형은 List Int이다. 줄들 = 단점 "보트" (단점 "dock" 닐) -- 문자열의 유형은 목록 문자열 ­ 갓트 자료 엑스퍼 a 어디에 에볼 :: 불 -> 엑스퍼 불 EInt :: 인트 -> 엑스퍼 인트 EEqual :: 엑스퍼 인트 -> 엑스퍼 인트 -> 엑스퍼 불 평가하다 :: 엑스퍼 a -> a 평가하다 e = 케이스 e 의 에볼 a -> a EInt a -> a EEqual a b -> (평가하다 a) == (평가하다 b) expr1 = EEqual (EInt 2) (EInt 3) - expr1의 유형은 expr Bool이다. 되받아치다 = 평가하다 expr1 -- ret is False 그것들은 현재 GHC 컴파일러에서 다른 것들 중에서도 퍼그와 닥스가 사용하는 비표준 확장으로 구현되어 있다.OCaml은 버전 4.00부터 기본적으로 GADT를 지원한다.[4]
GHC 구현은 실존적으로 계량화된 형식 매개변수와 국소 제약에 대한 지원을 제공한다.
역사
일반화된 대수 데이터 유형의 초기 버전은 아우구스트손과 피터슨(1994)에 의해 설명되었고 ALF의 패턴 매칭에 기초하였다.
일반화된 대수 데이터 유형은 체니&힌제(2003)가 독자적으로 도입했고, 시 주석, 첸&첸(2003)이 ML과 하스켈의 대수 데이터 유형에 대한 확장으로 도입했다.[5]둘 다 본질적으로 서로 동등하다.이들은 Coq의 유도 구성 미적분학 및 기타 의존적으로 입력된 언어에서 발견되는 데이터 유형(또는 유도 데이터 유형)의 유도 계열과 유사하며, 종속 유형을 변조하고, 후자는 GADT에서 시행되지 않는 추가적인 긍정의 제한을 가지고 있다는 점을 제외한다.[6]
Sulzmann, Wazny &, Stuckey(2006년)을 소개했다 확장된 대수적 데이터 형식을 결합한 GADTs과 함께 실존적 데이터 형식과 유형 클래스 제약 조건 도입된 페리(1991년)harvtxt 오류:노 타깃:CITEREFPerry1991( 도와 주), Läufer &, Odersky(1994년)harvtxt 오류:노 타깃:CITEREFLäuferOdersky1994( 도와 주)과 Läufer(1996년)하.어rvtxt
프로그래머가 제공한 유형의 주석이 없는 경우 형식 추론은 확인되지[7] 않으며 GADT를 통해 정의된 함수는 일반적으로 주형을 인정하지 않는다.[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 et al. 2009; Lin & Sheard 2010a 오류: 없음: Lin & Sheard : 대상 없음:Vytiniotis, Peyton Jones & Schrijvers 2010 Vytiniotis et al. 2011 ).
2021년 봄에는 스칼라 3.0이 출시된다.[9]스칼라의 이번 주요 업데이트는 ADT와 동일한 구문으로 GADT를[10] 쓸 수 있는 가능성을 소개하는데, 마틴 오더스키에 따르면 다른 프로그래밍 언어에서는 그렇지 않다.[11]
적용들
GADT의 응용 프로그램에는 일반 프로그래밍, 모델링 프로그래밍 언어(고차 추상 구문), 데이터 구조에서 불변성 유지, 내장된 도메인 고유 언어의 제약 표현, 모델링 객체 등이 포함된다.[12]
고차 추상 구문
GADT의 중요한 적용은 고차 추상 구문을 안전한 유형으로 내장하는 것이다.여기에 기본 유형, 튜플 및 고정 점 결합기의 임의 컬렉션이 포함된 단순 타이핑 람다 미적분학:
자료 램 :: * -> * 어디에 들어올리다 :: a -> 램 a -- ^ 상승된 값 짝을 :: 램 a -> 램 b -> 램 (a, b) -- ^ 제품 램 :: (램 a -> 램 b) -> 램 (a -> b) - ^ 람다 추상화 앱. :: 램 (a -> b) -> 램 a -> 램 b -- ^ 함수 적용 고치다 :: 램 (a -> a) -> 램 a -- ^ 고정점 유형 안전 평가 기능:
평가하다 :: 램 t -> t 평가하다 (들어올리다 v) = v 평가하다 (짝을 l r) = (평가하다 l, 평가하다 r) 평가하다 (램 f) = \x -> 평가하다 (f (들어올리다 x)) 평가하다 (앱. f x) = (평가하다 f) (평가하다 x) 평가하다 (고치다 f) = (평가하다 f) (평가하다 (고치다 f)) 이제 요인 함수는 다음과 같이 기록할 수 있다.
사실의 = 고치다 (램 (\f -> 램 (\y -> 들어올리다 (만일 평가하다 y == 0 그때 1 다른 평가하다 y * (평가하다 f) (평가하다 y - 1))))) 평가하다(사실의)(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.
- ^ Xi, Chen & Chen 2003.
- ^ 셰어드 & 파살릭 2004.
- ^ "OCaml 4.00.1". ocaml.org.
- ^ 체니 & 힌제 2003, 페이지 25.
- ^ 체니 & 힌즈 2003, 25-26페이지.
- ^ 페이튼 존스, 워시번 & 위리히 2004, 페이지 7.
- ^ 슈리히버스 외 연구진 2009년, 페이지 1.
- ^ Kmetiuk, Anatolii. "SCALA 3 IS HERE!🎉🎉🎉". scala-lang.org. École Polytechnique Fédérale Lausanne (EPFL) Lausanne, Switzerland. Retrieved 19 May 2021.
- ^ "SCALA 3 — BOOK ALGEBRAIC DATA TYPES". scala-lang.org. École Polytechnique Fédérale Lausanne (EPFL) Lausanne, Switzerland. Retrieved 19 May 2021.
- ^ Odersky, Martin. "A Tour of Scala 3 - Martin Odersky". youtube.com. Scala Days Conferences. Archived from the original on 2021-12-19. Retrieved 19 May 2021.
- ^ 페이튼 존스, 워시번 & 위리히 2004, 페이지 3.
추가 읽기
- 적용들
- Augustsson, Lennart; Petersson, Kent (September 1994). "Silly type families" (PDF).
{{cite journal}}:Cite 저널은 필요로 한다.journal=(도움말) - Cheney, James; Hinze, Ralf (2003). "First-Class Phantom Types". Technical Report CUCIS TR2003-1901. Cornell University. hdl:1813/5614.
- Xi, Hongwei; Chen, Chiyan; Chen, Gang (2003). Guarded Recursive Datatype Constructors. Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'03). ACM Press. pp. 224–235. CiteSeerX 10.1.1.59.4622. doi:10.1145/604131.604150. ISBN 978-1581136289.
- Sheard, Tim; Pasalic, Emir (2004). "Meta-programming with built-in type equality". Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-languages (LFM'04), Cork. 199: 49–65. doi:10.1016/j.entcs.2007.11.012.
- 의미론
- Patricia Johann과 Neil Ghani(2008)이다."GADT를 이용한 구조화 프로그래밍 기반"
- 아리 미들코프, 아체 디크스트라와 S.Doaitse Swierstra(2011)."GADT에 대한 희박한 규격: 1등급 동등성 증명이 있는 시스템 F"고차 및 심볼 연산.
- 유형재구성
- Peyton Jones, Simon; Washburn, Geoffrey; Weirich, Stephanie (2004). "Wobbly types: type inference for generalised algebraic data types" (PDF). Technical Report MS-CIS-05-25. University of Pennsylvania.
- Peyton Jones, Simon; Vytiniotis, Dimitrios; Weirich, Stephanie; Washburn, Geoffrey (2006). "Simple Unification-based Type Inference for GADTs" (PDF). Proceedings of the ACM International Conference on Functional Programming (ICFP'06), Portland.
- Sulzmann, Martin; Wazny, Jeremy; Stuckey, Peter J. (2006). "A Framework for Extended Algebraic Data Types". In Hagiya, M.; Wadler, P. (eds.). 8th International Symposium on Functional and Logic Programming (FLOPS 2006). Lecture Notes in Computer Science. Vol. 3945. pp. 46–64.
- Sulzmann, Martin; Schrijvers, Tom; Stuckey, Peter J. (2006). "Principal Type Inference for GHC-Style Multi-Parameter Type Classes". In Kobayashi, Naoki (ed.). Programming Languages and Systems: 4th Asian Symposium (APLAS 2006). Lecture Notes in Computer Science. Vol. 4279. pp. 26–43.
- Schrijvers, Tom; Peyton Jones, Simon; Sulzmann, Martin; Vytiniotis, Dimitrios (2009). "Complete and Decidable Type Inference for GADTs" (PDF). Proceedings of the ACM International Conference on Functional Programming (ICFP'09), Edinburgh.
- Lin, Chuan-kai (2010). Practical Type Inference for the GADT Type System (PDF) (Doctoral Dissertation thesis). Portland State University.
- 기타
- Andrew Kennedy와 Claudio 5세.루소 "일반화된 대수 데이터 유형과 객체 지향 프로그래밍"객체 지향 프로그래밍, 시스템, 언어 및 애플리케이션에 관한 제20차 연례 ACM SIGPlAN 회의의 진행에서.ACM Press, 2005.
외부 링크
 | Wikibooks에는 다음과 같은 주제의 책이 있다.하스켈/GADT |
- Haskell wiki의 Generalized 대수 데이터 유형 페이지
- GHC 사용자 가이드의 일반화된 대수 데이터 유형
- 일반화된 대수 데이터 유형과 객체 지향 프로그래밍
- GADT – Haskell Prime – Trac
- Simon Peyton Jones의 도서 목록, GADT에 대한 유형 추론에 관한 논문
- 제약조건에 대한 유형추론, 사이먼 페이튼 존스의 참고 문헌 목록
- 요네다 보조정리기를 통한 자바의 GADT 에뮬레이션
