Simulador para o cubo lambda estendido com tipos indutivos

Abstract

A compreensão de Cálculo Lambda e Teoria dos Tipos é importante para entender com mais profundidade os fundamentos tanto de linguagens funcionais modernas como de ferramentas assistentes de prova. Ao longo dos anos uma série de propostas de cálculos tipados foram apresentadas por diferentes autores. Neste cenário, o Cubo Lambda surgiu como uma forma de sistematizar o conhecimento em torno desses cálculos. No contexto do ensino das diversas variantes do Cálculo Lambda Tipado, uma ferramenta que consiga explorar todos os oito vértices do Cubo Lambda e com uma sintaxe unificada se mostra de sejável. Este trabalho descreve um simulador do Cálculo Lambda Tipado parametrizável, ou seja, que permite a experimentação com diversas funcionalidades do Cubo Lambda de forma conjunta ou independente, incluindo Polimorfismo, Construtores de Tipos, Tipos Dependentes e uma extensão dos respectivos cálculos que permite a definição de tipos indutivos como primitivas. Tipos indutivos são uma forma de definir estruturas de dados de forma recursiva muito utilizados em linguagens de programação funcionais modernas. A ferramenta pode ser encontrada no link <https://www.inf.ufrgs.br/~ebchandelier/>.

Understanding Lambda Calculus and Type Theory is important to deeply understand the fundamentals of both modern functional languages and proof assistant tools. Over the years different typed lambda calculus have been designed by different authors. In this scenario, the Lambda Cube emerged as a way to systematize knowledge around this subject. The Lambda Cube is a framework used to investigate the different versions of the typed Lambda Calculus. In the context of teaching the multiple variants of Typed Lambda Calculus, a tool that manages to explore all eight vertices of the Lambda Cube with a unified syntax is desirable. This work describes a parameterizable Typed Lambda Calculus simulator, that is, that allows experimentation with various functionalities of the Lambda Cube, including Polymorphism, Type Constructors, Dependent Types and an extension of the respective calculus that allows the definition of inductive types as primitives. Inductive types are a way of defining data structures recursively that are widely used in modern functional programming languages. The tool can be found at <https://www.inf.ufrgs.br/ ebchandelier/>.