An Agda Formalisation of Modalities and Erasure in a Dependently Typed Language
Ladda ner
Typ
Examensarbete för masterexamen
Program
Publicerad
2021
Författare
Eriksson, Oskar
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
Modal types extend the expressivity of types by giving them different interpretations
depending on the used modality. In this thesis, we develop a general modality
structure in the setting of a dependently typed language, notably containing dependent
products and sums as well as natural numbers, based on the work of Abel and
Bernardy [1]. The modality structure is based on a semiring, the elements of which
are used as annotations on terms and whose algebraic properties form the basis for
the modal type system.
In addition, we instantiate the general modality structure to a modality for erasure
in which annotations are interpreted as either computationally relevant, indicating
that the annotated term is used during evaluation, or computationally irrelevant,
indicating that the marked term is not useful during evaluation. Based on this
interpretation, we define an extraction function that translates terms to an untyped
lambda calculus, removing terms that have been marked for erasure. Using a logical
relation between terms of the two languages we then prove the extraction function
to be sound with respect to the semantics of the languages in the special case of
natural numbers.
Beskrivning
Ämne/nyckelord
modal type theory , Martin-Löf type theory , erasure , logical relation , modalities , Agda