Typy W vs typy indukcyjne

Teoria typów Martina-Löfa wykorzystuje typy W do definiowania struktur indukcyjnych, takich jak liczby całkowite, listy itp. Jednak rachunek konstrukcji indukcyjnych nie używa ich w ten sam sposób, typy indukcyjne wydają się być bardziej podobne do schematów aksjomatycznych.

Czy te dwa podejścia są równoważne (wydają się być)? Czy są jakieś filozoficzne powody, dla których jedno jest lepsze od drugiego (dla mnie typy W wydają się być bardziej intuicyjne, ponieważ są tylko drzewami o specjalnej strukturze)? Co jest łatwiejsze z punktu widzenia wdrożenia (typy indukcyjne wydają mi się lepsze, ponieważ aby typy W były przydatne, potrzebujemy co najmniej typów skończonych i produktów dostępnych w rdzeniu systemu)

(Zakładam, że przez „schematy aksjomatyczne” masz na myśli pracę Gimeneza )

Ponadto typy W i schematy aksjomatyczne Gimeneza są równoważne.

Jednak w ustawieniach intensywnych nie posuniesz się daleko z typami W: są one zbyt ekstensywne (z samej definicji kodowania), aby nadawać się do programowania. Zostało to omówione przez kilku autorów, w szczególności:

• Conor McBride: http://mazzo.li/epilogue/index.html%3Fp=324.html
• Peter Dybjer, „Reprezentowanie zbiorów zdefiniowanych indukcyjnie przez uporządkowanie w teorii typów Martina-Löfa”
• Guogen & Luo, „Indukcyjne typy danych: ponownie sprawdzono typy porządkowe”