An Agda Formalisation of Modalities and Erasure in a Dependently Typed Language

Abstract

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.