프로그래밍 언어 이론에서 서브타이핑은 유형 다형성의 한 형태이다. 서브타입(subtype)은 대체 가능성 개념에 의해 다른 데이터 유형(수퍼 유형)과 관련된 데이터 유형이다. 즉, 상위 유형의 요소에서 작동하도록 작성된 프로그램 요소(일반적으로 서브루틴 또는 함수)가 서브타입의 요소에서도 작동할 수 있다는 의미이다.

S가 T의 서브타입인 경우 서브타이핑 관계(S <: T, S ⊑ T^[1] 또는 S ≤: T로 작성됨)는 유형 S의 모든 용어가 유형 T의 용어가 다음과 같은 모든 컨텍스트에서 안전하게 사용될 수 있음을 의미한다. 예상되는. 여기서 서브타이핑의 정확한 의미는 주어진 유형 형식 또는 프로그래밍 언어에 의해 "안전하게 사용됨" 및 "모든 컨텍스트"가 어떻게 정의되는지에 따라 결정적으로 달라진다. 프로그래밍 언어의 유형 시스템은 본질적으로 자체 서브타이핑 관계를 정의한다. 이는 언어가 변환 메커니즘을 전혀(또는 거의) 지원하지 않는 경우 사소할 수 있다.

서브타이핑 관계로 인해 용어는 둘 이상의 유형에 속할 수 있다. 따라서 서브타이핑은 유형 다형성의 한 형태이다. 객체 지향 프로그래밍에서 '다형성'이라는 용어는 일반적으로 이러한 서브타입 다형성만을 지칭하는 데 사용되는 반면, 매개변수 다형성 기술은 일반 프로그래밍으로 간주된다.

함수형 프로그래밍 언어에서는 종종 레코드의 서브타이핑이 허용된다. 결과적으로, 레코드 유형으로 확장된 단순히 유형화된 람다 계산은 아마도 서브타이핑의 유용한 개념을 정의하고 연구할 수 있는 가장 간단한 이론적 설정일 것이다.^[2] 결과 계산에서는 용어가 두 개 이상의 유형을 가질 수 있으므로 더 이상 "단순" 유형 이론이 아니다. 함수형 프로그래밍 언어는 정의에 따라 레코드에도 저장될 수 있는 함수 리터럴을 지원하므로 서브타이핑이 있는 레코드 유형은 객체 지향 프로그래밍의 일부 기능을 제공한다. 일반적으로 함수형 프로그래밍 언어는 일반적으로 제한된 형태의 파라메트릭 다형성도 제공한다. 이론적 설정에서는 두 기능의 상호 작용을 연구하는 것이 바람직하다. 일반적인 이론적 설정은 시스템 F<:이다. 객체 지향 프로그래밍의 이론적 특성을 포착하려는 다양한 계산은 시스템 F<:에서 파생될 수 있다.

서브타이핑의 개념은 하위형(hyponymy) 및 신성형(holonymy)이라는 언어적 개념과 관련된다. 이는 수학적 논리의 제한된 수량화 개념과도 관련이 있다. 서브타이핑을 객체 지향 언어의 (클래스 또는 객체) 상속 개념과 혼동해서는 안 된다. 서브타이핑은 유형(객체 지향 용어로 인터페이스) 간의 관계인 반면 상속은 기존 객체에서 새 객체를 생성할 수 있도록 하는 언어 기능에서 비롯된 구현 간의 관계이다. 여러 객체 지향 언어에서 서브타이핑을 인터페이스 상속(interface inheritance)이라고 하며 상속을 구현 상속(implementation inheritance)이라고 한다.

• 공변성과 반공변성 (컴퓨터 과학)
• 클래스 기반 프로그래밍