A focused solution to the avoidance problem. (6th August 2020)

• Record Type: Journal Article
• Authors: CRARY, KARL
• Is Part Of: Journal of functional programming. Volume 30(2020)
• Publication Date: 2020-08-06
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796820000222
• Languages: English
• ISSNs: 0956-7968

Abstract

Abstract: In ML-style module type theory, sealing often leads to situations in which type variables must leave scope, and this creates a need for signatures that avoid such variables. Unfortunately, in general, there is no best signature that avoids a variable, so modules do not always enjoy principal signatures. This observation is called the avoidance problem. In the past, the problem has been circumvented using a variety of devices for moving variables so they can remain in scope. These devices work, but have heretofore lacked a logical foundation. They have also lacked a presentation in which the dynamic semantics is given on the same phrases as the static semantics, which limits their applications. We can provide a best supersignature avoiding a variable by fiat, by adding an existential signature that is the least upper bound of its instances. This idea is old, but a workable metatheory has not previously been worked out. This work resolves the metatheoretic issues using ideas borrowed from focused logic. We show that the new theory results in a type discipline very similar to the aforementioned devices used in prior work. In passing, this gives a type-theoretic justification for the generative stamps used in the early days of the static semantics of ML modules. All the proofs are formalized in Coq.