Переменная типа (ти́повая переменная) в языках программирования и теории типов — переменная, которая может принимать значение из множества типов данных.
Ти́повая переменная используется в определении алгебраического типа данных подобно тому, как используется параметр в определении функции, но используется для передачи типа данных без передачи самих данных. В качестве идентификаторов ти́повых переменных в теории типов традиционно используются буквы греческого алфавита (хотя многие языки программирования используют латиницу и допускают и более длинные именования).
В следующем определении полиморфного типа «список» на языке Standard ML, идентификатор 'a
(читается «альфа») является переменной типа[2]:
При использовании этого полиморфного типа, в ти́повую переменную подставляется конкретный тип, так что в программе может быть сформировано множество мономорфных типов: string list
, int list
, int list list
и так далее. При такой подстановке, вместо каждого упоминания переменной типа подставляется один и тот же тип. Полученная информация о типах используется для верификации и оптимизации программы, после чего обычно стирается, так что один и тот же целевой код обрабатывает объекты изначально разных типов (но существуют и исключения из этого правила, в частности, в MLton).
Если полиморфный тип параметризован несколькими переменными типа, то подставляемые в них типы могут быть как разными, так и идентичными, но правило подстановки соблюдается. Например, если такой тип:
то Single(4)
, Double(4,5)
и Pair(4,5.0)
будут допустимыми значениями типа t_ir
, а попытка построить значение Single(5.0)
приведёт к ошибке типизации, поскольку параметр 'a
получил значение «int
».