행 다형성

위키백과, 우리 모두의 백과사전

프로그래밍 언어 타입 이론에서 행 다형성은 다형성의 한 종류로, 레코드 타입 및/또는 변이체에 대해 구조적으로 [1] (명목적으로가 아니라) 다형적인 프로그램을 작성할 수 있게 한다.[2]

레코드에 대한 행 다형적 타입 시스템과 타입 추론의 증명은 Mitchell Wand가 도입하였다.[3][4]

행 다형성의 이론적 취급은 레코드 안에서 레이블이 서로 달라야 한다는 필요 때문에 다소 복잡해진다. Rémy와 동료들이 취한 한 가지 접근법은(그리고 아래의 설명에도 암묵적으로 나타나며, 이는 Wand의 설명에서 강하게 영감을 받았다) 레이블에 따라 서로 다른 행 타입의 종(kind)을 고려하는 것이다.[2]

Gaster와 Jones는 이 접근을 변이체에도 비형식적으로 확장하여, 레코드와 변이체 타입 생성자가 모두 행의 kind에서 타입으로 사상되도록 하였다.[5]

Blume 등은 continuation을 case-matching 코드에서 조합하기 위해 LetCC 구문이 처리하는 “일급 케이스(first-class cases)”를 추가함으로써, 이 접근을 조합 가능한 확장의 영역으로 한 걸음 더 밀고 나갈 것을 제안했다.[6] 이후 몇몇 프로젝트(Links, Koka)는 행 다형성을 대수적 효과 시스템의 타입 기반으로 사용하여, 사용자가 정의한 효과의 “자유로운 조합”을 목표로 삼았다.[7][8]

고유한 레이블 문제에 대한 또 다른 접근은 system F를 “coherent merge” 연산자로 확장하는 것으로, 이로부터 이른바 서로소 교차 타입을 갖는 계산 체계가 나온다.[9]

Morris와 McKinna는 행 타입을 행 이론으로 일반화하여, 하나의 이론적 틀 안에서 (레코드) 확장에 대한 다양한 개념을 일관되게 다루었다. 예를 들어 어떤 응용은 확장 연산이 이름이 일치할 때 기존 필드를 덮어쓰기를 원할 수 있고, 다른 응용은 둘 다 접근 가능하게 유지하기를 원할 수 있으며, 또 어떤 경우에는 경로 기반 주소 지정 방식을 원할 수도 있다.[10]

행 다형적 레코드 타입 정의

[편집]

행 다형적 레코드 타입은 각 필드와 그에 대응하는 타입의 목록, 누락된 필드의 목록, 그리고 임의의 추가 필드의 부재 또는 존재를 나타내는 변수를 정의한다. 두 목록은 모두 선택 사항이며, 변수에는 제약이 걸릴 수 있다. 구체적으로 이 변수는 “empty”일 수 있는데, 이는 그 레코드에 추가 필드가 존재할 수 없음을 뜻한다.

이는 $Image 1: {\displaystyle {\ell {1}:T{1},\dots ,\ell {n}:T{n},{\text{absent}}(f_{1}),\dots ,{\text{absent}}(f_{m}),\rho }}$ 와 같이 쓸 수 있다. 이는 각각 $Image 2: {\displaystyle \ell _{i}}$ 라는 필드를 가지며 그 타입이 $Image 3: {\displaystyle T_{i}}$ 인(단 $Image 4: {\displaystyle i=1\dots n}$ ) 레코드 타입을 나타내고, 또한 $Image 5: {\displaystyle f_{j}}$ 라는 필드는 가지지 않으며(단 $Image 6: {\displaystyle j=1\dots m}$ ), 한편 $Image 7: {\displaystyle \rho }$ 는 레코드가 $Image 8: {\displaystyle \ell _{i}}$ 이외의 다른 필드를 포함할 수 있음을 표현한다.

행 다형적 레코드 타입을 사용하면 레코드의 일부 구간에만 작용하는 프로그램을 작성할 수 있다. 예를 들어 두 개 이상의 좌표를 가진 레코드를 받아 동일한 타입을 반환하는 어떤 2차원 변환 함수를 정의할 수 있다.

$Image 9: {\displaystyle {\text{transform2d}}:{x:{\text{Number}},y:{\text{Number}},\rho }\to {x:{\text{Number}},y:{\text{Number}},\rho }}$

행 다형성 덕분에 이 함수는 3차원(사실은 _n_차원) 점에 대해서도 2차원 변환을 수행할 수 있으며, z 좌표(또는 다른 어떤 좌표든)를 그대로 유지한다. 보다 일반적으로 말하면, 이 함수는 $Image 10: {\displaystyle x}$ 와 $Image 11: {\displaystyle y}$ 필드를 타입 $Image 12: {\displaystyle {\text{Number}}}$ 와 함께 포함하는 어떤 레코드에도 작용할 수 있다. 정보 손실은 없다. 타입은 변수 $Image 13: {\displaystyle \rho }$ 로 표현되는 모든 필드가 반환 타입에도 존재함을 보장한다. 이와 대조적으로 타입 정의 $Image 14: {\displaystyle {x:{\text{Number}},y:{\text{Number}},\mathbf {empty} }}$ 는 그 타입의 레코드가 정확히 $Image 15: {\displaystyle x}$ 와 $Image 16: {\displaystyle y}$ 필드만 가지고 그 외에는 아무것도 없다는 사실을 표현한다. 이 경우에는 고전적인 레코드 타입이 얻어진다.

레코드에 대한 연산의 타입 지정

[편집]

필드 선택 $Image 17: {\displaystyle r.\ell }$ , 필드 추가 $Image 18: {\displaystyle r[\ell :=e]}$ , 필드 제거 $Image 19: {\displaystyle r\backslash \ell }$ 와 같은 레코드 연산에는 행 다형적 타입을 부여할 수 있다.

$Image 20: {\displaystyle \mathrm {select_{\ell }} =\lambda r.(r.\ell );:;{\ell :T,\rho }\rightarrow T}$

$Image 21: {\displaystyle \mathrm {add_{\ell }} =\lambda r.\lambda e.r[\ell :=e];:;{\mathrm {absent} (\ell ),\rho }\rightarrow T\rightarrow {\ell :T,\rho }}$

$Image 22: {\displaystyle \mathrm {remove_{\ell }} =\lambda r.r\backslash \ell ;:;{\ell :T,\rho }\rightarrow {\mathrm {absent} (\ell ),\rho }}$

행 다형성은 Standard ML에서는 지원되지 않지만, SML#[11]이나 Ocaml 같은 몇몇 확장판 또는 파생 언어에서는 지원된다.

SML#의 첫 번째 버전이 존재하게 된 직접적인 동기 중 하나는[12] 행 다형성의 추가였으며, 이는 Ohori 등[13]의 SIGMOD '89 논문에 기반한 것이었다. 이 논문은 SML에 대한 “Machiavelli” 확장을 도입했지만, 그 이름은 나중에 “SML# of Kansai”로 바뀌었고, 다시 더 짧은 이름으로 정착했다. 이름의 '#'는 F#와는 아무 관련이 없으며, 필드 접근에서 행 다형적 타입을 암묵적으로 정의하는 데 사용되는 # 연산자에서 유래한 것이다.

Ocaml에서는 행 다형성이 Ocaml의 object 타입과 다형적 변이체에 사용된다. 일반적인 레코드 타입은 Ocaml에서 행 다형적이지 않다.[14] Castagna 등은 Ocaml에 흐름 민감 타입 지정이 부족하다고 비판했는데, 이는 특히 다형적 변이체의 타입 추론에서 두드러진다. 또한 이들은 Ocaml에 진정한 비태그형 합집합 타입이 없기 때문에, 다형적 변이체에 대해 추론되는 일부 타입이 지나치게 제한적이라고 지적한다. 특히 곱 타입이 다형적 변이체와 함께 사용될 때 그러하다.[15]

F#는 “Statically Resolved Type Parameters”(SRTP) 메커니즘을 사용하여 행 다형성을 모사할 수 있으며, [16] 이는 비형식적으로 “정적 덕 타이핑”이라고도 불린다.[17] 그러나 이는 인라인 F# 함수에만 제한되므로, 그러한 함수들은 .NET 타입 시스템으로 내보내지지 않으며, .NET 자체도 이러한 기능을 지원하지 않는다.

행 다형성은 PureScript에서도 지원된다.[18]

^https://www.cs.cmu.edu/~aldrich/courses/819/slides/rows.pdf, p. 12
^ 위로 가기: a bFrançois Pottier and Didier Rémy, "The Essence of ML Type Inference", chapter 10 in Advanced Topics in Types and Programming Languages, edited by Benjamin C. Pierce, MIT Press, 2005. pages 389–489. In particular see p. 466 where record types are discussed and p. 483 where polymorphic variants are discussed.
**^**Wand, Mitchell (June 1989). "Type inference for record concatenation and multiple inheritance". Proceedings. Fourth Annual Symposium on Logic in Computer Science. pp.92–97. doi:10.1109/LICS.1989.39162.
**^**Wand, Mitchell (1991). "Type inference for record concatenation and multiple inheritance". Information and Computation. 93 (Selections from 1989 IEEE Symposium on Logic in Computer Science): 1–15. doi:10.1016/0890-5401(91)90050-C. ISSN 0890-5401.
**^**Benedict R. Gaster and Mark P. Jones, A Polymorphic Type System for Extensible Records and Variants, Technical report NOTTCS-TR-96-3, November 1996
**^**Matthias Blume, Umut A. Acar, Wonseok Chae, Extensible programming with first-class cases, ICFP '06
**^**D. Leijen. Koka: Programming with row polymorphic effect types. In P. Levy and N. Krishnaswami, editors, Proceedings 5th Workshop on Mathematically Structured Functional Programming, MSFP, Grenoble, France, April 2014, volume 153 of EPTCS, pages 100–126, 2014
**^**Daniel Hillerström, and Sam Lindley. “Liberating Effects with Rows and Handlers.” TyDe 2016. Nara, Japan. 2016. doi:10.1145/2976022.2976033.
**^**Ningning Xie, Bruno C. d. S. Oliveira, Xuan Bi, Tom Schrijvers, Row and Bounded Polymorphism via Disjoint Polymorphism, ECOOP 2020
**^**J. Garrett Morris, James McKinna, "Abstracting extensible data types: or, rows by any other name", POPL 2019
^"8 SML# feature: Record polymorphism‣ Part II Tutorials ‣ SML# Document Version 4.0.0 - SML# Project".
^"A Brief History of SML# - SML# Project".
**^**Ohori, Atsushi; Buneman, Peter; Breazu-Tannen, Val (1989). "Database programming in Machiavelli---a polymorphic language with static type inference". Proceedings of the 1989 ACM SIGMOD international conference on Management of data - SIGMOD '89. pp.46–57. doi:10.1145/67544.66931. ISBN 0-89791-317-5.
^https://www.cl.cam.ac.uk/teaching/1415/L28/rows.pdf, p. 8
**^**Giuseppe Castagna, Tommaso Petrucciani, Kim Nguyễn, "Set-theoretic types for polymorphic variants", ICFP 2016
^"Polymorphwhat?". 8 December 2017.
^"Static Duck Typing in F# | Compositional IT".
^"Pattern Matching - PureScript by Example".

위키백과, 우리 모두의 백과사전

레코드에 대한 행 다형적 타입 시스템과 타입 추론의 증명은 Mitchell Wand가 도입하였다.[3][4]

Gaster와 Jones는 이 접근을 변이체에도 비형식적으로 확장하여, 레코드와 변이체 타입 생성자가 모두 행의 kind에서 타입으로 사상되도록 하였다.[5]

행 다형적 레코드 타입 정의

[편집]

$Image 9: {\displaystyle {\text{transform2d}}:{x:{\text{Number}},y:{\text{Number}},\rho }\to {x:{\text{Number}},y:{\text{Number}},\rho }}$

레코드에 대한 연산의 타입 지정

[편집]

$Image 20: {\displaystyle \mathrm {select_{\ell }} =\lambda r.(r.\ell );:;{\ell :T,\rho }\rightarrow T}$

$Image 21: {\displaystyle \mathrm {add_{\ell }} =\lambda r.\lambda e.r[\ell :=e];:;{\mathrm {absent} (\ell ),\rho }\rightarrow T\rightarrow {\ell :T,\rho }}$

$Image 22: {\displaystyle \mathrm {remove_{\ell }} =\lambda r.r\backslash \ell ;:;{\ell :T,\rho }\rightarrow {\mathrm {absent} (\ell ),\rho }}$

행 다형성은 Standard ML에서는 지원되지 않지만, SML#[11]이나 Ocaml 같은 몇몇 확장판 또는 파생 언어에서는 지원된다.

행 다형성은 PureScript에서도 지원된다.[18]

^https://www.cs.cmu.edu/~aldrich/courses/819/slides/rows.pdf, p. 12
^ 위로 가기: a bFrançois Pottier and Didier Rémy, "The Essence of ML Type Inference", chapter 10 in Advanced Topics in Types and Programming Languages, edited by Benjamin C. Pierce, MIT Press, 2005. pages 389–489. In particular see p. 466 where record types are discussed and p. 483 where polymorphic variants are discussed.
**^**Wand, Mitchell (June 1989). "Type inference for record concatenation and multiple inheritance". Proceedings. Fourth Annual Symposium on Logic in Computer Science. pp.92–97. doi:10.1109/LICS.1989.39162.
**^**Wand, Mitchell (1991). "Type inference for record concatenation and multiple inheritance". Information and Computation. 93 (Selections from 1989 IEEE Symposium on Logic in Computer Science): 1–15. doi:10.1016/0890-5401(91)90050-C. ISSN 0890-5401.
**^**Benedict R. Gaster and Mark P. Jones, A Polymorphic Type System for Extensible Records and Variants, Technical report NOTTCS-TR-96-3, November 1996
**^**Matthias Blume, Umut A. Acar, Wonseok Chae, Extensible programming with first-class cases, ICFP '06
**^**D. Leijen. Koka: Programming with row polymorphic effect types. In P. Levy and N. Krishnaswami, editors, Proceedings 5th Workshop on Mathematically Structured Functional Programming, MSFP, Grenoble, France, April 2014, volume 153 of EPTCS, pages 100–126, 2014
**^**Daniel Hillerström, and Sam Lindley. “Liberating Effects with Rows and Handlers.” TyDe 2016. Nara, Japan. 2016. doi:10.1145/2976022.2976033.
**^**Ningning Xie, Bruno C. d. S. Oliveira, Xuan Bi, Tom Schrijvers, Row and Bounded Polymorphism via Disjoint Polymorphism, ECOOP 2020
**^**J. Garrett Morris, James McKinna, "Abstracting extensible data types: or, rows by any other name", POPL 2019
^"8 SML# feature: Record polymorphism‣ Part II Tutorials ‣ SML# Document Version 4.0.0 - SML# Project".
^"A Brief History of SML# - SML# Project".
**^**Ohori, Atsushi; Buneman, Peter; Breazu-Tannen, Val (1989). "Database programming in Machiavelli---a polymorphic language with static type inference". Proceedings of the 1989 ACM SIGMOD international conference on Management of data - SIGMOD '89. pp.46–57. doi:10.1145/67544.66931. ISBN 0-89791-317-5.
^https://www.cl.cam.ac.uk/teaching/1415/L28/rows.pdf, p. 8
**^**Giuseppe Castagna, Tommaso Petrucciani, Kim Nguyễn, "Set-theoretic types for polymorphic variants", ICFP 2016
^"Polymorphwhat?". 8 December 2017.
^"Static Duck Typing in F# | Compositional IT".
^"Pattern Matching - PureScript by Example".

행 다형적 레코드 타입 정의

레코드에 대한 연산의 타입 지정

관련 추천 글

로우 타입 보트, 물살을 가르며

행 타입 로워링, 확실히

낮춰진 로우의 심장

X 설계 노트: OCaml 모듈과 값의 통합

행 다형적 레코드 타입 정의

레코드에 대한 연산의 타입 지정

관련 추천 글

로우 타입 보트, 물살을 가르며

행 타입 로워링, 확실히

낮춰진 로우의 심장

X 설계 노트: OCaml 모듈과 값의 통합