Чистая система типов

Чистая система типов (система обобщенных типов) — форма типизированного лямбда-исчисления, допускающая произвольное количество сортов переменных и зависимостей между ними. Разработана независимо Стефано Берарди (1988) и Яном Терловым (1989)^[1]^[2].

Чистую систему типов можно рассматривать как обобщение лямбда-куба, подразумевая, что каждой из его вершин соответствует экземпляр чистой системы типов с двумя сортами переменных^[1]^[2] (подобный взгляд высказывал автор идеи лямбда-куба Барендрегт^[3]).

ПримечанияПравить

↑ ¹ ² Pierce, Benjamin C. Types and programming languages. — Cambridge, Mass.: MIT Press, 2002. — 1 с. — ISBN 0-585-44269-X, 978-0-585-44269-3, 0-262-25681-9, 978-0-262-25681-0, 9786612096693, 6612096691, 1-282-09669-9, 978-1-282-09669-1, 0-262-30382-5, 978-0-262-30382-8.
↑ ¹ ² Kamareddine, Fairouz D. A modern perspective on type theory : from its origins until today. — Dordrecht: Kluwer Academic Publishers, 2004. — 1 с. — ISBN 1-4020-2334-0, 978-1-4020-2334-7, 1-4020-2335-9, 978-1-4020-2335-4.
↑ Henk Barendregt. Introduction to generalized type systems (англ.) // Journal of Functional Programming. — 1991/04. — Vol. 1, iss. 2. — P. 125–154. — ISSN 1469-7653 0956-7968, 1469-7653. — doi:10.1017/S0956796800020025.

[:0-1] ¹ ² Pierce, Benjamin C. Types and programming languages. — Cambridge, Mass.: MIT Press, 2002. — 1 с. — ISBN 0-585-44269-X, 978-0-585-44269-3, 0-262-25681-9, 978-0-262-25681-0, 9786612096693, 6612096691, 1-282-09669-9, 978-1-282-09669-1, 0-262-30382-5, 978-0-262-30382-8.

[:1-2] ¹ ² Kamareddine, Fairouz D. A modern perspective on type theory : from its origins until today. — Dordrecht: Kluwer Academic Publishers, 2004. — 1 с. — ISBN 1-4020-2334-0, 978-1-4020-2334-7, 1-4020-2335-9, 978-1-4020-2335-4.

[3] Henk Barendregt. Introduction to generalized type systems (англ.) // Journal of Functional Programming. — 1991/04. — Vol. 1, iss. 2. — P. 125–154. — ISSN 1469-7653 0956-7968, 1469-7653. — doi:10.1017/S0956796800020025.

[1]

[2]

[3]