다형 재귀
Polymorphic recursion컴퓨터 과학에서 다형성 재귀(Molymorphic recursion, Milner-Mycroft typeability 또는 Milner-Mycroft 미적분이라고도 함)는 일정한 재귀 호출에 따라 유형 매개변수가 변화하는 재귀 파라메트릭 함수를 말한다.다형재귀의 유형추론은 반통합과 같기 때문에 결정할 수 없으며 반알고리즘 또는 프로그래머가 제공한 유형 [1]주석을 사용해야 합니다.
예
중첩된 데이터 유형
데이터. 네스트된 a = a :<: (네스트된 [a]) 입실론 인픽스 5 :<: 중첩된 = 1 :<: [2,3,4] :<: [[5,6],[7],[8,9]] :<: 입실론 이 데이터 유형에 대해 정의된 길이 함수는 인수 유형이 다음에서 변경됨에 따라 다형적으로 재귀적입니다.Nested a로.Nested [a]재귀 콜의 경우:
길이 :: 네스트된 a -> 내부 길이 입실론 = 0 길이 (_ :<: xs) = 1 + 길이 xs Haskell은 보통 이와 같이 단순한 함수의 유형 시그니처를 유추하지만 여기서는 유형 오류를 트리거하지 않고 생략할 수 없습니다.
상위 유형
![[icon]](/wiki/File:Wiki_letter_w_cropped.svg){kind=small} | 이 섹션은 확장해야 합니다.추가함으로써 도움이 될 수 있습니다. (2012년 5월) |
적용들
프로그램 분석
유형 기반 프로그램 분석에서 다형 재귀는 분석의 높은 정밀도를 얻기 위해 종종 필수적입니다.다형성 재귀를 사용하는 시스템의 주목할 만한 예로는 Dussart, Henglein 및 Mossin의 바인딩 시간[2] 분석 및 Tofe-Talpin 지역 기반 메모리 [3]관리 시스템이 있습니다.이러한 시스템은 표현식이 기본 유형 시스템에 이미 입력되었다고 가정하기 때문에(다형 재귀를 사용할 필요가 없음), 추론은 다시 결정될 수 있다.
데이터 구조, 오류 검출, 그래프 솔루션
기능적 프로그래밍 데이터 구조에서는 종종 다형 재귀를 사용하여 유형 오류 검사를 단순화하고 트리와 같은 보다 전통적인 데이터 구조에서 메모리를 소비하는 불쾌한 "중간" 임시 솔루션을 사용하여 문제를 해결합니다.다음 두 인용문에서 오카사키(p. 144~146)는 Haskell에서 다형식 시스템이 자동으로 프로그래머 [4]오류를 플래그하는 CONS 예를 제시한다.재귀적인 측면은 가장 바깥쪽 생성자가 단일 요소, 두 번째 쌍, 세 번째 쌍 등을 재귀적으로 가지도록 함으로써 데이터 유형에 자동 오류 검색 패턴을 설정하는 것입니다.Roberts(171)는 Java에서 클래스를 사용하여 스택프레임을 나타내는 관련 예를 나타냅니다.제시된 예는 하노이 타워 문제의 해결책으로 스택은 시작, 일시 및 종료 중첩된 스택 대체 구조를 사용하여 다형 재귀 [5]시뮬레이션을 수행합니다.
「 」를 참조해 주세요.
메모들
- ^ 헨글레인 1993년
- ^ Dussart, Dirk; Henglein, Fritz; Mossin, Christian. "Polymorphic Recursion and Subtype Qualifications: Polymorphic Binding-Time Analysis in Polynomial Time". Proceedings of the 2nd International Static Analysis Symposium (SAS).
- ^ Tofte, Mads; Talpin, Jean-Pierre (1994). "Implementation of the Typed Call-by-Value λ-calculus using a Stack of Regions". POPL '94: Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM. pp. 188–201. doi:10.1145/174675.177855. ISBN 0-89791-636-0.
- ^ Chris Okasaki (1999). Purely Functional Data Structures. New York: Cambridge. p. 144. ISBN 978-0521663502.
- ^ Eric Roberts (2006). Thinking Recursively with Java. New York: Wiley. p. 171. ISBN 978-0471701460.
추가 정보
- Meertens, Lambert (1983). "Incremental polymorphic type checking in B" (PDF). ACM Symposium on Principles of Programming Languages (POPL), Austin, Texas.
- Mycroft, Alan (1984). Polymorphic type schemes and recursive definitions. International Symposium on Programming, Toulouse, France. Lecture Notes in Computer Science. Vol. 167. pp. 217–228. doi:10.1007/3-540-12925-1_41. ISBN 978-3-540-12925-7.
- Henglein, Fritz (1993). "Type inference with polymorphic recursion". ACM Transactions on Programming Languages and Systems. 15 (2): 253–289. CiteSeerX 10.1.1.42.3091. doi:10.1145/169701.169692.
- Kfoury, A. J.; Tiuryn, J.; Urzyczyn, P. (April 1993). "Type reconstruction in the presence of polymorphic recursion". ACM Transactions on Programming Languages and Systems. 15 (2): 290–311. doi:10.1145/169701.169687. ISSN 0164-0925.
- Michael I. Schwartzbach (June 1995). "Polymorphic type inference". Technical Report BRICS-LS-95-3.
- Emms, Martin; Leiß, Hans (1996). "Extending the type checker for SML by polymorphic recursion—A correctness proof". Technical Report 96-101.
- 리처드 버드와 램버트 미어텐스(1998)."네스트된 데이터 유형"
- C. Vasconcellos, L. Figueiredo, C. Camarao(2003)"다형 재귀의 실용적 유형 추론: 해스켈에서의[dead link] 구현"유니버설 컴퓨터 사이언스 저널.
- L. 피게이레도, C. 카마리오"다형 재귀 정의에 대한 형식 추론: 해스켈의 사양"
- Hallett, J. J; Kfoury, A. J. (July 2005). "Programming Examples Needing Polymorphic Recursion". Electronic Notes in Theoretical Computer Science. 136: 57–102. doi:10.1016/j.entcs.2005.06.014. ISSN 1571-0661.
