SHF: Small: Typed Self-Application

点击翻译按钮获取中文摘要

Static type checking has brought us more reliable software. Types make programs more readable, prevent entire classes of mistakes, and help compilers optimize data layout and data access. Types also make it easier to use libraries and to design interfaces, and they make it harder to misuse data and write bad programs. An entirely different trend is as old as programming: self-application. In particular, self-application is popular in the form of implementing a language in itself. When the trends of types and self-application meet, a fundamental challenge for type systems arises. For example, what is the type of an interpreter that can interpret a representation of itself? And what is the type of a compiler that can compile a representation of itself? The goal of the project is to enable the next generation of typed, self-applicable interpreters, compilers, and partial evaluators. This next generation will guarantee that the output represents a typed program, and that the type of the output program is related to the type of the input program. The result will be self-applicable meta-programs that are more reliable and have all the benefits of static type checking.Many popular languages have a self-interpreter, that is, an interpreter for the language written in itself; examples include Standard ML, Haskell, Scheme, JavaScript, Python, and Ruby. Similarly, many languages have self-compilers, that is, a compiler for the language written in itself. Also, some languages have a virtual machine written in itself, including Java and Self. The project will bring static type checking to self-applicable interpreters, compilers, and partial evaluators, and take such meta-programs to a higher level of reliability by ensuring that the output programs type check and therefore cannot contain entire classes of mistakes. The investigator will teach the results to students as part of existing undergraduate and graduate courses.