서브타이핑

프로그래밍 언어이론에서 서브타이핑(subtyping, subtype polymorphism 또는 inclusion polymorphism)은 대체성의 어떤 개념에 의해 다른 데이터타입(슈퍼타입)과 관련되는 데이터타입인 타입의 일종으로, 프로그램 요소들, 전형적으로 서브루틴이나 함수들이 t의 요소에서 작동하도록 쓰여진 것을 의미한다.슈퍼타입은 서브타입의 요소에서도 작동할 수 있다.S가 T의 하위 유형인 경우, S 유형의 어떤 항도 T 유형의 항이 예상되는 맥락에서 안전하게 사용될 수 있다는 것을 의미하기 위해 S <: T의 하위 유형 관계를 종종 쓴다.서브타이핑의 정확한 의미론은 주어진 프로그래밍 언어에서 "안전하게 사용되는" 맥락에서 무엇을 의미하느냐의 세부사항에 따라 결정적으로 좌우된다.프로그래밍 언어의 형식 시스템은 기본적으로 자신의 하위 형식 관계를 정의하는데, 이는 언어가 no(또는 매우 적은) 변환 메커니즘을 지원하는 경우 그러하다.

하위 형식 관계로 인해 용어는 둘 이상의 유형에 속할 수 있다.그러므로 서브타이핑은 다형성의 한 형태다.객체지향적 프로그래밍에서 '폴리모프리즘'이라는 용어는 일반적으로 이 아형 다형만을 지칭하는 데 사용되는 반면, 파라메트릭 다형성의 기법은 일반적인 프로그래밍으로 간주될 것이다.

기능적인 프로그래밍 언어는 종종 레코드의 하위 형식화를 허용한다.따라서 기록 유형으로 확장된 단순 타이핑된 람다 미적분은 아마도 하위 타이핑의 유용한 개념을 정의하고 연구할 수 있는 가장 단순한 이론적 설정일 것이다.^[1]결과 미적분학은 항이 둘 이상의 유형을 가질 수 있도록 허용하기 때문에 더 이상 "단순한" 형태의 이론이 아니다.기능 프로그래밍 언어는 정의상 기록에도 저장될 수 있는 기능 리터럴을 지원하므로, 서브타이핑이 있는 레코드 타입은 객체 지향 프로그래밍의 특징의 일부를 제공한다.전형적으로 기능 프로그래밍 언어는 또한 일부, 대개 제한된 형태의 파라메트릭 다형성(parmetric polymorphism.이론적 설정에서는 두 형상의 상호작용을 연구하는 것이 바람직하다. 공통적인 이론적 설정은 시스템 F이다_<:.객체 지향 프로그래밍의 이론적 특성을 포착하려는 다양한 캘컬리는 시스템 F에서_<: 도출될 수 있다.

Subtyping의 개념은 hyponymy와 holonymy의 언어적 개념과 관련이 있다.수학적 논리에서의 경계 정량화 개념과도 관련이 있다(순서 정렬 논리 참조).서브타이핑은 객체지향 언어로부터(클래스 또는 객체)상속의 개념과 혼동해서는 안 되며,[2]서브타이핑은 유형들 간의 관계(객체지향적 언어의 상호관계)인 반면, 상속은 기존 객체로부터 새로운 객체를 창조할 수 있는 언어적 특징에서 기인하는 구현들 간의 관계다.여러 객체 지향 언어에서 하위 타이핑을 인터페이스 상속이라고 하며, 상속을 구현 상속이라고 한다.

오리진스

프로그래밍 언어에서 서브타이핑의 개념은 1960년대로 거슬러 올라간다; 그것은 Simula 파생상품에 도입되었다.서브타이핑의 첫 번째 공식적인 치료는 존 C에 의해 주어졌다. 1980년 범주 이론을 이용해 암묵적 전환을 공식화한 레이놀즈, 그리고 루카 카델리(1985)가 대표적이다.^[3]

서브타이핑의 개념은 객체 지향 프로그래밍의 주류 채택과 함께 가시성(그리고 일부 서클에서는 다형성과의 유사성)을 얻었다.이런 맥락에서 1987년 객체지향 프로그래밍에 관한 컨퍼런스의 기조연설에서 이를 대중화한 바바라 리스크노프의 이름을 따 안전대체 원리를 리스크노프 대체원리라고 부르는 경우가 많다.변이 가능한 객체를 고려해야 하기 때문에, 행동적 서브타이핑이라고 불리는 리스크노프와 제넷 윙에 의해 정의되는 서브타이핑의 이상적인 개념은 타입 체커에서 구현될 수 있는 것보다 상당히 강하다. (자세한 내용은 아래의 § 기능 유형 참조)

예

하위 유형 예: 여기서 새는 슈퍼 유형이고 다른 모든 유형은 UML 표기법에서 화살표로 표시된 하위 유형이다.

하위 유형의 간단한 실제 예가 도표에 나와 있다.'새'형식으로는 '덕', '쿠쿠', '오스트리치' 세 가지 아형이 있다.개념적으로 이들 각각은 많은 "새" 특성을 계승하지만 일부 구체적인 차이가 있는 기본형 "새"의 다양성이다.UML 표기법은 슈퍼타입과 그 하위타입 사이의 관계의 방향과 유형을 보여주는 오픈헤드 화살표가 이 다이어그램에서 사용된다.

보다 실제적인 예로서, 언어는 부동소수 값이 예상되는 곳이라면 어디에서나 정수 값을 사용할 수 있다.Integer<:Float() 또는 일반적인 유형의 정수와 실제의 일반적인 수퍼타입으로 정의할 수 있다.이 두 번째 경우, 우리는 단지Integer<:Number그리고Float<:Number그렇지만Integer그리고Float서로의 아형이 아니야

프로그래머들은 서브타이핑을 이용하여 코드 없이 가능한 것보다 더 추상적인 방법으로 코드를 작성할 수 있다.다음 예를 고려해 보십시오.

기능을 발휘하다 맥스. (x 로서 숫자, y 로서 숫자) 이다     만일 x < y 그때         돌아오다 y     다른         돌아오다 x 종지부를 찍다 

정수 및 실제가 둘 다의 하위 유형인 경우Number그리고 임의의 번호와의 비교 연산자는 두 가지 유형 모두에 대해 정의된다. 그러면 두 유형의 값은 이 함수에 전달될 수 있다.그러나, 그러한 연산자를 실행할 수 있는 바로 그 가능성은 숫자형(예를 들어 복잡한 숫자와 정수를 비교할 수 없음)을 상당히 구속하고, 실제로는 정수와의 정수, 실재와의 비교만 하는 것이 타당하다.같은 유형의 'x'와 'y'만 받아들이도록 이 함수를 다시 쓰는 것은 경계가 있는 다형성(bound polymorism)이 필요하다.

서브섬션

형식 이론에서 S형이 T형의 하위 유형인지 여부를 정의하거나 평가하는 데 Subsum의^[4] 개념을 사용한다.

유형은 값의 집합이다.집합은 모든 값을 나열하여 확장적으로 설명할 수도 있고, 또는 가능한 값의 영역에 걸쳐 술어에 의해 집합의 멤버십을 명시함으로써 장력적으로 설명할 수도 있다.공통 프로그래밍 언어에서 열거형은 값을 나열하여 확장적으로 정의된다.레코드(구조물, 인터페이스) 또는 클래스와 같은 사용자 정의 유형은 명시적 형식 선언 또는 형식 정보를 인코딩하는 기존 값을 복사하거나 확장할 프로토타입으로 사용하여 장력적으로 정의된다.

서브섬션의 개념을 논할 때, 형식의 값 집합은 수학 이탤릭체로 그 이름을 써서 표시한다:T.도메인 위에 술어로 보이는 유형은 그 이름을 굵은 글씨로 써서 표시한다:T.종래의 기호 <::는 "subtype"을 의미하고 :는 "supertype"을 의미한다.

• T형은 자신이 정의하는 값 T 집합이 S 집합의 상위 집합인 경우 S를 소급하여 S의 모든 멤버도 T의 멤버가 된다.
• 형식은 둘 이상의 유형으로 요약될 수 있다: S의 슈퍼타입은 S에서 교차한다.
• 만약 S <: T (따라서 S ⊆ T )가 되면, 세트 T를 곡선으로 하는 술어인 T는 S를 정의하는 (동일한 영역에 걸쳐) 술어 S의 일부가 되어야 한다.
• S가 T를 소급하고 T가 S를 소급하면 두 유형이 동일하다(형식 시스템이 이름별로 유형을 구분하는 경우에는 동일하지 않을 수 있지만).

경험 법칙은 다음과 같다: 하위 유형은 상위 유형(정보가 더 제한되고 하위 유형의 상위 집합인 경우) 중 하나보다 "더 큰/와이더/더 작은" (값 집합이 더 작은 경우)일 가능성이 높다.

서브섬션의 맥락에서 형식 정의는 술어를 사용하여 집합을 정의하는 Set-builder 표기법을 사용하여 표현할 수 있다.술어는 도메인(가능한 값의 집합) D에 걸쳐 정의될 수 있다.술어는 값을 선택 기준과 비교하는 부분 함수다.예를 들어, "정수 값이 100보다 크거나 같고 200보다 작다"는 식이다.값이 기준과 일치하면 함수는 값을 반환한다.그렇지 않으면 값을 선택하지 않고 아무것도 반환되지 않는다.(목록 포괄성은 많은 프로그래밍 언어에서 사용되는 이러한 패턴의 한 형태)

두 가지 술어가 있는 경우, ${\displaystyle P_{}}$ T ${\$T형식 선택기준을 적용하는$$ $T}$과 S형식 추가기준을 적용하는 P$$ ${\displaystyle s_{}}$ ${\$을(를) 적용한 후, 다음 두 가지 유형에 대해 설정을 정의할 수 있다.

${\displaystyle T=\{v\in D\mid \P_{T}(v)\}}}$

${\displaystyle S=\{v\in D\mid \P_{T}(v){\text{ 및 }P_{s}(v)\}}}$

술어 $T{\displaystyle \mathbf{}}$= ${\displaystyle {}_{}}$ ${\displaystyle T_{}}$ ${\$= $P_{$복합 술어 S 정의 S의 일부로$$ T$}$을(를) P ${\$와 함께 적용한다$$.두 술어는 결합되어 있으므로 값을 선택하려면 둘 다 참이어야 한다.술어 $S{\displaystyle \mathbf{}}$= ${\displaystyle T\mathbf{}}$ ${\displaystyle \wedge }$ ${\displaystyle {}_{}}$ ${\displaystyle s_{}}$= ${\displaystyle {}_{}}$ ${\displaystyle T_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle s_{}}$ ${\${$s}=P_{T}\land P_s}}}$는 술어 T를 소급하므로 S <: T.

예를 들어 고양이과 펠리네라고 불리는 고양이과 하위과가 있는데, 펠리네과는 펠리네과에 속한다.국내 고양이 종인 Felis catus가 속한 Felis 속은 그 하위과에 속한다.

${\displaystyle {\mathit {Felinae=\{cat\in Felie\mid \ of Subfamily(cat,felinaeSubfamilyName)\}}}}$

${\displaystyle {felis=\{cat\in Felinae\mid \ ofGenus(cat,felisGenusName)\\}}}}$

여기서 술어의 결합은 첫 번째 술어에 적합한 값의 영역에 대한 두 번째 술어의 적용을 통해 표현되었다.유형으로 보면 펠리스 <: 펠리네 <: 펠리네 <: 펠리과

만일 TSsubsumes s∈ T{\displaystyle s\in T}(T:>S) 다음 절차, 기능이나 표현 그래서 가치에 대한 하나의 형식 T로 운용할 수 있을 것입니다. S{\displaystyles\in S}∈ 피연산자(입력 인수 또는 용어)로 값이 주어진 위의 예에서, 우리는 기능 ofSubfamily가 되applicab 예상할 수 있다.르3종류의 펠리네, 펠리네, 펠리스의 가치에 대한 값을 모두 매긴다.

하위 형식 구성표

형식 이론가들은 특정한 방식으로 선언된 형식만 서로 하위 유형일 수 있는 명목상의 하위 유형과 두 유형의 구조가 다른 유형의 하위 유형인지 아닌지를 결정하는 구조 하위 유형을 구별한다.위에서 설명한 클래스 기반의 객체 지향 서브타이핑은 명목상이다. 객체 지향 언어에 대한 구조적인 서브타이핑 규칙은 타입 A의 물체가 B 유형의 물체가 처리할 수 있는 모든 메시지(즉, 모든 동일한 방법을 정의한다면)를 처리할 수 있다면, A는 어느 쪽이든 t에서 상속되는지 여부에 관계없이 B의 하위 유형이라고 말할 수 있다.다른 사람소위 오리타입이라고 불리는 이 타이핑은 동적으로 타이핑된 객체 지향 언어에서 흔히 볼 수 있다.객체 유형 이외의 유형에 대한 건전한 구조 하위 유형 규칙도 잘 알려져 있다.^{[citation needed]}

서브타이핑을 사용하는 프로그래밍 언어의 구현은 두 가지 일반 세분류로 분류된다: A형의 어떤 가치의 표현도 A형의 <: B의 경우 B형의 동일한 가치를 나타내는 포괄적 구현과 A형의 값이 B형의 하나로 자동 변환될 수 있는 강압적 구현이다.객체 지향 언어로 하위 분류하여 유도하는 서브타이핑은 대개 포함되며, 상이하게 표현되는 정수 및 부동 소수점 관련 서브타이핑 관계는 대개 강압적이다.

서브타이핑 관계를 정의하는 거의 모든 유형 시스템에서 그것은 반사적(A <: A 형식에 대해 A를 의미)이고 타동적(A <: B와 B <: C를 의미하면 A <: C를 의미함)이다.이것은 형식에 대한 사전 주문으로 만든다.

기록유형

폭 및 깊이 하위 유형

기록의 종류는 폭과 깊이 하위타입의 개념을 낳는다.이는 원래 레코드 유형과 동일한 작업을 수행할 수 있는 새로운 유형의 레코드를 획득하는 두 가지 다른 방법을 표현한다.

레코드가 (이름) 필드의 모음임을 상기하십시오.서브타입은 원래 타입에서 허용된 모든 연산을 허용하는 타입이므로, 레코드 서브타입은 지원되는 타입과 필드에서 동일한 연산을 지원해야 한다.

이러한 지원을 얻기 위한 방법 중 하나인 width subtyping은 기록에 더 많은 필드를 추가한다.보다 형식적으로 width supertype에 나타나는 모든 (이름) 필드가 width subtype에 나타난다.따라서 슈퍼타입에서 실현 가능한 모든 작동은 서브타입에 의해 지원될 것이다.

두 번째 방법은 깊이 하위 유형이라고 하며, 다양한 필드를 하위 유형으로 대체한다.즉, 서브타입의 필드는 슈퍼타입의 필드의 하위타입이다.슈퍼타입의 필드에 대해 지원되는 조작은 그 서브타입에 대해 지원되므로, 레코드 슈퍼타입에서 실현 가능한 조작은 레코드 서브타입에 의해 지원된다.깊이 하위타입은 불변의 기록에만 의미가 있다. 예를 들어 1.5를 실제 지점의 'x' 필드(실제 필드가 두 개인 레코드)에 할당할 수 있지만 1.5는 정수가 아니기 때문에 정수 지점의 'x' 필드(단, 실제 지점 유형의 깊은 하위 유형임)에는 동일하게 할 수 없다(분산 참조).

기록의 서브타이핑은 파라메트릭 다형성과 기록 유형의 서브타이핑을 결합한 시스템 F에서_<: 정의될 수 있으며, 두 가지 특징을 모두 지원하는 많은 기능 프로그래밍 언어의 이론적 근거가 된다.

일부 시스템은 라벨이 부착된 분리 결합 유형(대수 데이터 유형 등)의 하위 유형도 지원한다.width subtype에 나타나는 모든 태그는 width supertype에 나타나야 한다.

함수형식

T₁ → T가₂ 함수형이라면, 그것의 하위형은 T₁ <: S와₁ S₂ <: T₂>라는 속성을 가진 어떤 함수형₁ S → S이다₂.이는 다음과 같은 타이핑 규칙을 사용하여 요약할 수 있다.

${\displaystyle T_{1}\leq :S_{1}\quad S_{2}\leq :T_{2} \over S_{1}\오른쪽 화살표 S_{2}\leq :T_{1}\오른쪽 화살표 T_{2}}$

S₁ → S의₂ 주장형은 그에 대해 하위형태가 역전되는 반면, 반환형은 공변량이기 때문에 대립된다고 한다.비공식적으로, 이러한 반전은 정제된 타입이 그것이 받아들이는 타입에서는 "더 자유주의"이고 반환되는 타입에서는 "더 보수적"이기 때문에 발생한다.This is what exactly works in Scala: a n-ary function is internally a class that inherits the ${\displaystyle {\mathtt {Function_{N}(-A_{1},-A_{2},\dots ,-A_{n},+B)}}}$trait (which can be seen as a general interface in Java-like languages), where ${\displaystyle {\mathtt{A}}_{\mathtt{1}}\mathtt{,}{\mathtt{A}}_{\mathtt{2}}}$${\displaystyle {}_{},{n\mathtt{}}_{}}$ ${\$이(가) 매개 변수 유형이며$$,B는 반환형이다. "-"는 형식이 어긋난다는 의미인 반면 "+"는 공변량을 의미한다.

대부분의 객체 지향 언어와 마찬가지로 부작용을 허용하는 언어에서 하위 타이핑은 일반적으로 기능이 다른 언어의 맥락에서 안전하게 사용될 수 있다는 것을 보장하기에 충분하지 않다.이 분야에서 리스크노프의 작업은 행동적 서브타이핑에 초점을 맞췄는데, 이 글에서 논의된 타입 시스템 안전성 이외에도 서브타입은 어떤 계약에서 슈퍼타입에 의해 보장된 모든 불변성을 보존할 것을 요구한다.^[5]이러한 서브타이핑의 정의는 일반적으로 판독할 수 없으므로 형식 검사기로 확인할 수 없다.

변이 가능한 참조의 하위 형식은 함수 인수 및 반환 값의 처리와 유사하다.쓰기 전용 참조(또는 싱크)는 함수 인수와 같이 반대방향이고 읽기 전용 참조(또는 소스)는 반환 값과 같은 공변량이다.출처와 싱크대 역할을 하는 변이성 언급은 불변하다.

상속관계

서브타이핑과 상속은 독립적(직교적) 관계다.그들은 일치할지도 모르지만, 어느 것도 다른 특별한 경우는 아니다.즉, 두 가지 타입 S와 T 사이에 서브타이핑과 상속의 모든 조합이 가능하다.

1. S는 하위 유형도 아니고 파생 유형도 아니다.
2. S는 하위 유형이지만 T의 파생 유형이 아니다.
3. S는 하위 유형이 아니라 파생된 T 유형이다.
4. S는 T의 하위 유형이자 파생 유형이다.

첫 번째 사례는 다음과 같은 독립적인 유형으로 설명된다.Boolean그리고Float.

두 번째 사례는 다음의 관계에 의해 설명될 수 있다.Int32그리고Int64. 대부분의 객체 지향 프로그래밍 언어에서,Int64상속과 관계가 없다Int32그러나Int32의 하위 유형으로 간주할 수 있다.Int6432비트 정수 값은 64비트 정수 값으로 승격될 수 있기 때문이다.

세 번째 경우는 기능 하위 유형 입력 왜곡의 결과물이다.같은 유형의 물체를 반환하는 방법 m을 가진 T형식의 슈퍼클래스와 T형에서 파생된 S형이라고 가정한다(즉, m형은 T → T형이며, m의 첫 번째 인수는 이/자체라는 점에 유의한다).By inheritance, the type of m in S is S → S. In order for S to be a subtype of T the type of m in S must be a subtype of the type of m in T, in other words: S → S ≤: T → T. By bottom-up application of the function subtyping rule, this means: S ≤: T and T ≤: S, which is only possible if S and T are the same.상속은 불손한 관계인 만큼 S는 T의 아형이 될 수 없다.

서브타이핑과 상속은 모든 상속된 필드 및 파생된 형식의 메서드가 해당 필드의 하위 유형인 유형과 상속된 유형으로부터 메서드를 가질 때 호환된다.^[2]

강제력

강압적인 서브타이핑 시스템에서 서브타입은 서브타입에서 슈퍼타입으로의 암묵적 타입 변환 함수에 의해 정의된다.각 서브타이핑 관계(S <: T)에 대해 강제함수 coerce: S → T가 제공되며, S 타입의 모든 객체 s는 T 타입의 객체 coerce로_{S → T} 간주된다.강제함수는 구성으로 정의될 수 있다: S <: T와 T <: U>인 경우 s는 복합강제(coerce_{T → U} co coerce_{S → T})에 따른 u형식의 대상으로 간주될 수 있다.유형에서 그 자체로_{T → T} 강요하는 타입의 강제성은 ID 함수 ID이다_T.

기록과 분리 결합 하위 유형의 강제 함수는 구성요소에 따라 정의될 수 있다. 폭 확장 기록의 경우, 형식 강제성은 단지 슈퍼타입에 정의되지 않은 구성요소를 배제한다.함수 유형의 형식 강제성은 함수 인수의 왜곡과 반환 값의 공분산을 반영하여 f's(s) = coerce_{S2 → T2}(f(coerce_{T1 → S1}(t)))로 지정할 수 있다.

강제함수는 하위형과 슈퍼타입에 따라 고유하게 결정된다.그러므로 복수의 서브타이핑 관계가 정의될 때, 모든 타입의 강제성이 일관성을 보장하도록 주의해야 한다.예를 들어, 2 : int와 같은 정수를 부동 소수점 번호(예: 2.0 : float)로 강제할 수 있다면 2.1 : 2 : int로 float하는 것은 허용되지 않는다. 왜냐하면 coerce_{int → float} ∘ coerce가_{float → int} 제공하는 복합강제 coerce는_{float → float} 신분강제 id와_float 구별되기 때문이다.

참고 항목

위키북 에이다 프로그래밍에는 다음과 같은 주제의 페이지가 있다: 하위 유형

• 공분산 및 왜곡
• 원-엘리프 문제(값 유형과 동일한 기준으로 변수 유형의 위험)
• 클래스 기반 프로그래밍
• 탑타입
• 정제형
• 행동하위태핑

메모들

참조

교과서

페이퍼스

추가 읽기