Induktiiviset tyypit

Abstract

Induktiiviset tyypit ovat tapa mallintaa erilaisia tietotyyppejä kuten listoja, luonnollisia lukuja ja binäärihakupuita tyyppiteoriassa. Induktiivisia tyyppejä käytetään laajasti todistusassistenteissa erilaisten teoreemojen ja tietokoneohjelmien toteutukseen. Yleistys induktiivisista tyypeistä ovat korkeammat induktiiviset tyypit, jotka laajentavat induktiivisia tyyppejä mahdollistamalla tyypin alkioiden välisten ekvivalenssirelaatioiden määrittämisen. Tässä kirjallisuuskatsauksessa käsitellään induktiivisten ja korkeampien induktiivisten tyyppien teoriaa, niiden toteutuksia eri ohjelmointikielissä sekä erilaisia sovelluskohteita.

Inductive types are a way to represent complex datatypes such as lists, natural numbers and binary search trees in type theory. Inductive types are currently widely used in proof assistants to implement mathematical theorems and computer programs. A generalization of inductive types are higher inductive types, which extend inductive types by making it possible to define equivalence relations between inhabitants of a type. This thesis explores theory behind inductive and higher inductive types, their implementations in different programming languages and their use cases.