짧은 대답은 “기존 코드의 추가 속성을 확인하는 것”입니다. 더 긴 대답은 다음과 같습니다.

“암시 적”대 “명시 적”이라는 용어가 좋은 용어인지 잘 모르겠습니다. 이 구분을 “구조적”대 “명 목적”하위 유형이라고도합니다. 그런 다음 구조적 서브 타이핑의 가능한 해석에 두 번째 차이점이 있습니다 (곧 설명). 서브 타이핑에 대한 세 가지 해석은 모두 직교이므로 각각의 사용법을 이해하기보다는 서로 비교하는 것이 의미가 없습니다.

구조적 서브 타이핑 관계 A <: B를 해석 할 때의 주요 운영상의 차이점은 (런타임 / 컴파일 타임) 계산 내용으로 실제 강요에 의해 목격되는지 또는 동일성 강요에 의해 목격 될 수 있는지 여부입니다. 전자의 경우 중요한 이론적 속성이 “일관성”인 경우, 즉 A가 B의 하위 구조적 하위 유형임을 나타내는 여러 가지 방법이있는 경우, 수반되는 각 강제 변환은 동일한 계산 내용을 가져야합니다.

당신이 준 링크는 구조적 서브 타입의 두 번째 해석을 염두에 둔 것으로 보입니다. 여기서 A <: B는 정체성 강요에 의해 목격 될 수 있습니다. 이것을 서브 타이핑의 “서브 세트 해석”이라고도하며, 타입이 값 세트를 나타낸다는 순진한 견해를 취하기 때문에 A <: B는 A 타입의 모든 값이 B 타입의 값일 경우를 대비합니다. “refinement typing”이라고도하며 원래 동기 부여를위한 좋은 논문 은 ML에 대한 Freeman & Pfenning의 Refinement 유형입니다 . F #의 최신 화신에 대해서는 안전한 구현을위한 Bengston et al, Refinement 유형을 읽을 수 있습니다.. 기본 개념은 이미 유형을 가지고 있거나 그렇지 않을 수도 있지만 유형이 그다지 많은 것을 보장하지 않는 (예를 들어, 메모리 안전성 만) 존재하는 기존 프로그래밍 언어를 사용하여 프로그램의 하위 집합을 선택하는 두 번째 유형의 계층을 고려하는 것입니다 더 정확한 추가 속성.

(이제 서브 타이핑에 대한이 해석의 수학적 이론은 여전히 ​​이해해야 할만큼 잘 이해되지 않았으며, 아마도 그것의 사용이 예상만큼 널리 인식되지 않았기 때문일 것입니다. 한 가지 문제는 유형에 대한 해석이 너무 순진하기 때문에 때로는 세련되지 않고 포기되기도합니다. 하위 유형 지정에 대한 이러한 해석이 더 많은 수학적주의를 기울여야한다는 또 다른 주장 은 Abstract Stone Duality 의 Paul Taylor의 하위 공간 소개를 읽어보십시오 .)

답변