在計算機科學和邏輯學中，從屬類型是一種類型，其定義取決于一個值。它是類型理論和類型系統的一個重疊的特征。在直覺類型理論中，從屬類型被用來編碼邏輯的量詞，如forall和thereexists。在Agda、ATS、Coq、F*、Epigram和Idris等函數式編程語言中，從屬類型通過讓程序員分配類型來進一步限制可能的實現集，從而幫助減少錯誤。依賴類型的兩個常見例子是依賴函數和依賴對。從屬函數的返回類型可能取決于它的一個參數的值（不僅僅是類型）。例如，一個函數取一個正整數，其中數組的長度是數組類型的一部分。(注意，這與多態性和泛型編程不同，兩者都將類型作為一個參數。）一個依賴對可能有第二個值，其類型取決于xxx個值。堅持以數組為例，依賴對可以用來以類型安全的方式將一個數組與它的長度配對。從屬類型增加了類型系統的復雜性。在一個程序中決定從屬類型的平等性可能需要進行計算。如果在從屬類型中允許任意的值，那么決定類型平等可能涉及到決定兩個任意程序是否產生相同的結果；因此類型檢查可能變得不可判定。歷史在1934年，HaskellCurry注意到，在類型化lambdacalculus中使用的類型，以及在它的組合邏輯對應物中使用的類型，遵循著與命題邏輯中公理相同的模式。進一步說，對于邏輯中的每個證明，在編程語言中都有一個匹配的函數（術語）。庫里的例子之一是簡單類型的λ微積分和直覺邏輯之間的對應關系。謂詞邏輯是命題邏輯的擴展，增加了量詞。Howard和deBruijn擴展了lambdacalculus以匹配這種更強大的邏輯，他們為依賴函數和依賴對創建了類型，前者對應于forall，后者對應于thereexists。(由于霍華德的這項工作和其他工作，命題即類型被稱為庫里-霍華德的對應關系）。

Π類型寬泛地說，依賴類型類似于集合的索引族的類型。更正式地說，給定一個類型一個函數的返回值類型隨其參數的變化而變化（即沒有固定的模域），是一個依賴函數，這個函數的類型被稱為依賴積類型、π類型（Π類型）或依賴函數類型。從一個類型的家族中{displaystyleB:Ato{mathcal{U}}是一個常數函數。｝是一個常數函數，相應的依存積類型就等同于一個普通的函數類型。就是說Π型"這個名字來自于這樣的想法：這些類型可以被看作是類型的笛卡爾乘積。Π-類型也可以被理解為通用量詞的模型。

例如，如果我們寫表示實數的n個元組，那么{textstyleprod_{n:mathbb{N}}operatorname{Vec}(mathbb{R},n)}。}/operatorname{Vec}(`mathbb{R},n)}將是一個函數的類型，該函數給定自然數n，返回實數元組。這將是一個函數的類型，給定一個自然數n，返回一個大小為n的實數元組。例如{displaystyle}{mathbb{N}}是自然數到實數的函數類型，寫成N→Rto`mathbb{R}}。在類型化的lambda計算中。