ในทฤษฎีประเภทระบบประเภทจะกล่าวได้ว่ามี คุณสมบัติ ประเภทหลักหากเมื่อกำหนดเทอมและสภาพแวดล้อมแล้ว มีประเภทหลักสำหรับเทอมนี้ในสภาพแวดล้อมนี้ กล่าวคือ ประเภทที่ทำให้ประเภทอื่นๆ ทั้งหมดสำหรับเทอมนี้ในสภาพแวดล้อมนี้เป็นอินสแตนซ์ของประเภทหลัก

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

ตัวอย่างเช่น ระบบ MLมีคุณสมบัติประเภทหลัก (principal type) และประเภทหลักสำหรับนิพจน์สามารถคำนวณได้โดยอัลกอริทึมการรวมของ Robinsonซึ่งใช้ใน อัลกอริทึม การอนุมานประเภท Hindley–Milnerอย่างไรก็ตาม ส่วนขยายหลายอย่างของระบบประเภทของ ML เช่นการเรียกซ้ำแบบพหุรูป (polymorphic recursion ) อาจทำให้การอนุมานประเภทหลักไม่สามารถตัดสินได้ ส่วนขยายอื่นๆ เช่นประเภทข้อมูลพีชคณิตทั่วไปของHaskellทำลายคุณสมบัติประเภทหลักของภาษา ทำให้ต้องใช้คำอธิบายประกอบประเภทหรือให้คอมไพเลอร์ "เดา" ประเภทที่ต้องการจากตัวเลือกหลายๆ ตัวเลือก

แนวคิดนี้ได้รับการแนะนำโดยCurryและFeysประมาณปี 1958 ^{[ 1 ]}ภายใต้ชื่อ "อักขระฟังก์ชันหลัก" ^{[ 2 ]}ชื่อ "ประเภทหลัก" (รวมถึง " แผนผัง ประเภท ") มาจากHindley (1969) ^{[ 2 ]}

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

คุณสมบัติการกำหนดประเภทหลักช่วยให้สามารถให้เหตุผลประเภทแบบ "องค์ประกอบ" ได้ ซึ่งหมายความว่าการวิเคราะห์สามารถดำเนินการกับส่วนต่างๆ ได้ในลำดับใดก็ได้ระบบประเภท Hindley–Milnerไม่ใช่แบบองค์ประกอบในแง่นี้เนื่องจากวิธีlet val x = e1 in e2 endการกำหนดประเภทก่อนโดยการประเมินประเภทของe1และใช้ผลลัพธ์เพื่อกำหนดประเภทe2[ ^{4 ] ดังนั้น}จึงกล่าวได้ว่า ML มีประเภทหลักแต่ไม่มีการกำหนดประเภทหลัก^{[ 3 ]}ในทางกลับกันแคลคูลัสแลมบ์ดาแบบกำหนดประเภทอย่างง่ายมี คุณสมบัติทั้งสองนี้ ^{[ 3 ] [ 4 ]}

โดยทั่วไป ระบบประเภทที่อิงตามประเภทการตัดกันยังมีคุณสมบัติการกำหนดประเภทหลักด้วย^{[ 5 ]}ซึ่งอาจคำนวณ ไม่ได้ แม้ว่าหากจำกัดการตัดกันไว้ที่อันดับ 2 ^{[ 3 ]}หรือด้วยการแนะนำตัวแปรเพิ่มเติมบางอย่างไปยังอันดับจำกัดใดๆ การกำหนดประเภทหลักก็จะสามารถคำนวณได้สำหรับประเภทการตัดกัน^{[ 6 ]}ระบบประเภทเหล่านี้ได้รับการเสนอสำหรับการใช้งานต่างๆ โดยทั่วไปมุ่งเน้นไปที่การคอมไพล์แบบเพิ่มทีละน้อย^{[ 7 ] [ 8 ] [ 3 ]}หรือการ กำหนดประเภทแบบ ค่อยเป็นค่อยไป^{[ 9 ]}