ในทฤษฎีภาษาโปรแกรมการกำหนดชนิดย่อย (หรือเรียกว่าโพลีมอร์ฟิซึมชนิดย่อยหรือ โพลีมอร์ ฟิซึมการรวม ) เป็นรูปแบบหนึ่งของ โพ ลีมอร์ฟิซึมชนิด ข้อมูล ชนิดย่อยคือชนิดข้อมูลที่เกี่ยวข้องกับชนิดข้อมูลอื่น ( ชนิดข้อมูลหลัก ) โดยแนวคิดเรื่องความสามารถในการทดแทนกันหมายความว่าองค์ประกอบของโปรแกรม (โดยทั่วไปคือรูทีนย่อยหรือฟังก์ชัน) ที่เขียนขึ้นเพื่อทำงานกับองค์ประกอบของชนิดข้อมูลหลัก สามารถทำงานกับองค์ประกอบของชนิดย่อยได้เช่นกัน

ถ้า S เป็นชนิดย่อยของ T ความสัมพันธ์ ของชนิดย่อย (เขียนเป็นS <: T ,   S ⊑ T , ^{[ 1 ]}หรือ   S ≤: T  ) หมายความว่าเทอมใดๆ ของชนิด S สามารถใช้ได้อย่างปลอดภัยในบริบทใดๆที่คาดหวังเทอมของชนิด T ความหมายที่แม่นยำของความสัมพันธ์ของชนิดย่อยในที่นี้ขึ้นอยู่กับรายละเอียดของวิธีการกำหนด"สามารถใช้ได้อย่างปลอดภัย"และ"บริบทใดๆ" โดย รูปแบบชนิดหรือภาษาโปรแกรมที่กำหนดระบบชนิดของภาษาโปรแกรมโดยพื้นฐานแล้วกำหนดความสัมพันธ์ของชนิดย่อยของตัวเอง ซึ่งอาจเป็นเรื่องง่ายๆหากภาษานั้นไม่รองรับ (หรือมีน้อยมาก) กลไกการแปลง

เนื่องจากความสัมพันธ์แบบซับไทป์ เทอมหนึ่งอาจเป็นของประเภทมากกว่าหนึ่งประเภทได้ ดังนั้น ซับไทป์จึงเป็นรูปแบบหนึ่งของโพลีมอร์ฟิซึมของประเภท ในการเขียนโปรแกรมเชิงวัตถุคำว่า 'โพลีมอร์ฟิซึม' มักใช้เพื่ออ้างถึงโพลีมอร์ฟิซึมแบบซับไทป์ นี้เท่านั้น ในขณะที่เทคนิคของโพลีมอร์ฟิซึมแบบพารามิเตอร์จะถูกพิจารณาว่าเป็นโปรแกรมเชิงเจเนริก

ภาษาการเขียนโปรแกรมเชิงฟังก์ชันมักอนุญาตให้มีการกำหนดประเภทย่อยของเรคอร์ดดังนั้นแคลคูลัสแลมบ์ดาแบบกำหนดประเภทอย่างง่ายที่ขยายด้วยประเภทเรคอร์ดจึงอาจเป็นการตั้งค่าทางทฤษฎีที่ง่ายที่สุดในการกำหนดและศึกษาแนวคิดที่มีประโยชน์ของการกำหนดประเภทย่อย^{[ 2 ]}เนื่องจากแคลคูลัสที่ได้อนุญาตให้เทอมมีประเภทมากกว่าหนึ่งประเภท จึงไม่ใช่ทฤษฎีประเภท "ง่าย" อีกต่อไป เนื่องจากภาษาการเขียนโปรแกรมเชิงฟังก์ชันตามคำจำกัดความรองรับตัวอักษรฟังก์ชันซึ่งสามารถจัดเก็บไว้ในเรคอร์ดได้เช่นกัน ประเภทเรคอร์ดที่มีการกำหนดประเภทย่อยจึงให้คุณสมบัติบางอย่างของการเขียนโปรแกรมเชิงวัตถุ โดยทั่วไป ภาษาการเขียนโปรแกรมเชิงฟังก์ชันยังให้รูปแบบของการพหุรูปพารามิเตอร์ที่จำกัด ในการตั้งค่าทางทฤษฎี การศึกษาปฏิสัมพันธ์ของคุณสมบัติทั้งสองเป็นสิ่งที่พึงปรารถนา การตั้งค่าทางทฤษฎีทั่วไปคือระบบ F _<:แคลคูลัสต่างๆ ที่พยายามจับคุณสมบัติทางทฤษฎีของการเขียนโปรแกรมเชิงวัตถุอาจได้มาจากระบบ F _< :

แนวคิดของการกำหนดชนิดย่อยมีความเกี่ยวข้องกับแนวคิดทางภาษาศาสตร์ของhyponymyและholonymyนอกจากนี้ยังเกี่ยวข้องกับแนวคิดของการกำหนดปริมาณแบบจำกัดในตรรกะทางคณิตศาสตร์ (ดูตรรกะเรียงลำดับ ) การกำหนดชนิดย่อยไม่ควรสับสนกับแนวคิดของการสืบทอด (คลาสหรือวัตถุ) จากภาษาเชิงวัตถุ^{[ 3 ]}การกำหนดชนิดย่อยเป็นความสัมพันธ์ระหว่างชนิด (อินเทอร์เฟซในภาษาเชิงวัตถุ) ในขณะที่การสืบทอดเป็นความสัมพันธ์ระหว่างการใช้งานที่เกิดจากคุณลักษณะของภาษาที่อนุญาตให้สร้างวัตถุใหม่จากวัตถุที่มีอยู่ ในภาษาเชิงวัตถุจำนวนหนึ่ง การกำหนดชนิดย่อยเรียกว่าการสืบทอดอินเทอร์เฟซโดยการสืบทอดเรียกว่าการสืบทอดการใช้งาน

แนวคิดเรื่องการกำหนดประเภทย่อยในภาษาโปรแกรมมีมาตั้งแต่ทศวรรษ 1960 โดยได้รับการแนะนำในภาษา ที่พัฒนามาจาก Simulaการวิเคราะห์การกำหนดประเภทย่อยอย่างเป็นทางการครั้งแรกเกิดขึ้นโดยJohn C. Reynoldsในปี 1980 ซึ่งใช้ทฤษฎีหมวดหมู่ในการกำหนดรูปแบบการแปลงโดยปริยายอย่าง เป็นทางการ และLuca Cardelli (1985) ^{[ 4 ]}

แนวคิดเรื่องการกำหนดชนิดย่อย (subtyping) ได้รับความสนใจมากขึ้น (และมีความหมายเหมือนกับ polymorphism ในบางแวดวง) เนื่องจากการนำการเขียนโปรแกรมเชิงวัตถุมาใช้กันอย่างแพร่หลาย ในบริบทนี้ หลักการทดแทนที่ปลอดภัย (safe substitution) มักถูกเรียกว่า หลักการทดแทนของลิสคอฟ (Liskov substitution principle ) ตาม ชื่อของ บาร์บารา ลิสคอฟผู้ทำให้หลักการนี้เป็นที่นิยมใน ปาฐกถา หลักในการประชุมเกี่ยวกับการเขียนโปรแกรมเชิงวัตถุในปี 1987 เนื่องจากต้องพิจารณาวัตถุที่เปลี่ยนแปลงได้ แนวคิดในอุดมคติของการกำหนดชนิดย่อยที่กำหนดโดยลิสคอฟและฌองเน็ตต์ วิงซึ่งเรียกว่า การกำหนดชนิดย่อยเชิงพฤติกรรม ( behavioral subtyping ) จึงมีความแข็งแกร่งกว่าสิ่งที่สามารถนำไปใช้ใน ตัวตรวจสอบชนิด (type checker ) ได้มาก(ดู รายละเอียดเพิ่มเติมในหัวข้อ § ชนิดฟังก์ชันด้านล่าง)

แผนภาพแสดงตัวอย่างง่ายๆ ในทางปฏิบัติของชนิดย่อย ชนิด "นก" มีชนิดย่อยสามชนิด ได้แก่ "เป็ด" "นกคuckoo" และ "นกกระจอกเทศ" ในเชิงแนวคิดแล้ว แต่ละชนิดย่อยเหล่านี้เป็นสายพันธุ์หนึ่งของชนิดพื้นฐาน "นก" ที่สืบทอดลักษณะหลายอย่างของ "นก" แต่ก็มีความแตกต่างเฉพาะบางประการ แผนภาพนี้ใช้สัญลักษณ์ UMLโดยลูกศรหัวเปิดแสดงทิศทางและประเภทของความสัมพันธ์ระหว่างชนิดหลักและชนิดย่อย

ตัวอย่างที่เป็นรูปธรรมมากขึ้นคือ ภาษาอาจอนุญาตให้ใช้ค่าจำนวนเต็มได้ทุกที่ที่คาดหวังค่าทศนิยม ( Integer<: Float) หรืออาจกำหนดประเภททั่วไปขึ้นมาตัวเลขในฐานะที่เป็นซูเปอร์ไทป์ทั่วไปของจำนวนเต็มและจำนวนจริง ในกรณีที่สองนี้ เรามีเพียงInteger<: NumberและFloat<: Numberเท่านั้น แต่IntegerและFloatไม่ใช่ซับไทป์ของกันและกัน

โปรแกรมเมอร์อาจใช้ประโยชน์จากการกำหนดชนิดย่อย (subtyping) เพื่อเขียนโค้ดในลักษณะที่เป็นนามธรรมมากขึ้นกว่าที่เคยเป็นไปได้หากไม่มีการกำหนดชนิดย่อย ลองพิจารณาตัวอย่างต่อไปนี้:

ฟังก์ชันmax ( x as Number , y as Number ) คือถ้าx < y ให้คืนค่าy มิฉะนั้นให้คืนค่าx

ถ้าจำนวนเต็มและจำนวนจริงเป็นชนิดย่อยของNumberและมีการกำหนดตัวดำเนินการเปรียบเทียบกับจำนวนใดๆ สำหรับทั้งสองชนิดแล้ว ค่าของชนิดใดชนิดหนึ่งสามารถส่งผ่านไปยังฟังก์ชันนี้ได้ อย่างไรก็ตาม ความเป็นไปได้ในการใช้งานตัวดำเนินการดังกล่าวจำกัดชนิดของจำนวนอย่างมาก (ตัวอย่างเช่น ไม่สามารถเปรียบเทียบจำนวนเต็มกับจำนวนเชิงซ้อนได้) และในความเป็นจริง การเปรียบเทียบเฉพาะจำนวนเต็มกับจำนวนเต็ม และจำนวนจริงกับจำนวนจริงเท่านั้นจึงจะสมเหตุสมผล การเขียนฟังก์ชันนี้ใหม่เพื่อให้รับเฉพาะ 'x' และ 'y' ที่มีชนิดเดียวกันเท่านั้น จำเป็นต้องใช้ โพลีมอ ร์ ฟิซึมแบบจำกัด

การกำหนดชนิดย่อย (Subtyping) ช่วยให้สามารถใช้ชนิดข้อมูลหนึ่งแทนชนิดข้อมูลหรือนามธรรมอื่นได้ กล่าวได้ว่าการกำหนดชนิดย่อยเป็นการสร้าง ความสัมพันธ์ แบบ "เป็น" (is-a)ระหว่างชนิดย่อยกับนามธรรมที่มีอยู่แล้ว ไม่ว่าจะโดยปริยายหรือโดยชัดแจ้ง ขึ้นอยู่กับการรองรับของภาษา ความสัมพันธ์นี้สามารถแสดงออกมาอย่างชัดเจนได้ผ่านการสืบทอด (Inheritance) ในภาษาที่รองรับการสืบทอดเป็นกลไกการกำหนดชนิดย่อย

โค้ด C++ ต่อไปนี้สร้างความสัมพันธ์การสืบทอดแบบชัดเจนระหว่างคลาสBและAโดยที่Bเป็นทั้งคลาสย่อยและชนิดย่อยของAและสามารถใช้แทนA ได้ ทุกที่ที่ มีการระบุ B (ผ่านการอ้างอิง ตัวชี้ หรือตัววัตถุเอง)

คลาสA { public : void methodOfA () const { // ... } };คลาสB : สาธารณะA { สาธารณะ: void methodOfB () const { // ... } };void functionOnA ( const A & a ) { a . methodOfA (); }int main () { B b ; functionOnA ( b ); // สามารถแทนที่ b ด้วย A ได้}

^{[ 5 ]}

โค้ด Python ต่อไปนี้สร้างความสัมพันธ์การสืบทอดแบบชัดเจนระหว่างคลาสBและAโดยที่Bเป็นทั้งคลาสย่อยและชนิดย่อยของAและสามารถใช้แทนA ได้ ทุกที่ที่ต้องการใช้ B

คลาสA : def method_of_a ( self ) -> None : passคลาสB ( A ): def method_of_b ( self ) -> None : passdef function_on_a ( a : A ) -> None : a . method_of_a ()ถ้า__name__ == "__main__" : b : B = B () function_on_a ( b ) # b สามารถแทนที่ด้วย A ได้

ตัวอย่างต่อไปนี้type(a)เป็นประเภท "ปกติ" และtype(type(a))เป็นเมตาไทป์ ในขณะที่ประเภทที่กระจายทั้งหมดจะมีเมตาไทป์เดียวกัน ( PyType_Typeซึ่งเป็นเมตาไทป์ของตัวเองด้วย) แต่นี่ไม่ใช่ข้อกำหนด ประเภทของคลาสแบบคลาสสิกที่เรียกว่าtypes.ClassTypeก็สามารถถือเป็นเมตาไทป์ที่แตกต่างกันได้เช่นกัน^{[ 6 ]}

a = 0 print(type(a)) # พิมพ์: <type 'int'> print(type(type(a))) # พิมพ์: <type 'type'> print(type(type(type(a)))) # พิมพ์: <type 'type'> print(type(type(type(type(a))))) # พิมพ์: <type 'type'>

ในภาษา Java ความสัมพันธ์ระหว่างพารามิเตอร์ประเภทของคลาสหรืออินเทอร์เฟซหนึ่งกับพารามิเตอร์ประเภทของอีกคลาสหรืออินเทอร์เฟซหนึ่ง จะถูกกำหนดโดยข้อความ extends และ implements

โดยใช้CollectionsคลาสArrayList<E>implements List<E>และList<E>extends Collection<E>ดังนั้น จึงArrayList<String>เป็นซับไทป์ของList<String>ซึ่งเป็นซับไทป์ของCollection<String>ความสัมพันธ์แบบซับไทป์จะถูกรักษาไว้ระหว่างประเภทโดยอัตโนมัติ เมื่อกำหนดอินเทอร์เฟซPayloadListที่เชื่อมโยงค่าเสริมของประเภททั่วไป P กับแต่ละองค์ประกอบ การประกาศอาจมีลักษณะดังนี้:

interface PayloadList < E , P > extends List < E > { void setPayload ( int index , P val ); ... }

การกำหนดพารามิเตอร์ต่อไปนี้ของ PayloadList เป็นชนิดย่อยของList<String>:

PayloadList < String , String > PayloadList < String , Integer > PayloadList < String , Exception >

ในทฤษฎีประเภท แนวคิดของการครอบคลุม^{[ 7 ]} ใช้เพื่อกำหนดหรือประเมินว่าประเภทSเป็นประเภทย่อยของประเภทT หรือ ไม่

ประเภท (Type) คือเซตของค่าต่างๆ เซตนี้สามารถอธิบายได้ในเชิงขยาย (extensively)โดยการระบุค่าทั้งหมด หรือสามารถอธิบายได้ ในเชิงความหมาย (intensionally)โดยการระบุการเป็นสมาชิกของเซตโดยใช้述语 (predicate) บนโดเมนของค่าที่เป็นไปได้ ในภาษาโปรแกรมทั่วไป ประเภทการแจงนับ (enumeration types) จะถูกกำหนดในเชิงขยายโดยการระบุค่าต่างๆส่วนประเภทที่ผู้ใช้กำหนดเองเช่น เรคอร์ด (structs, interfaces) หรือคลาส จะถูกกำหนดในเชิงความหมายโดยการประกาศประเภทอย่างชัดเจน หรือโดยการใช้ค่าที่มีอยู่แล้ว ซึ่งเข้ารหัสข้อมูลประเภท เป็นต้นแบบที่จะคัดลอกหรือขยายเพิ่มเติม

ในการอธิบายแนวคิดเรื่องการครอบคลุม (subsumption) เซตของค่าของชนิดข้อมูลหนึ่งจะถูกระบุโดยการเขียนชื่อของชนิดข้อมูลนั้นด้วยตัวเอียงทางคณิตศาสตร์: Tส่วนชนิดข้อมูลนั้น เมื่อมองในแง่ของภาคแสดง (predicate) บนโดเมน จะถูกระบุโดยการเขียนชื่อของชนิดข้อมูลนั้นด้วยตัวหนา: Tสัญลักษณ์ทั่วไป<:หมายถึง "เป็นชนิดย่อยของ" และ:>หมายถึง "เป็นชนิดหลักของ"

• ประเภทT ครอบคลุม ประเภท S ก็ต่อ เมื่อเซตของค่าTที่มันกำหนดขึ้น เป็นซูเปอร์เซตของเซตSกล่าวคือ สมาชิกทุกตัวของSเป็นสมาชิกของT ด้วยเช่น กัน
• ประเภทหนึ่งอาจถูกรวมเข้ากับประเภท อื่นได้มากกว่าหนึ่งประเภท: ประเภทหลักของSจะตัดกันที่S
• ถ้าS < T (และดังนั้นS ⊆ T ) แล้วTซึ่งเป็น述语ที่ล้อมรอบเซตTจะต้องเป็นส่วนหนึ่งของ述语S (บนโดเมนเดียวกัน) ซึ่งกำหนดS
• ถ้าSครอบคลุมTและTครอบคลุมSแล้ว ประเภททั้งสองจะเท่ากัน (ถึงแม้ว่าอาจจะไม่ใช่ประเภทเดียวกันก็ได้ หากระบบประเภทแยกแยะประเภทตามชื่อ)

ในแง่ของความเฉพาะเจาะจงของข้อมูล ประเภทย่อยจะถือว่ามีความเฉพาะเจาะจงมากกว่าประเภทหลักใดๆ เนื่องจากมีข้อมูลอย่างน้อยเท่ากับประเภทหลักแต่ละประเภท ซึ่งอาจเพิ่มความสามารถในการใช้งานหรือความเกี่ยวข้องของประเภทย่อย (จำนวนสถานการณ์ที่สามารถยอมรับหรือนำไปใช้ได้) เมื่อเทียบกับประเภทหลักที่ "ทั่วไปกว่า" ข้อเสียของการมีข้อมูลที่ละเอียดกว่านี้คือ มันแสดงถึงทางเลือกที่ถูกรวมไว้ ซึ่งลดความแพร่หลายของประเภทย่อย (จำนวนสถานการณ์ที่สามารถสร้างหรือก่อให้เกิดประเภทย่อยนั้นได้)

ในบริบทของการครอบคลุม (subsumption) นิยามประเภทสามารถแสดงได้โดยใช้ สัญกร ณ์การสร้างเซต (Set-builder notation ) ซึ่งใช้述语 (predicate) ในการกำหนดเซต 述语สามารถกำหนดได้บนโดเมน (เซตของค่าที่เป็นไปได้) D述语เป็นฟังก์ชันบางส่วนที่เปรียบเทียบค่ากับเกณฑ์การเลือก ตัวอย่างเช่น: "ค่าจำนวนเต็มมากกว่าหรือเท่ากับ 100 และน้อยกว่า 200 หรือไม่?" ถ้าค่าตรงกับเกณฑ์ ฟังก์ชันจะส่งคืนค่า ถ้าไม่ตรง ค่าจะไม่ถูกเลือก และจะไม่ส่งคืนอะไรเลย (List comprehensions เป็นรูปแบบหนึ่งของรูปแบบนี้ที่ใช้ในภาษาโปรแกรมหลายภาษา)

หากมีเงื่อนไขสองเงื่อนไข เงื่อนไขหนึ่งใช้เกณฑ์การเลือกสำหรับประเภทTและอีกเงื่อนไขหนึ่งใช้เกณฑ์เพิ่มเติมสำหรับประเภทSแล้ว สามารถกำหนดเซตสำหรับทั้งสองประเภทได้: ${\displaystyle P_{T}}$${\displaystyle P_{s}}$

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

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

述语 (predicate) ถูกนำมาใช้ร่วมกับ述语เชิงประกอบSที่กำหนดS述语ทั้งสองเชื่อมโยงกันดังนั้นทั้งสองต้องเป็นจริงจึงจะสามารถเลือกค่าได้ 述语นี้ครอบคลุม述语Tดังนั้นS <: T${\displaystyle \mathbf {T} =P_{T}}$${\displaystyle P_{s}}$${\displaystyle \mathbf {S} =\mathbf {T} \land P_{s}=P_{T}\land P_{s}}$

ตัวอย่างเช่น มีวงศ์ย่อยของแมวชนิดหนึ่งที่เรียกว่าFelinaeซึ่งเป็นส่วนหนึ่งของวงศ์FelidaeสกุลFelisซึ่งเป็นสกุลของแมวบ้านชนิดFelis catusก็เป็นส่วนหนึ่งของวงศ์ย่อยนั้น

${\displaystyle {\mathit {Felinae=\{cat\in Felidae\mid \ ofSubfamily(cat,felinaeSubfamilyName)\}}}}$

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

การเชื่อมโยงของภาคแสดงได้ถูกแสดงออกมาในที่นี้โดยการประยุกต์ใช้ภาคแสดงที่สองกับโดเมนของค่าที่สอดคล้องกับภาคแสดงแรก เมื่อมองในแง่ของประเภท จะได้ว่าFelis <: Felinae <: Felidae

ถ้าTครอบคลุมS ( T :> S ) แล้ว ขั้นตอน ฟังก์ชัน หรือนิพจน์ที่รับค่าเป็นตัวดำเนินการ (ค่าพารามิเตอร์หรือเทอม) จะสามารถดำเนินการกับค่านั้นได้เหมือนกับค่าประเภทTเพราะในตัวอย่างข้างต้น เราคาดว่าฟังก์ชันofSubfamilyจะสามารถใช้ได้กับค่าทั้งสามประเภทได้แก่ Felidae , FelinaeและFelis${\displaystyle s\in S}$${\displaystyle s\in T}$

นักทฤษฎีประเภทแยกความแตกต่างระหว่างการกำหนดประเภทแบบนาม (nominal subtyping ) ซึ่งประเภทที่ประกาศในลักษณะใดลักษณะหนึ่งเท่านั้นที่จะเป็นประเภทย่อยของกันและกันได้ และการกำหนดประเภทแบบโครงสร้าง (structural subtyping ) ซึ่งโครงสร้างของสองประเภทจะเป็นตัวกำหนดว่าประเภทหนึ่งเป็นประเภทย่อยของอีกประเภทหนึ่งหรือไม่ การกำหนดประเภทแบบคลาสในภาษาเชิงวัตถุที่อธิบายไว้ข้างต้นเป็นการกำหนดประเภทแบบนาม กฎการกำหนดประเภทแบบโครงสร้างสำหรับภาษาเชิงวัตถุอาจกล่าวว่า หากวัตถุประเภทAสามารถจัดการข้อความทั้งหมดที่วัตถุประเภทB สามารถจัดการได้ (นั่นคือ หากพวกมันกำหนด เมธอดเดียวกันทั้งหมด) แล้วAจะเป็นประเภทย่อยของBโดยไม่คำนึงว่าประเภทใดจะสืบทอดจากอีกประเภทหนึ่ง หรือไม่ การกำหนดประเภทแบบเป็ด (duck typing ) นี้ พบได้ทั่วไปในภาษาเชิงวัตถุแบบไดนามิก กฎการกำหนดประเภทแบบโครงสร้างที่ถูกต้องสำหรับประเภทอื่นนอกเหนือจากประเภทวัตถุก็เป็นที่รู้จักกันดีเช่นกัน

การใช้งานภาษาโปรแกรมที่มีการกำหนดชนิดย่อยนั้นแบ่งออกเป็นสองประเภทหลักๆ คือ การใช้งาน แบบรวม (inclusive)ซึ่งการแสดงค่าใดๆ ของชนิดAจะแสดงค่าเดียวกันในชนิดB ได้เช่นกัน ถ้าA  <:  Bและ การใช้งาน แบบบังคับ (coercive)ซึ่งค่าของชนิดAสามารถแปลงเป็นค่าของชนิดB ได้โดยอัตโนมัติ การกำหนดชนิดย่อยที่เกิดจากการสร้างคลาสย่อยในภาษาเชิงวัตถุมักจะเป็นแบบรวม ส่วนความสัมพันธ์ของการกำหนดชนิดย่อยที่เชื่อมโยงจำนวนเต็มและจำนวนทศนิยม ซึ่งมีการแสดงค่าแตกต่างกัน มักจะเป็นแบบบังคับ

ในระบบประเภทข้อมูลเกือบทั้งหมดที่กำหนดความสัมพันธ์แบบซับไทป์ ความสัมพันธ์นั้นจะเป็นแบบสะท้อนกลับ (หมายความว่าA  <:  AสำหรับประเภทA ใดๆ ) และแบบถ่ายทอดได้ (หมายความว่า ถ้าA  <:  BและB  <:  Cแล้วA  <:  C ) ทำให้มันเป็นพรีออร์เดอร์บนประเภทข้อมูล

ประเภทของระเบียนก่อให้เกิดแนวคิดเรื่อง การแบ่งประเภท ย่อยตามความกว้างและความลึกซึ่งแสดงถึงสองวิธีที่แตกต่างกันในการสร้างระเบียนประเภทใหม่ที่อนุญาตให้ดำเนินการได้เช่นเดียวกับระเบียนประเภทเดิม

โปรดจำไว้ว่า เรคอร์ด คือ ชุดของฟิลด์ (ที่มีชื่อ) เนื่องจากซับไทป์คือไทป์ที่อนุญาตให้ดำเนินการทุกอย่างที่อนุญาตบนไทป์ดั้งเดิม ดังนั้น ซับไทป์ของเรคอร์ดจึงควรสนับสนุนการดำเนินการเดียวกันกับฟิลด์ต่างๆ เช่นเดียวกับที่ไทป์ดั้งเดิมสนับสนุน

วิธีหนึ่งในการรองรับการทำงานดังกล่าว เรียกว่า การกำหนด ชนิดย่อย ของความกว้าง (width subtyping ) โดยการเพิ่มฟิลด์เพิ่มเติมลงในเรคอร์ด กล่าวอย่างเป็นทางการคือ ฟิลด์ทุกฟิลด์ (ที่มีชื่อ) ที่ปรากฏในชนิดหลักของความกว้าง (width supertype) จะปรากฏในชนิดย่อยของความกว้าง (width subtype) ด้วย ดังนั้น การดำเนินการใดๆ ที่สามารถทำได้กับชนิดหลักก็จะได้รับการสนับสนุนโดยชนิดย่อยเช่นกัน

วิธีที่สอง เรียกว่าการกำหนดชนิดย่อยเชิงลึก (depth subtyping ) จะแทนที่ฟิลด์ต่างๆ ด้วยชนิดย่อยของฟิลด์เหล่านั้น กล่าวคือ ฟิลด์ของชนิดย่อยจะเป็นชนิดย่อยของฟิลด์ของชนิดหลัก เนื่องจากทุกการดำเนินการที่รองรับสำหรับฟิลด์ในชนิดหลักจะรองรับสำหรับชนิดย่อยของมัน ดังนั้น การดำเนินการใดๆ ที่ทำได้กับชนิดหลักของเรคอร์ดจึงรองรับโดยชนิดย่อยของเรคอร์ด การกำหนดชนิดย่อยเชิงลึกนั้นเหมาะสมเฉพาะกับเรคอร์ดที่ไม่สามารถเปลี่ยนแปลงได้เท่านั้น ตัวอย่างเช่น คุณสามารถกำหนดค่า 1.5 ให้กับฟิลด์ 'x' ของจุดจำนวนจริง (เรคอร์ดที่มีฟิลด์จำนวนจริงสองฟิลด์) แต่คุณไม่สามารถทำเช่นเดียวกันกับฟิลด์ 'x' ของจุดจำนวนเต็ม (ซึ่งเป็นชนิดย่อยเชิงลึกของชนิดจุดจำนวนจริง) ได้ เพราะ 1.5 ไม่ใช่จำนวนเต็ม (ดูความแปรปรวน )

การกำหนดชนิดย่อยของเรคอร์ดสามารถทำได้ในSystem F _<:ซึ่งเป็นการผสมผสานระหว่างโพลีมอร์ฟิซึมแบบพารามิเตอร์กับการกำหนดชนิดย่อยของประเภทเรคอร์ด และเป็นพื้นฐานทางทฤษฎีสำหรับภาษาการเขียนโปรแกรมเชิงฟังก์ชัน หลายภาษา ที่รองรับคุณสมบัติทั้งสองนี้

บางระบบยังรองรับการกำหนดชนิดย่อยของ ชนิด ยูเนียนที่ไม่ทับซ้อนกันที่ มีป้ายกำกับ (เช่นชนิดข้อมูลเชิงพีชคณิต ) กฎสำหรับการกำหนดชนิดย่อยของความกว้างจะกลับกัน: แท็กทุกตัวที่ปรากฏในชนิดย่อยของความกว้างจะต้องปรากฏในชนิดหลักของความกว้างด้วย

ถ้าT ₁ → T ₂เป็นประเภทฟังก์ชันแล้ว ประเภทย่อยของมันคือประเภทฟังก์ชันS ₁ → S ₂ ใดๆ ที่มีคุณสมบัติว่าT ₁ <: S ₁และS ₂ <: T ₂สามารถสรุปได้โดยใช้กฎการกำหนดประเภท ต่อไป นี้ :

$${\displaystyle {T_{1}\leq :S_{1}\quad S_{2}\leq :T_{2}} \over {S_{1}\rightarrow S_{2}\leq :T_{1}\rightarrow T_{2}}}$$

ประเภทพารามิเตอร์ของS ₁ → S ₂เรียกว่าเป็นแบบคอนทราแวเรียนต์ (contravariant)เพราะความสัมพันธ์ของการกำหนดชนิดย่อย (subtyping) นั้นกลับด้าน ในขณะที่ประเภทค่าส่งคืนเป็นแบบโคแวเรียนต์ (covariant ) โดยทั่วไป การกลับด้านนี้เกิดขึ้นเพราะชนิดที่ปรับปรุงแล้วนั้น "มีความยืดหยุ่นมากกว่า" ในชนิดที่ยอมรับ และ "มีความเข้มงวดมากกว่า" ในชนิดที่ส่งคืน นี่คือสิ่งที่ใช้งานได้จริงในScala : ฟังก์ชัน n -ary ภายในเป็นคลาสที่สืบทอดคุณสมบัติ (trait ) (ซึ่งสามารถมองได้ว่าเป็นอินเทอร์เฟซ ทั่วไป ใน ภาษาที่คล้าย Java ) โดยที่คือประเภทของพารามิเตอร์ และคือประเภทค่าส่งคืน เครื่องหมาย "−" หน้าประเภทหมายความว่าประเภทนั้นเป็นคอนทราแวเรียนต์ ในขณะที่เครื่องหมาย "+" หมายความว่าเป็นแบบโคแวเรียนต์ ${\displaystyle {\mathtt {Function_{N}({-A_{1}},{-A_{2}},\dots ,{-A_{n}},{+B})}}}$${\displaystyle {\mathtt {A_{1},A_{2},\dots ,A_{n}}}}$${\displaystyle {\mathtt {B}}}$

ในภาษาที่อนุญาตให้มีผลข้างเคียง เช่น ภาษาเชิงวัตถุส่วนใหญ่ การกำหนดชนิดย่อยโดยทั่วไปไม่เพียงพอที่จะรับประกันว่าฟังก์ชันสามารถใช้งานได้อย่างปลอดภัยในบริบทของฟังก์ชันอื่น งานของ Liskov ในด้านนี้มุ่งเน้นไปที่การกำหนดชนิดย่อยเชิงพฤติกรรม ซึ่งนอกจากความปลอดภัยของระบบประเภทที่กล่าวถึงในบทความนี้แล้ว ยังต้องการให้ชนิดย่อยรักษา คุณสมบัติคงที่ทั้งหมดที่รับประกันโดยชนิดหลักในสัญญา บาง อย่าง^{[ 8 ]}คำจำกัดความของการกำหนดชนิดย่อยนี้โดยทั่วไปไม่สามารถตัดสินได้ดังนั้นจึงไม่สามารถตรวจสอบได้ด้วย ตัวตรวจ สอบ ประเภท

การกำหนดชนิดย่อยของตัวอ้างอิงที่เปลี่ยนแปลงได้นั้นคล้ายกับการจัดการค่าพารามิเตอร์และค่าส่งคืน ตัวอ้างอิงที่เขียนได้อย่างเดียว (หรือsink ) นั้นเป็นแบบ contravariant เช่นเดียวกับค่าพารามิเตอร์ ตัวอ้างอิงที่อ่านได้อย่างเดียว (หรือsource ) นั้นเป็นแบบ covariant เช่นเดียวกับค่าส่งคืน ตัวอ้างอิงที่เปลี่ยนแปลงได้ซึ่งทำหน้าที่ทั้งเป็น source และ sink นั้นเป็นแบบ invariant

การกำหนดชนิดย่อยและการสืบทอดเป็นความสัมพันธ์ที่เป็นอิสระต่อกัน (ตั้งฉากกัน) ทั้งสองอาจเกิดขึ้นพร้อมกันได้ แต่ไม่มีความสัมพันธ์ใดเป็นกรณีพิเศษของอีกความสัมพันธ์หนึ่ง กล่าวคือ ระหว่างชนิดSและT สองชนิด การกำหนดชนิดย่อยและการสืบทอดทุกรูปแบบเป็นไปได้ทั้งหมด:

1. Sไม่ใช่ทั้งชนิดย่อยหรือชนิดที่ได้มาจากT
2. Sเป็นชนิดย่อย แต่ไม่ใช่ชนิดที่ได้มาจากT
3. Sไม่ใช่ชนิดย่อย แต่เป็นชนิดที่ได้มาจากT
4. Sเป็นทั้งชนิดย่อยและชนิดที่ได้มาจากT

กรณีแรกแสดงให้เห็นได้จากประเภทอิสระเช่น BooleanและFloat

กรณีที่สองสามารถอธิบายได้ด้วยความสัมพันธ์ระหว่างInt32และInt64ในภาษาการเขียนโปรแกรมเชิงวัตถุส่วนใหญ่Int64จะไม่เกี่ยวข้องกับการสืบทอดทางกรรมพันธุ์กับInt32อย่างไรก็ตามInt32สามารถพิจารณาได้ว่าเป็นชนิดย่อยของInt64เนื่องจากค่าจำนวนเต็ม 32 บิตใดๆ ก็สามารถแปลงเป็นค่าจำนวนเต็ม 64 บิตได้

กรณีที่สามเป็นผลมาจากความสัมพันธ์ผกผันของอินพุตในการกำหนดประเภทย่อยของฟังก์ชันสมมติว่ามีคลาสแม่ประเภทTที่มีเมธอดmซึ่งส่งคืนอ็อบเจ็กต์ประเภทเดียวกัน ( กล่าวคือประเภทของmคือT → Tและโปรดทราบว่าพารามิเตอร์แรกของmคือ this/self) และมีคลาสที่สืบทอดประเภทSจากTโดยการสืบทอด ประเภทของmในSคือS → Sเพื่อให้Sเป็นประเภทย่อยของTประเภทของmในSต้องเป็นประเภทย่อยของประเภทของmในTกล่าวอีกนัยหนึ่งคือS → S ≤ T → Tโดยการประยุกต์ใช้กฎการกำหนดประเภทย่อยของฟังก์ชันจากล่างขึ้นบน หมายความว่าS ≤ TและT ≤ Sซึ่งเป็นไปได้ก็ต่อเมื่อSและTเหมือนกันเท่านั้น เนื่องจากความสัมพันธ์ในการสืบทอดเป็นความสัมพันธ์ที่ไม่สะท้อนกลับSจึงไม่สามารถเป็นประเภทย่อยของTได้

การกำหนดประเภทย่อยและการสืบทอดจะเข้ากันได้เมื่อฟิลด์และเมธอดที่สืบทอดทั้งหมดของประเภทที่ได้มามีประเภทที่เป็นประเภทย่อยของฟิลด์และเมธอดที่สอดคล้องกันจากประเภทที่สืบทอดมา^{[ 3 ]}

ในระบบการกำหนดชนิดย่อยแบบบังคับ ชนิดย่อยจะถูกกำหนดโดย ฟังก์ชัน การแปลงชนิด ที่ชัดเจน จากชนิดย่อยไปยังชนิดหลัก สำหรับความสัมพันธ์การกำหนดชนิดย่อยแต่ละรายการ ( S <: T ) จะมีฟังก์ชันการแปลงcoerce : S → Tให้ และวัตถุs ใดๆ ที่มีชนิดSจะถือว่าเป็นวัตถุcoerce _{S → T} ( s ) ที่มีชนิดTฟังก์ชันการแปลงอาจถูกกำหนดโดยการประกอบ: ถ้าS <: TและT <: Uแล้วsอาจถือว่าเป็นวัตถุที่มีชนิดuภายใต้การแปลงแบบผสม ( coerce _{T → U} ∘ coerce _{S → T} ) การแปลงชนิดจากชนิดหนึ่งไปยังตัวมันเองcoerce T _{→ T คือ}ฟังก์ชันเอกลักษณ์id _T

ฟังก์ชันการแปลงประเภทสำหรับเรคอร์ดและ ซับไทป์ ยูเนียนที่ไม่ทับซ้อนกันอาจถูกกำหนดแบบแยกส่วน ในกรณีของเรคอร์ดที่ขยายความกว้าง การแปลงประเภทจะละทิ้งส่วนประกอบใดๆ ที่ไม่ได้กำหนดไว้ในซูเปอร์ไทป์ การแปลงประเภทสำหรับประเภทฟังก์ชันอาจกำหนดโดยf' ( t ) = coerce _{S 2 → T 2} ( f ( coerce _{T 1 → S 1} ( t ))) ซึ่งสะท้อนถึงความแปรปรวนผกผันของค่าพารามิเตอร์และความแปรปรวนร่วมของค่าส่งคืน

ฟังก์ชันการแปลงประเภทจะถูกกำหนดอย่างเฉพาะเจาะจงโดยขึ้นอยู่กับชนิดย่อยและชนิดหลักดังนั้น เมื่อมีการกำหนดความสัมพันธ์ของชนิดย่อยหลายแบบ จึงต้องระมัดระวังเพื่อให้แน่ใจว่าการแปลงประเภททั้งหมดมีความสอดคล้องกัน ตัวอย่างเช่น หากจำนวนเต็ม เช่น 2 : intสามารถแปลงเป็นจำนวนทศนิยม (เช่น 2.0 : float ) ได้ ก็จะไม่สามารถแปลง 2.1 : floatเป็น 2 : int ได้เพราะการแปลงแบบผสม coerce float _{→ float ที่}กำหนดโดยcoerce _{int → float} ∘ coerce _{float → int}จะแตกต่างจากการแปลงแบบเอกลักษณ์ id _float

หนังสือวิกิเกี่ยวกับการเขียนโปรแกรมภาษาอะดามีหน้าหนึ่งที่กล่าวถึงหัวข้อ: ชนิดย่อย (Subtypes)

• ความแปรปรวนร่วมและความแปรปรวนผกผัน
• ปัญหาเรื่อง วงกลม-วงรี (สำหรับอันตรายของการกำหนดชนิดย่อยของชนิดตัวแปรบนพื้นฐานเดียวกับชนิดค่า)
• การเขียนโปรแกรมแบบแบ่งตามคลาส
• ประเภทสูงสุด
• ประเภทการปรับแต่ง
• การจำแนกประเภทพฤติกรรมย่อย