ในวิทยาการคอมพิวเตอร์และตรรกศาสตร์ประเภท ที่ขึ้นอยู่กับค่า (dependent type)คือประเภทที่นิยามของมันขึ้นอยู่กับค่า มันเป็นคุณลักษณะที่ทับซ้อนกันระหว่างทฤษฎีประเภท (type theory)และระบบประเภท (type systems ) ในทฤษฎีประเภทแบบสัญชาตญาณ (intuitionistic type theory)ประเภทที่ขึ้นอยู่กับค่าถูกใช้เพื่อเข้ารหัสตัวบ่งปริมาณ ของตรรกศาสตร์ เช่น "สำหรับทุก" (for all) และ "มีอยู่" (there exists) ในภาษาการเขียนโปรแกรมเชิงฟังก์ชัน เช่นAgda , ATS , Rocq (เดิมชื่อCoq ), F* , Epigram , IdrisและLeanประเภทที่ขึ้นอยู่กับค่าช่วยลดข้อผิดพลาดโดยการทำให้นักเขียนโปรแกรมสามารถกำหนดประเภทที่จำกัดชุดของการใช้งานที่เป็นไปได้เพิ่มเติมได้

ตัวอย่างทั่วไปสองอย่างของประเภทที่ขึ้นอยู่กันคือฟังก์ชันที่ขึ้นอยู่กันและคู่ที่ขึ้นอยู่กันประเภทการส่งคืนของฟังก์ชันที่ขึ้นอยู่กันอาจขึ้นอยู่กับค่า (ไม่ใช่แค่ประเภท) ของอาร์กิวเมนต์ตัวใดตัวหนึ่ง เช่น ฟังก์ชันที่รับจำนวนเต็มบวกอาจส่งคืนอาร์เรย์ที่มีความยาวโดยที่ความยาวของอาร์เรย์เป็นส่วนหนึ่งของประเภทของอาร์เรย์ (โปรดทราบว่านี่แตกต่างจากโพลีมอร์ฟิซึมและการเขียนโปรแกรมแบบเจเนริกซึ่งทั้งสองอย่างนี้รวมประเภทเป็นอาร์กิวเมนต์ด้วย) คู่ที่ขึ้นอยู่กันอาจมีค่าที่สอง ซึ่งประเภทของค่าที่สองนั้นขึ้นอยู่กับค่าแรก ยกตัวอย่างเช่น อาร์เรย์ คู่ที่ขึ้นอยู่กันอาจใช้เพื่อจับคู่อาร์เรย์กับความยาวของมันในลักษณะที่ปลอดภัยต่อประเภท ${\displaystyle n}$${\displaystyle n}$

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

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

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

ด้วยเหตุนี้ และจากผลงานอื่นๆ ของฮาวาร์ด แนวคิดเรื่องข้อเสนอในฐานะประเภท จึงถูกเรียกว่า การสอดคล้องกันระหว่างเคอร์รีและฮาวาร์ด (Curry–Howard correspondence )

ในทฤษฎีประเภทแบบพึ่งพา (dependent type theory) ประเภทแบบพึ่งพาคือประเภทที่ข้อกำหนดอาจเปลี่ยนแปลงไปตามค่า และสามารถมองได้ว่าคล้ายคลึงกับตระกูลของเซตที่มีดัชนี ให้ แทนเอกภพของประเภท และเขียนเพื่อระบุว่าเป็นประเภทในสำหรับเทอมของประเภทเขียนตระกูลของประเภทแบบพึ่งพาบนเขียนซึ่งหมายความว่าสำหรับแต่ละเทอมตระกูลจะกำหนดประเภทดังนั้น เมื่อกำหนดและนิพจน์จะหมายถึงประเภทที่ขึ้นอยู่กับค่าเฉพาะนั้นในศัพท์เฉพาะมาตรฐาน จะอธิบายสิ่งนี้โดยการกล่าวว่าประเภทเปลี่ยนแปลงไปตาม ${\displaystyle {\คณิตศาสตร์ {U}}}$${\displaystyle A:{\คณิตศาสตร์ {U}}}$${\displaystyle A}$${\displaystyle {\mathcal {U}}}$${\displaystyle a}$${\displaystyle A}$${\displaystyle a:A}$${\displaystyle A}$${\displaystyle B:A\to {\mathcal {U}}}$${\displaystyle a:A}$${\displaystyle B(a):{\mathcal {U}}}$${\displaystyle A:{\mathcal {U}}}$${\displaystyle B:A\to {\mathcal {U}}}$${\displaystyle B(a)}$${\displaystyle a}$${\displaystyle B(a)}$${\displaystyle a}$

ฟังก์ชันที่มีประเภทของค่าส่งคืนแปรผันตามอาร์กิวเมนต์ (กล่าวคือไม่มีโคโดเมน คงที่ ) เรียกว่าฟังก์ชันขึ้นอยู่และประเภทของฟังก์ชันนี้เรียกว่าประเภทผลคูณขึ้นอยู่ประเภทพาย ( ประเภทΠ ) หรือประเภทฟังก์ชันขึ้นอยู่ [ ^{4 ] จาก}ตระกูลของประเภทเราสามารถสร้างประเภทของฟังก์ชันขึ้นอยู่ซึ่งเทอมต่างๆ เป็นฟังก์ชันที่รับเทอมและส่งคืนเทอมในสำหรับตัวอย่างนี้ ประเภทฟังก์ชันขึ้นอยู่มักจะเขียนเป็น หรือ${\displaystyle B:A\to {\mathcal {U}}}$${\textstyle \prod _{x:A}B(x)}$${\displaystyle a:A}$${\displaystyle B(a)}$${\textstyle \prod _{x:A}B(x)}$${\textstyle \prod {(x:A)}B(x)}$

ถ้าเป็นฟังก์ชันคงที่ ประเภทผลคูณแบบขึ้นอยู่ที่สอดคล้องกันจะเทียบเท่ากับประเภทฟังก์ชัน ธรรมดา นั่นคือมีค่าเท่ากันโดยพิจารณาจากเมื่อไม่ขึ้นอยู่กับ ${\displaystyle B:A\to {\mathcal {U}}}$${\textstyle \prod _{x:A}B}$${\displaystyle A\to B}$${\displaystyle B}$${\displaystyle x}$

ชื่อ 'Π-type' มาจากแนวคิดที่ว่าสิ่งเหล่านี้สามารถมองได้ว่าเป็นผลคูณคาร์ทีเซียน ของประเภทต่างๆ นอกจาก นี้ Π-type ยังสามารถเข้าใจได้ว่าเป็นแบบจำลองของตัวบ่งปริมาณสากล

ตัวอย่างเช่น ถ้าเราเขียนสำหรับ ทูเปิล nตัวของจำนวนจริงแล้วจะเป็นประเภทของฟังก์ชันซึ่งเมื่อกำหนดจำนวนธรรมชาติnจะส่งคืนทูเปิลของจำนวนจริงที่มีขนาดnพื้นที่ฟังก์ชันปกติเกิดขึ้นเป็นกรณีพิเศษเมื่อประเภทของช่วงไม่ขึ้นอยู่กับอินพุต เช่นคือประเภทของฟังก์ชันจากจำนวนธรรมชาติไปยังจำนวนจริง ซึ่งเขียนเป็นในแคลคูลัสแลมบ์ดาแบบมีประเภท ${\displaystyle \operatorname {Vec} (\mathbb {R} ,n)}$${\textstyle \prod _{n:\mathbb {N} }\operatorname {Vec} (\mathbb {R} ,n)}$${\textstyle \prod _{n:\mathbb {N} }{\mathbb {R} }}$${\displaystyle \mathbb {N} \to \mathbb {R} }$

เพื่อให้ได้ตัวอย่างที่ชัดเจนยิ่งขึ้น สมมติว่าเป็นชนิดของจำนวนเต็มที่ไม่ติดลบตั้งแต่ 0 ถึง 255 (จำนวนที่พอดีกับ 8 บิตหรือ 1 ไบต์) และสำหรับแล้วจะกลายเป็นผลคูณของ ${\displaystyle A}$${\displaystyle B(a)=X_{a}}$${\displaystyle a:A}$${\textstyle \prod _{x:A}B(x)}$${\displaystyle X_{0}\times X_{1}\times X_{2}\times \ldots \times X_{253}\times X_{254}\times X_{255}}$

คู่ตรงข้ามของประเภทผลคูณแบบพึ่งพาคือประเภทคู่แบบพึ่งพาประเภท ผลรวม แบบพึ่งพาประเภทซิกมาหรือ (อย่างสับสน) ประเภทผลคูณแบบพึ่งพา [ ^{4 ] ประเภท}ซิกมายังสามารถเข้าใจได้ว่าเป็นตัวบ่งชี้ปริมาณเชิงมีอยู่จริงจากตัวอย่างข้างต้น หากในเอกภพของประเภทมีประเภทและตระกูลของประเภทแล้วจะมีประเภทคู่แบบพึ่งพา(สัญลักษณ์ทางเลือกจะคล้ายกับ ประเภท Π ) ${\displaystyle {\mathcal {U}}}$${\displaystyle A:{\mathcal {U}}}$${\displaystyle B:A\to {\mathcal {U}}}$${\textstyle \sum _{x:A}B(x)}$

ประเภทคู่ที่ขึ้นอยู่กันจะรวบรวมแนวคิดของคู่ลำดับที่ประเภทของพจน์ที่สองขึ้นอยู่กับค่าของพจน์แรก ถ้าแล้วและถ้าเป็นฟังก์ชันคงที่ ประเภทคู่ที่ขึ้นอยู่กันจะกลายเป็น (ถือว่าเท่ากับ) ประเภทผลคูณนั่นคือ ผลคูณคาร์ทีเซียนธรรมดา^{[ 4 ]}${\textstyle (a,b):\sum _{x:A}B(x),}$${\displaystyle a:A}$${\displaystyle b:B(a)}$${\displaystyle B}$${\displaystyle A\times B}$

สำหรับตัวอย่างที่เป็นรูปธรรมมากขึ้น โดยกำหนดให้ เป็นจำนวนเต็มที่ไม่ติดลบตั้งแต่ 0 ถึง 255 และให้เท่ากับสำหรับค่า 256 ที่กำหนดขึ้น เอง ก็จะ ได้ผลลัพธ์เป็น ผล รวม${\displaystyle A}$${\displaystyle B(a)}$${\displaystyle X_{a}}$${\displaystyle X_{a}}$${\textstyle \sum _{x:A}B(x)}$${\displaystyle X_{0}+X_{1}+X_{2}+\ldots +X_{253}+X_{254}+X_{255}}$

ให้เป็นชนิดข้อมูลบางประเภท และให้โดยความสัมพันธ์แบบเคอร์รี-ฮาวาร์ดสามารถตีความได้ว่าเป็น述语เชิงตรรกะ ในแง่ของสำหรับค่า ที่กำหนดให้ การที่ ชนิดข้อมูล นั้น มีอยู่หรือไม่ บ่งชี้ว่า สอดคล้องกับ述语นี้หรือไม่ ความสัมพันธ์นี้สามารถขยายไปสู่การกำหนดปริมาณเชิงมีอยู่และคู่ที่ขึ้นอยู่กันได้ กล่าวคือ ข้อเสนอจะเป็นจริงก็ต่อเมื่อชนิดข้อมูลนั้นมีอยู่ ${\displaystyle A:{\mathcal {U}}}$${\displaystyle B:A\to {\mathcal {U}}}$${\displaystyle B}$${\displaystyle A}$${\displaystyle a:A}$${\displaystyle B(a)}$${\displaystyle a}$${\displaystyle \exists {a}{\in }A\,B(a)}$${\textstyle \sum _{a:A}B(a)}$

ตัวอย่างเช่นน้อยกว่าหรือเท่ากับก็ต่อเมื่อมีจำนวนธรรมชาติอีกจำนวนหนึ่ง ที่ทำให้ เป็น เช่นนั้นในตรรกศาสตร์ ข้อความนี้ถูกบันทึกไว้โดยการกำหนดปริมาณเชิงมีอยู่ (existential quantification): ${\displaystyle m:\mathbb {N} }$${\displaystyle n:\mathbb {N} }$${\displaystyle k:\mathbb {N} }$${\displaystyle m+k=n}$

$${\displaystyle m\leq n\iff \exists {k}{\in }\mathbb {N} \,m+k=n.}$$

ข้อเสนอแนะนี้สอดคล้องกับประเภทคู่ที่ขึ้นอยู่กัน:

$${\displaystyle \sum _{k:\mathbb {N} }m+k=n.}$$

กล่าวคือ การพิสูจน์ข้อความที่ว่า น้อยกว่าหรือเท่ากับคือคู่ที่ประกอบด้วยจำนวนที่ไม่เป็นลบซึ่งเป็นผลต่างระหว่างและและการพิสูจน์ความเท่าเทียมกัน ${\displaystyle m}$${\displaystyle n}$${\displaystyle k}$${\displaystyle m}$${\displaystyle n}$${\displaystyle m+k=n}$

Henk Barendregtได้พัฒนาlambda cubeขึ้นมาเพื่อใช้ในการจัดประเภทระบบประเภทตามแกนสามแกน มุมทั้งแปดของแผนภาพรูปทรงลูกบาศก์ที่ได้นั้นแต่ละมุมจะสอดคล้องกับระบบประเภทหนึ่งๆ โดยที่แคลคูลัสแลมบ์ดาแบบกำหนดประเภทอย่างง่ายจะอยู่ในมุมที่มีการแสดงออกน้อยที่สุด และแคลคูลัสของการสร้างจะอยู่ในมุมที่มีการแสดงออกมากที่สุด แกนทั้งสามของลูกบาศก์สอดคล้องกับการเพิ่มเติมที่แตกต่างกันสามแบบของแคลคูลัสแลมบ์ดาแบบกำหนดประเภทอย่างง่าย ได้แก่ การเพิ่มประเภทที่ขึ้นอยู่กัน การเพิ่มพหุรูป และการเพิ่ม ตัวสร้างประเภท ที่มีชนิด ที่สูงกว่า (เช่น ฟังก์ชันจากประเภทหนึ่งไปยังอีกประเภทหนึ่ง) lambda cube ได้รับการขยายความเพิ่มเติมโดยระบบประเภทบริสุทธิ์

ระบบของประเภทพึ่งพาอันดับแรกบริสุทธิ์ ซึ่งสอดคล้องกับกรอบตรรกะLF นั้นได้มาจากการขยายประเภทพื้นที่ฟังก์ชันของแคลคูลัสแลมบ์ดาแบบง่ายไปสู่ประเภทผลคูณพึ่งพา ${\displaystyle \lambda \Pi }$

ระบบของประเภทพึ่งพาอันดับสองได้มาจากการอนุญาตให้มีการกำหนดปริมาณเหนือตัวสร้างประเภท ในทฤษฎีนี้ ตัวดำเนินการผลคูณแบบพึ่งพาครอบคลุมทั้งตัวดำเนินการของแคลคูลัสแลมบ์ดาแบบง่าย และตัวผูกของระบบ F ${\displaystyle \lambda \Pi 2}$${\displaystyle \lambda \Pi }$${\displaystyle \to }$${\displaystyle \forall }$

ระบบลำดับสูงกว่าขยายไปสู่รูปแบบนามธรรมทั้งสี่รูปแบบจากลูกบาศก์แลมบ์ดาได้แก่ ฟังก์ชันจากเทอมไปยังเทอม ประเภทไปยังประเภท เทอมไปยังประเภท และประเภทไปยังเทอม ระบบนี้สอดคล้องกับแคลคูลัสของการสร้างซึ่งอนุพันธ์ของมัน คือแคลคูลัสของการสร้างแบบอุปนัยเป็นระบบพื้นฐานของ Rocq ${\displaystyle \lambda \Pi \omega }$${\displaystyle \lambda \Pi 2}$

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

• แคลคูลัสแลมบ์ดาแบบพิมพ์
• ทฤษฎีประเภทสัญชาตญาณนิยม
• ออกแบบตามสัญญา

• การเขียนโปรแกรมแบบกำหนดประเภทตามตัวแปร 2008
• การเขียนโปรแกรมแบบกำหนดประเภทข้อมูลโดยอาศัยความสัมพันธ์ 2010
• การเขียนโปรแกรมแบบกำหนดประเภทตามการพึ่งพา 2011
• "Dependent type"ใน Haskell Wiki
• ทฤษฎีประเภทที่ขึ้นอยู่กับที่n Lab
• ประเภทที่ขึ้นอยู่กับที่ห้องปฏิบัติการn
• ประเภทผลิตภัณฑ์ที่ขึ้นอยู่กับที่ห้องปฏิบัติการn
• ประเภทผลรวมที่ขึ้นอยู่กันที่n Lab
• ผลิตภัณฑ์ที่ขึ้นอยู่กับที่ห้องปฏิบัติการn
• ผลรวมที่ขึ้นอยู่กันที่n Lab