類型推理是指在形式語言中自動檢測表達式的類型。這些語言包括編程語言和數學類型系統，但也包括計算機科學和語言學某些分支中的自然語言。

從最普遍的觀點來看，類型可以與指定的用途相關聯，建議并限制該類型的對象可能的活動。語言中的許多名詞都規定了這種用途。例如，皮帶這個詞表示的是與線這個詞不同的用途。稱某物為桌子，與稱其為木柴，表明了另一種指定，盡管它在物質上可能是同樣的東西。雖然它們的物質屬性使事物可以用于某些目的，但它們也是特定稱呼的對象。這在抽象領域，即數學和計算機科學中尤其如此，在這些領域中，物質最終只是比特或公式。

在類型劃分中，一個表達式E與一個類型T相對，正式寫成E:通常，類型化只在某些上下文中才有意義，這里省略不談。在這種情況下，下面的問題是特別值得關注的。E:T在這種情況下，表達式E和類型T都被給出。

類型是一些強靜態類型語言中的一個特征。它通常是一般功能性編程語言的特征。一些包含類型推理的語言包括C++11、C#（從3.0版開始）、Chapel、Clean、Crystal、D、F#、FreeBASIC、Go、Haskell、Java（從10版開始）、Julia、Kotlin、ML、Nim、OCaml、Opa、Q#、RPython、Rust、Scala、Swift、TypeScript、Vala、Dart和VisualBasic（從9版開始。它們中的大多數使用簡單的類型推理形式；Hindley-Milner類型系統可以提供更完整的類型推理。