Dlaczego Martin-Löf potrzebował stworzyć intuicyjną teorię typów?

Czytałem o Intuitionistic Type Theory (ITT) i to ma sens. Ale staram się zrozumieć, dlaczego „dlaczego” zostało stworzone?

Intuicyjna logika (IL) i prosty typ rachunek (STLC) i teoria typów ogólnie poprzedzają samo istnienie samego Martina-Löfa! Wydaje się, że w STLC można zrobić wszystko, co jest możliwe w ITT (mogę się mylić, ale przynajmniej tak się czuje). $\lambda$

Czym więc była „nowość” w ITT i jak dokładnie (lub czy) rozwinęła teorię obliczeń? Z tego, co rozumiem, wprowadził pojęcie „typów zależnych”, ale wydaje się, że były one już w pewnym sensie w STLC. Czy jego ITT była próbą abstrakcji, aby zrozumieć razem podstawowe zasady STLC i IL? Ale czy STLC już tego nie zrobiło? Dlaczego w ogóle stworzono ITT? Jaki był / miał sens?

Oto fragment z Wikipedii : Ale wciąż nie mam powodu, dla którego nie powstał wcześniej.

Pierwszy szkic artykułu Martina-Löfa na temat teorii typów pochodzi z 1971 roku. Ta impredykatywna teoria uogólniła system F. Girarda. Jednak system ten okazał się niespójny ze względu na paradoks Girarda, który odkrył Girard podczas badania Systemu U, niespójnego rozszerzenia Systemu F. Doświadczenie to doprowadziło Per Martina-Löfa do opracowania filozoficznych podstaw teorii typów, wyjaśnienia jego znaczenia, formy semantyki dowodowej, która uzasadnia predykatywną teorię typów, przedstawioną w jego książce Bibliopolis z 1984 roku ...

Z fragmentu wydaje się, że powodem było rozwinięcie „ filozoficznych podstaw teorii typów ” - myślałem, że ten fundament już istnieje (a może tak przypuszczałem). Czy to był zatem główny powód?

$\lambda$

• Wykorzystanie reguły Leibniza dotyczącej tożsamości nierozróżnialnych do zakodowania równości zdań. Takie podejście jest stosowane w rachunku konstrukcji, ale wymaga impredykatywnych wszechświatów, które zostały odrzucone przez Martina-Löfa z powodów filozoficznych.

• Bezpośrednia konstruktywna charakterystyka równości. Nadanie takiej charakterystyki przy użyciu typów tożsamości może być główną nowością intuicyjnej teorii typów Martina-Löfa.

Typy tożsamości wydają się dziś zwodniczo proste, ale ponownie skupiły się na zrozumieniu teorii typów częściowo dlatego, że dały początek intrygującym pytaniom semantycznym, takim jak: czy dowody tożsamości są unikalne? W pewnym sensie pytanie to prowadzi do teorii typu homotopii i aksjomatu jedności (który jest niezgodny z wyjątkowością tożsamości). Hofmann i Streicher pokazali, że wyjątkowości dowodów tożsamości nie da się wyprowadzić z intuicyjnej teorii typów Martina-Löfa w: „Grupoidoidalna interpretacja teorii typów”. Nawiasem mówiąc, wynik ten pokazuje również, że dopasowanie wzorca nie jest konserwatywnym rozszerzeniem tradycyjnej teorii typów.