ในทฤษฎีประเภทการอนุมานประเภท ( บางครั้งเรียกว่าการสร้างประเภทใหม่ ) คือการตรวจจับประเภทของนิพจน์ โดยอัตโนมัติ ^{[ 1 ] : 320} ซึ่งรวมถึงภาษาโปรแกรมและระบบประเภท ทางคณิตศาสตร์ แต่ยังรวมถึงภาษา ธรรมชาติในบางสาขาของวิทยาศาสตร์คอมพิวเตอร์และภาษาศาสตร์ด้วย

บางครั้ง คำว่า "ความสามารถในการกำหนดประเภท" ถูกใช้ในความหมายที่คล้ายคลึงกันกับ "การอนุมานประเภท" อย่างไรก็ตาม ผู้เขียนบางคนแยกความแตกต่างระหว่างความสามารถในการกำหนดประเภทในฐานะปัญหาการตัดสินใจ (ที่มีคำตอบใช่/ไม่ใช่) และการอนุมานประเภทในฐานะการคำนวณประเภทจริงสำหรับเทอม^{[ 2 ]}

ในภาษาที่มีการกำหนดประเภทคำ ประเภทของคำจะเป็นตัวกำหนดวิธีการใช้คำนั้นในภาษานั้น ตัวอย่างเช่น ลองพิจารณาภาษาอังกฤษและคำที่สามารถเติมลงในช่องว่างในวลี "ร้องเพลง..." คำว่า "เพลง" (a song) เป็นประเภทคำที่ใช้ร้องเพลงได้ ดังนั้นจึงสามารถใส่ลงในช่องว่างเพื่อสร้างวลีที่มีความหมายได้ว่า "ร้องเพลงเพลงหนึ่ง" (sing a song) ในทางกลับกัน คำว่า "เพื่อน" (a friend) ไม่ใช่ประเภทคำที่ใช้ร้องเพลงได้ ดังนั้น "ร้องเพลงเพื่อน" (sing a friend) จึงไม่มีความหมาย อย่างดีที่สุดก็อาจเป็นเพียงคำอุปมา การแหกกฎประเภทคำเป็นลักษณะเฉพาะของภาษากวี

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

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

การกำหนดประเภทมักใช้เพื่อป้องกันไม่ให้วัตถุถูกมองว่าเป็นสิ่งทั่วไปเกินไป ตัวอย่างเช่น หากระบบประเภทถือว่าตัวเลขทั้งหมดเหมือนกัน โปรแกรมเมอร์ที่เขียนโค้ดผิดพลาดโดยที่ตัวเลขหนึ่ง4ควรหมายถึง "4 วินาที" แต่ถูกตีความว่าเป็น "4 เมตร" จะไม่ได้รับคำเตือนถึงความผิดพลาดจนกว่าจะเกิดปัญหาขณะรันไทม์ การรวมหน่วยเข้าไปในระบบประเภทจะช่วยให้ตรวจพบความผิดพลาดเหล่านี้ได้เร็วขึ้นมาก อีกตัวอย่างหนึ่งคือปรากฏการณ์ของรัสเซลล์เกิดขึ้นเมื่อสิ่งใดๆ ก็สามารถเป็นสมาชิกของเซตได้ และ述语ใดๆ ก็สามารถกำหนดเซตได้ แต่การกำหนดประเภทอย่างระมัดระวังมากขึ้นจะช่วยแก้ปัญหานี้ได้หลายวิธี อันที่จริง ปรากฏการณ์ของรัสเซลล์เป็นแรงบันดาลใจให้เกิดทฤษฎีประเภทในยุคแรกๆ

คำศัพท์หนึ่งๆ สามารถได้รับรูปแบบเฉพาะได้หลายวิธี:

• รูปแบบตัวอักษรอาจมาจากแหล่งอื่นนอกเหนือจากเนื้อหาหลัก ตัวอย่างเช่น หากผู้พูดกล่าวถึง "เพลง" ในภาษาอังกฤษ โดยทั่วไปแล้วพวกเขาไม่จำเป็นต้องบอกผู้ฟังว่า "เพลง" นั้นสามารถร้องและแต่งได้ เพราะข้อมูลนั้นเป็นส่วนหนึ่งของความรู้พื้นฐานที่ผู้ฟังมีร่วมกันอยู่แล้ว
• สามารถประกาศชนิดข้อมูลได้อย่างชัดเจน ตัวอย่างเช่น โปรแกรมเมอร์อาจเขียนคำสั่งเช่นนี้delay: seconds := 4ในโค้ดของตน โดยที่เครื่องหมายโคลอนเป็นสัญลักษณ์ทางคณิตศาสตร์ที่ใช้กันทั่วไปเพื่อระบุชนิดของข้อมูล นั่นหมายความว่า คำสั่งนี้ไม่เพียงแต่กำหนดdelayค่าให้กับตัวแปร เท่านั้น 4แต่delay: secondsส่วน `--time` ยังบ่งชี้ด้วยว่าdelayชนิดของตัวแปรคือปริมาณเวลาในหน่วยวินาที
• เราสามารถ อนุมานประเภทของคำได้จากบริบท ตัวอย่างเช่น ในวลี "I bought it for a song" (ฉันซื้อมาในราคาถูกมาก) เราจะสังเกตได้ว่า การพยายามกำหนดประเภทของคำให้กับคำว่า "a song" เช่น "ร้องได้" และ "แต่งได้" จะทำให้ความหมายผิดเพี้ยนไป ในขณะที่ประเภท "จำนวนเงิน" นั้นเหมาะสมกว่า ดังนั้นโดยไม่ต้องมีใครบอก เราจึงสรุปได้ว่า "song" ในที่นี้ต้องหมายถึง "น้อยมากหรือไม่มีเลย" ดังเช่นสำนวนภาษาอังกฤษ " for a song " (ในราคาถูกมาก) ไม่ใช่ "บทเพลงที่มีเนื้อร้อง"

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

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

ในบริบทนี้ คำถามต่อไปนี้มีความน่าสนใจเป็นพิเศษ:

1. E : T? ในกรณีนี้ ทั้งนิพจน์ E และชนิดข้อมูล T ถูกกำหนดมาให้แล้ว ทีนี้ E เป็น T จริงๆ หรือไม่? สถานการณ์นี้เรียกว่าการตรวจสอบชนิดข้อมูล (type-checking )
2. E : _? ในที่นี้ เรารู้เพียงแค่รูปแบบการแสดงออกเท่านั้น หากมีวิธีใดที่จะอนุมานประเภทของ E ได้ เราก็จะประสบความสำเร็จในการอนุมานประเภทแล้ว
3. _ : T? กลับกัน ถ้ากำหนดแค่ชนิดข้อมูลมา จะมีนิพจน์ใดที่ใช้แทนชนิดข้อมูลนั้นได้หรือไม่ หรือว่าชนิดข้อมูลนั้นไม่มีค่า? มีตัวอย่างของ T หรือไม่? นี่เรียกว่าการมีอยู่ของชนิดข้อมูล (type inhabitation )

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

ประเภทเป็นคุณลักษณะที่มีอยู่ใน ภาษา ที่มีการกำหนดประเภทแบบคงที่อย่างเข้มงวด บางภาษา โดยทั่วไปแล้วมักเป็นลักษณะเฉพาะของภาษาการเขียนโปรแกรมเชิงฟังก์ชัน ภาษา บางภาษาที่รวมการอนุมานประเภทไว้ ได้แก่ C (ตั้งแต่C23 ), ^{[ 3 ]} C++ (ตั้งแต่C++11 ), ^{[ 4 ]} C# (เริ่มตั้งแต่เวอร์ชัน 3.0), Chapel , Clean , Crystal , D , Dart , ^{[ 5 ]} F# , ^{[ 6 ]} FreeBASIC , Go , Haskell , Java (เริ่มตั้งแต่เวอร์ชัน 10), Julia , ^{[ 7 ]} Kotlin , ^{[ 8 ]} ML , Nim , OCaml , Opa , Q#, RPython , Rust , ^{[ 9 ]} Scala , ^{[ 10 ]} Swift , ^{[ 11 ]} TypeScript , ^{[ 12 ]} Vala , ^{[ 13 ]} ZigและVisual Basic ^{[ 14 ]} (เริ่มตั้งแต่เวอร์ชัน 9.0) ระบบ ส่วนใหญ่ใช้การอนุมานประเภทแบบง่ายๆระบบประเภท Hindley–Milnerสามารถให้การอนุมานประเภทที่สมบูรณ์กว่าได้ ความสามารถในการอนุมานประเภทโดยอัตโนมัติทำให้งานเขียนโปรแกรมหลายอย่างง่ายขึ้น ทำให้โปรแกรมเมอร์สามารถละเว้นการระบุประเภท ได้ ในขณะที่ยังคงอนุญาตให้มีการตรวจสอบประเภทอยู่

ในบางภาษาโปรแกรม ค่าทั้งหมดจะมีชนิดข้อมูลที่ประกาศไว้อย่างชัดเจนในขั้นตอนการคอมไพล์ซึ่งจำกัดค่าที่นิพจน์นั้นๆ สามารถรับได้ในขั้นตอนการ รันไทม์ การคอมไพล์แบบ Just-in-Time (JIT) ทำให้ความแตกต่างระหว่างขั้นตอนการรันไทม์และขั้นตอนการคอมไพล์นั้นเลือนลาง ลงเรื่อยๆอย่างไรก็ตาม ในอดีต หากทราบชนิดของค่าเฉพาะในขั้นตอนการรันไทม์ ภาษาเหล่านั้นจะเป็นภาษาแบบไดนามิกไทป์ ส่วนในภาษาอื่นๆ หากทราบชนิดของนิพจน์เฉพาะในขั้นตอนการคอมไพล์ภาษาเหล่านั้นจะ เป็นภาษา แบบสแตติกไทป์ในภาษาแบบสแตติกไทป์ส่วนใหญ่ ชนิดข้อมูลขาเข้าและขาออกของฟังก์ชันและตัวแปรโลคอลมักจะต้องระบุอย่างชัดเจนด้วยคำอธิบายประกอบชนิดข้อมูล ตัวอย่างเช่น ในภาษา ANSI C :

int increment ( int x ) { int result ; // ประกาศตัวแปรประเภท integer resultผลลัพธ์= x + 1 ; ส่งคืนผลลัพธ์; }

ลายเซ็นของนิยามฟังก์ชันนี้ประกาศว่าเป็นฟังก์ชันที่รับอาร์กิวเมนต์หนึ่งตัว คือจำนวนเต็มและส่งคืนค่าจำนวนเต็มประกาศว่าตัวแปรโลคอลเป็นจำนวนเต็ม ในภาษาสมมุติที่รองรับการอนุมานประเภท โค้ดอาจเขียนได้แบบนี้แทน: intincrement(intx)increment()int result;result

เพิ่มค่า( x ) { var result ; // ตัวแปรประเภทอนุมาน result var result2 ; // ตัวแปรประเภทอนุมาน result #2result = x + 1 ; result2 = x + 1.0 ; // บรรทัดนี้จะไม่ทำงาน (ในภาษาที่เสนอ) return result ; }

วิธีการนี้เหมือนกับวิธีการเขียนโค้ดในภาษาDartทุกประการ ยกเว้นว่าจะมีข้อจำกัดเพิ่มเติมบางประการดังที่อธิบายไว้ด้านล่าง เป็นไปได้ที่จะอนุมานชนิดของตัวแปรทั้งหมดในระหว่างการคอมไพล์ ในตัวอย่างข้างต้น คอมไพเลอร์จะอนุมานว่าresultและxมีชนิดเป็นจำนวนเต็ม เนื่องจากค่าคงที่นั้น1มีชนิดเป็นจำนวนเต็ม ดังนั้น จึงincrement()เป็นฟังก์ชันint -> intส่วนตัวแปรresult2ไม่ได้ถูกใช้งานอย่างถูกต้อง ดังนั้นจึงไม่มีชนิดข้อมูล

ในภาษาสมมติที่ใช้เขียนตัวอย่างสุดท้าย คอมไพเลอร์จะสันนิษฐานว่า ในกรณีที่ไม่มีข้อมูลอื่นใดมาหักล้าง ฟังก์ชัน+จะรับจำนวนเต็มสองจำนวนและส่งคืนค่าจำนวนเต็มหนึ่งจำนวน (นี่คือวิธีการทำงานในภาษาOCamlเป็นต้น) จากนั้น ตัวอนุมานประเภทสามารถอนุมานได้ว่าประเภทของx + 1เป็นจำนวนเต็ม ซึ่งหมายความว่าresultเป็นจำนวนเต็ม และดังนั้นค่าที่ส่งคืนของ จึงadd_oneเป็นจำนวนเต็ม ในทำนองเดียวกัน เนื่องจาก+ต้องการให้พารามิเตอร์ทั้งสองมีประเภทเดียวกัน ดังนั้นxต้องเป็นจำนวนเต็ม และด้วยเหตุนี้ จึงadd_oneรับจำนวนเต็มหนึ่งจำนวนเป็นพารามิเตอร์

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

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

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

สุดท้ายนี้ ข้อเสียที่สำคัญอย่างหนึ่งของอัลกอริธึมการอนุมานประเภทที่ซับซ้อนก็คือ ผลลัพธ์ของการอนุมานประเภทจะไม่ชัดเจนสำหรับมนุษย์ (โดยเฉพาะอย่างยิ่งเนื่องจากการย้อนกลับ) ซึ่งอาจเป็นอันตรายได้ เนื่องจากโค้ดนั้นมีจุดประสงค์หลักเพื่อให้มนุษย์เข้าใจได้

การเกิดขึ้นของการคอมไพล์แบบทันเวลา (Just-in-Time Compilation หรือ JIT) ในปัจจุบัน ทำให้เกิดแนวทางแบบผสมผสาน โดยที่ประเภทของอาร์กิวเมนต์ที่ส่งมาจากบริบทการเรียกใช้ต่างๆ จะทราบได้ในระหว่างการคอมไพล์ และสามารถสร้างเวอร์ชันที่คอมไพล์แล้วจำนวนมากของฟังก์ชันเดียวกันได้ จากนั้นแต่ละเวอร์ชันที่คอมไพล์แล้วสามารถปรับให้เหมาะสมกับชุดประเภทที่แตกต่างกันได้ ตัวอย่างเช่น การคอมไพล์แบบ JIT อนุญาตให้มีเวอร์ชันที่คอมไพล์แล้วอย่างน้อยสองเวอร์ชันของincrement():

เวอร์ชันที่รับค่าจำนวนเต็มเป็นอินพุตและใช้การแปลงประเภทโดยปริยาย

เวอร์ชันที่รับค่าตัวเลขทศนิยมเป็นอินพุตและใช้คำสั่งคำนวณเลขทศนิยมตลอดทั้งระบบ

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

เพื่อให้ได้ข้อมูลที่จำเป็นในการอนุมานประเภทของนิพจน์ คอมไพเลอร์จะรวบรวมข้อมูลนี้โดยการรวบรวมและลดทอนคำอธิบายประเภทที่กำหนดไว้สำหรับนิพจน์ย่อย หรือโดยความเข้าใจโดยปริยายเกี่ยวกับประเภทของค่าอะตอมต่างๆ (เช่น true : Bool; 42 : Integer; 3.14159 : Real; เป็นต้น) การรับรู้ถึงการลดทอนนิพจน์ไปเป็นค่าอะตอมที่มีประเภทโดยปริยายนี้เองที่ทำให้คอมไพเลอร์สำหรับภาษาที่อนุมานประเภทสามารถคอมไพล์โปรแกรมได้อย่างสมบูรณ์โดยไม่ต้องใช้คำอธิบายประเภท

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

วิธีการอนุมานประเภทบางวิธีขึ้นอยู่กับความพึงพอใจของข้อจำกัด^{[ 16 ]}หรือ ความพึงพอใจ ตามทฤษฎีโมดูล^{[ 17 ]}

ตัวอย่างเช่นฟังก์ชันในภาษา Haskellmapจะใช้ฟังก์ชันกับแต่ละองค์ประกอบของลิสต์ และสามารถนิยามได้ดังนี้:

map f [] = [] map f ( first : rest ) = f first : map f rest

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

การอนุมานประเภทของmapฟังก์ชันดำเนินไปดังนี้mapเป็นฟังก์ชันที่มีอาร์กิวเมนต์สองตัว ดังนั้นประเภทของฟังก์ชันจึงถูกจำกัดให้อยู่ในรูปแบบใน Haskell รูปแบบและจะตรงกับลิสต์เสมอ ดังนั้นอาร์กิวเมนต์ตัวที่สองต้องเป็นประเภทลิสต์: สำหรับบางประเภทอาร์กิวเมนต์ตัวแรกจะถูกนำไปใช้กับอาร์กิวเมนต์ซึ่งต้องมีประเภทที่สอดคล้องกับประเภทในอาร์กิวเมนต์ลิสต์ ดังนั้น( หมายถึง "มีประเภท") สำหรับบางประเภท สุดท้ายแล้ว ค่าที่ส่งคืนของ คือลิส ต์ ของสิ่งที่สร้างขึ้น ดังนั้นa->b->c[](first:rest)b=[d]dffirstdf::d->e::emapff[e]

เมื่อนำส่วนต่างๆ มารวมกันจะได้. ไม่มีอะไรพิเศษเกี่ยวกับตัวแปรประเภท ดังนั้นจึงสามารถเปลี่ยนชื่อเป็น ได้ map::(d->e)->[d]->[e]

แผนที่:: ( a -> b ) -> [ a ] ​​-> [ b ]

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

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

map f [] = [] map f ( first : rest ) = f first : map f rest

(ย้ำอีกครั้งว่า ` :there` คือตัวสร้างลิสต์ของ Haskell ไม่ใช่ตัวดำเนินการ `of` ซึ่ง Haskell เขียนว่า ` ::.` แทน)

ขั้นแรก เราสร้างตัวแปรประเภทใหม่สำหรับแต่ละคำศัพท์:

• αจะบ่งบอกถึงประเภทmapที่เราต้องการอนุมาน
• βจะระบุประเภทของfในสมการแรก
• [γ]จะระบุประเภทของ[]ด้านซ้ายของสมการแรก
• [δ]จะระบุประเภทของ[]ทางด้านขวาของสมการแรก
• εจะระบุประเภทของfในสมการที่สอง
• ζ -> [ζ] -> [ζ]จะหมายถึงประเภทของตัวแปร:ทางด้านซ้ายของสมการแรก (รูปแบบนี้ทราบได้จากคำนิยาม)
• ηจะระบุประเภทfirstของ
• θจะระบุประเภทrestของ
• ι -> [ι] -> [ι]จะระบุประเภทของ:ทางด้านขวาของสมการแรก

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

• κจะหมายถึงประเภทของเราสรุปได้ว่าโดยที่สัญลักษณ์ "คล้ายกัน" หมายถึง "รวมเป็นหนึ่งเดียวกับ" เรากำลังบอกว่าประเภทของจะต้องเข้ากันได้กับประเภทของฟังก์ชันที่รับและรายการของ และส่งคืนค่าmapf[]α ~ β -> [γ] -> κ~αmapβγκ
• λจะบ่งบอกถึงประเภทของเราสรุปได้ว่า(first:rest)ζ -> [ζ] -> [ζ] ~ η -> θ -> λ
• μจะบ่งบอกถึงประเภทของเราสรุปได้ว่าmapf(first:rest)α ~ ε -> λ -> μ
• νจะบ่งบอกถึงประเภทของเราสรุปได้ว่าffirstε ~ η -> ν
• ξจะบ่งบอกถึงประเภทของเราสรุปได้ว่าmapfrestα ~ ε -> θ -> ξ
• οจะบ่งบอกถึงประเภทของเราสรุปได้ว่าffirst:mapfrestι -> [ι] -> [ι] ~ ν -> ξ -> ο

นอกจากนี้ เรายังกำหนดให้ด้านซ้ายและด้านขวาของแต่ละสมการสามารถรวมกันได้ดังนี้: κ ~ [δ]และμ ~ οโดยรวมแล้ว ระบบสมการที่ต้องแก้คือ:

α ~ β -> [γ] -> κ ζ -> [ζ] -> [ζ] ~ η -> θ -> แล α ~ ε -> λ -> μ ε ~ η -> ν α ~ ε -> θ -> ξ ι -> [ι] -> [ι] ~ ν -> ξ -> ο κ ~ [δ] μ ~ ο 

จากนั้นเราจะทำการแทนค่าไปเรื่อยๆ จนกว่าจะไม่สามารถกำจัดตัวแปรใดๆ ได้อีก ลำดับที่แน่นอนไม่สำคัญ หากโค้ดผ่านการตรวจสอบประเภทแล้ว ลำดับใดๆ ก็จะนำไปสู่รูปแบบสุดท้ายเดียวกัน มาเริ่มกันด้วยการแทนค่าοสำหรับμและ[δ]สำหรับκ:

α ~ β -> [γ] -> [δ] ζ -> [ζ] -> [ζ] ~ η -> θ -> แล α ~ ε -> λ -> ο ε ~ η -> ν α ~ ε -> θ -> ξ ι -> [ι] -> [ι] ~ ν -> ξ -> ο 

การแทนที่ζด้วยη, [ζ]ด้วยθและλ, ιด้วยν, ด้วย และ[ι]ด้วยξและοทั้งหมดนี้เป็นไปได้เพราะตัวสร้างประเภทเช่นสามารถผกผันได้ในอาร์กิวเมนต์: ·->·

α ~ β -> [γ] -> [δ] α ~ ε -> [ζ] -> [ι] ε ~ ζ -> ι 

แทนที่ζ -> ιด้วยεและβ -> [γ] -> [δ]ด้วย โดยαคงข้อจำกัดที่สองไว้เพื่อให้เราสามารถกู้คืนได้αในตอนท้าย:

α ~ (ζ -> ι) -> [ζ] -> [ι] β -> [γ] -> [δ] ~ (ζ -> ι) -> [ζ] -> [ι] 

และสุดท้าย การแทนที่(ζ -> ι)ด้วยβเช่นเดียวζกับγและιเนื่องจากδตัวสร้างประเภท เช่นสามารถผกผันได้จึงช่วยขจัดตัวแปรทั้งหมดที่เฉพาะเจาะจงกับข้อจำกัดที่สอง: [·]

α ~ (ζ -> ι) -> [ζ] -> [ι] 

ไม่สามารถทำการทดแทนเพิ่มเติมได้อีกแล้ว และการติดฉลากใหม่จะให้ผลลัพธ์เช่นเดียวกับที่เราพบโดยไม่ต้องลงรายละเอียดเหล่านี้ map::(a->b)->[a]->[b]

อัลกอริทึมที่ใช้ครั้งแรกในการอนุมานประเภทในปัจจุบันเรียกกันอย่างไม่เป็นทางการว่าอัลกอริทึม Hindley–Milner แม้ว่าอัลกอริทึมนี้ควรจะถูกยกให้เป็นผลงานของ Damas และ Milner อย่างถูกต้องก็ตาม^{[ 18 ]} นอกจากนี้ยังเรียกกันตามธรรมเนียมว่าการสร้างประเภทใหม่^{[ 1 ] : 320} หากเทอมใดมีประเภทที่ดีตามกฎการกำหนดประเภทของ Hindley–Milner กฎเหล่านั้นจะสร้างการกำหนดประเภทหลักสำหรับเทอมนั้น กระบวนการค้นหาการกำหนดประเภทหลักนี้คือกระบวนการ "การสร้างใหม่"

ที่มาของอัลกอริทึมนี้คืออัลกอริทึมการอนุมานประเภทสำหรับแคลคูลัสแลมบ์ดาแบบง่ายที่คิดค้นโดยHaskell CurryและRobert Feysในปี 1958 ในปี 1969 J. Roger Hindleyได้ขยายงานนี้และพิสูจน์ว่าอัลกอริทึมของพวกเขาอนุมานประเภททั่วไปที่สุดเสมอ ในปี 1978 Robin Milner [ ^{19 ] ได้}เสนออัลกอริทึมที่เทียบเท่ากันโดยอิสระจากงานของ Hindley ซึ่งก็คือAlgorithm Wในปี 1982 Luis Damas ^{[ 18 ]}ได้พิสูจน์ในที่สุดว่าอัลกอริทึมของ Milner นั้นสมบูรณ์และขยายเพื่อรองรับระบบที่มีการอ้างอิงแบบโพลีมอร์ฟิก

โดยปกติแล้ว การอนุมานประเภทจะอนุมานประเภททั่วไปที่เหมาะสมที่สุด อย่างไรก็ตาม ภาษาโปรแกรมหลายภาษา โดยเฉพาะภาษาโปรแกรมรุ่นเก่า มีระบบประเภทที่ไม่สมบูรณ์นัก ซึ่งการใช้ประเภททั่วไปอาจไม่ได้เป็นกลางทางอัลกอริทึมเสมอไป กรณีทั่วไปได้แก่:

• โดยทั่วไปแล้ว ประเภทเลขทศนิยมถือเป็นการขยายความของประเภทเลขจำนวนเต็ม แต่ในความเป็นจริงแล้ว การคำนวณเลขทศนิยมมีความแม่นยำและปัญหาเรื่องการวนรอบที่แตกต่างจากเลขจำนวนเต็ม
• ประเภทตัวแปร/ไดนามิกถูกพิจารณาว่าเป็นรูปแบบทั่วไปของประเภทอื่นในกรณีที่ส่งผลต่อการเลือกโอเวอร์โหลดของตัวดำเนินการ ตัวอย่างเช่น+ตัวดำเนินการอาจบวกจำนวนเต็ม แต่สามารถเชื่อมต่อตัวแปรเป็นสตริงได้ แม้ว่าตัวแปรเหล่านั้นจะมีค่าเป็นจำนวนเต็มก็ตาม

อัลกอริทึมการอนุมานประเภทถูกนำมาใช้ในการวิเคราะห์ภาษาธรรมชาติและภาษาโปรแกรม^{[ 20 ] [ 21 ] [ 22 ]}อัลกอริทึมการอนุมานประเภทยังถูกนำมาใช้ในการเหนี่ยวนำไวยากรณ์ บางระบบ ^{[ 23 ] [ 24 ]}และ ระบบ ไวยากรณ์ตามข้อจำกัดสำหรับภาษาธรรมชาติ^{[ 25 ]}

• ข้อความอีเมลที่เก็บถาวรโดย Roger Hindley อธิบายประวัติความเป็นมาของการอนุมานประเภท
• บทความ "Polymorphic Type Inference"โดย Michael Schwartzbach ให้ภาพรวมของการอนุมานประเภทแบบโพลีมอร์ฟิก (Polymorphic type inference)
• บทความเรื่อง "การตรวจสอบประเภทข้อมูลพื้นฐาน"โดย Luca Cardelli อธิบายอัลกอริทึม รวมถึงการนำไปใช้ในModula-2
• การนำการอนุมานประเภท Hindley–Milner มาใช้ในScalaโดย Andrew Forrest (สืบค้นเมื่อ 30 กรกฎาคม 2552)
• การนำ Hindley-Milner ไปใช้ใน Perl 5 โดย Nikita Borisovที่Wayback Machine (เก็บถาวรเมื่อวันที่ 18 กุมภาพันธ์ 2550)
• Hindley-Milner คืออะไร? (และทำไมมันถึงเจ๋ง?)อธิบาย Hindley-Milner พร้อมตัวอย่างใน Scala