Curios - a web of types

Abstract

Ever since their inception lambda calculus and type theory have been such an influence in the design of modern programming languages so much so that even programming lan guages outside of the functional circle have adopted its practices. But even inside the functional circle, not many programming languages have dared to venture beyond the higher order polymorphic lambda calculus, towards the calculus of constructions: it can be troublesome to incorporate dependent types into a more traditional type system without constraining the calculus in some way, and these constraints usually lead to the calculus not being a good theoretical foundation for a programming language. However, program ming languages like Idris and Agda have proven that there exists benefits in bringing full, unrestricted dependent types to the type system of functional programming languages. Despite the advances that these programming languages have achieved in the research surrounding advanced type systems, they do not target an executable format and, for the purposes of execution, choose to transpile their programs into other programming languages. While transpilation has its advantages, it also has its drawbacks: the program ming language now depends on the compiler toolchain of a second, separate programming language. This gives rise to a question: would it be desirable to compile a dependently typed programming language to an executable format without indirection? In the present research project we explore the topic of compiling Curios, a dependently typed functional programming language to WebAssembly, a binary instruction format for a stack-based virtual machine. We describe Curios through practical examples showcas ing its syntax and basic features, and how to represent more complex concepts by using its basic features as building blocks. The type system of Curios is formally specified next, and following that we give a detailed explanation on the inner workings of the com piler, from source code to executable. We conclude by presenting the bodies of work that have influenced Curios, what was achieved and what was left as topics for future research.

Desde o seu princípio o cálculo lambda e a teoria dos tipos têm sido uma influência tão grande no design de linguagens de programação modernas que mesmo linguagens de programação fora do círculo funcional adotaram as suas práticas. Mas mesmo dentro do círculo funcional, não existem muitas linguagens de programação que se atreveram a se aventurar além do cálculo lambda polimórfico de order maior, em direção ao cálculo das construções: pode ser problemático incorporar tipos dependentes em um sistema de tipos mais tradicional sem restringir o cálculo de alguma forma, e estas restrições normal mente fazem o cálculo não ser uma fundamentação teórica tão boa para uma linguagem de programação. No entanto, linguagens de programação como Idris e Agda provaram que existem benefícios em trazer tipos dependentes completos e irrestritos para o sistema de tipos de linguagens de programação funcionais. Apesar dos avanços que estas linguagens de programação conquistaram na pesquisa em torno de sistemas de tipos avançados, elas não têm como alvo um formato executável e, com o objetivo de serem executadas, escolhem transpilar os seus programas para outras linguagens de programação. Embora a transpilação tenha as suas vantagens, ela também tem suas desvantagens: a linguagem de programação acaba por depender das ferramentas de compilação de uma segunda, distinta linguagem de programação. Isso levanta uma pergunta: seria desejável compilar uma linguagem de programação para um formato exe cutável sem indireção? No presente projeto de pesquisa exploramos o tópico de compilar Curios, uma linguagem de programação dependentemente tipada para WebAssembly, um formato de instruções binárias para uma máquina virtual baseada em pilhas. Descrevemos Curios atráves de exemplos práticos demonstrando a sua sintaxe e funcionalidades básicas, e como repre sentar conceitos mais complexos usando as suas funcionalidades básicas como ingredi entes modulares. O sistema de tipos de Curios é formalmente especificado por próximo, e em seguida damos uma descrição detalhada das operações internas do compilador, de código fonte até executável. Concluímos apresentando os trabalhos que influenciaram Curios, o que foi alcançado e o que foi deixado como tópico para pesquisa futura.