Type-based termination of recursive definitions and constructor subtyping in typed lambda calculi

Abstract

In type systems, a combination of subtyping and overloading is a way to achieve more precise typings. This thesis explores how to use these mechanisms in two directions: (i) as a way to ensure termination of recursive functions; (ii) as a way to capture in a type-theoretic context the use of subtyping as inclusion between inductively defined sets. The first part of the thesis presents a mechanism that ensures termination through types and defines a system that incorporates it. More precisely, we formalize the notion of type-based termination using a restricted form of type dependency (also known as indexed types). Every datatype is replaced by a family of approximations indexed over a set of stages; then being in a certain approximation means that a term can be seen as having a certain bound on constructor usage. We introduce λˆ, a simply typed λ-calculus à la Curry, supporting parametric inductive datatypes, case-expressions and letrec-expressions with termination ensured by types. We show that λˆ enjoys important meta-theoretical properties, including confluence, subject reduction and strong normalization. We also show that the calculus is powerful enough to encode many recursive definitions rejected by existing type systems, and give some examples. We prove that this system encompasses in a strict way Giménez' λς, a system in which termination of typable expressions is ensured by a syntactical condition constraining the uses of recursive calls in the body of definitions. The second part of the thesis studies properties of a type system featuring constructor subtyping. Constructor subtyping is a form of subtyping in which an inductive type σ is viewed as a subtype of another inductive type τ if each constructor c of σ is also a constructor of τ (but τ may have more constructors), and whenever c : θ'→σ is a declaration for τ, then c : θ'→τ is a declaration for τ with θ'→≤θ'. In this thesis we allow for this form of subtyping in the system λcs, which is a simply typed λ-calculus à la Curry, supporting mutually recursive parametric datatypes, case-expressions and letrec-expressions. We establish the properties of confluence, subject reduction and decidability of type checking for this calculus. As the system features general recursion, the reduction calculus is obviously non-terminating. However, we sketch two ways of achieving strong normalization. One way is to constrain the system to guard-by-destructors recursion, following what is done for λς. The other way is to enrich the type system with stages (following the ideas presented for λˆ) and enforcing termination through typing. Potential uses of constructor subtyping include proof assistants and functional programming languages. In particular, constructor subtyping provides a suitable foundation for extensible datatypes, and is specially adequate to re-usability. The combination of subtyping between datatypes and overloading of constructors allows the definition of new datatypes by restricting or by expanding the set of constructors of an already defined datatype. This flexibility in the definition of datatypes induces a convenient form of code reuse for recursive functions, allowing the definition of new functions by restricting or by expanding already defined ones. We enrich a calculus featuring constructor subtyping with a mechanism to define extensible overloaded recursive functions by pattern-matching, obtaining the system λcs+fun. We formalize the concept of well-formed environment of function declarations and establish that under such environments the properties of confluence, subject reduction and decidability of type-checking hold. Moreover, we prove that the requirements imposed for the well-formed environments are decidable and show how standard techniques can still be used for compiling pattern-matching into case-expressions.

Em sistemas de tipos, a combinação de mecanismos de subtipagem e de sobrecarga de construtores permite alcançar tipagens mais precisas para os termos. Esta tese investiga a utilização destes mecanismos, quer como forma de assegurar a terminação de funções recursivas, quer como forma de captar subtipagem através de inclusão de conjuntos num sistema com tipos indutivos. A primeira parte da tese apresenta um sistema de tipos capaz de assegurar a terminação de funções recursivas, unicamente por tipagem. Mais concretamente, a noção de terminação baseada em tipos é formalizada utilizando uma forma restrita de dependência de tipos, também conhecida por tipos indexados. Cada tipo de dados é visto como uma família de aproximações, indexada por um conjunto de níveis, fornecendo tais níveis indicações sobre o uso de construtores na formação de termos. Esta forma de garantir terminação por tipos encontra-se formalizada no que é um cálculo lambda simplesmente tipado à la Curry, com tipos indutivos paramétricos, com expressões de ponto fixo e de análise de casos. Demonstra-se que λˆ é um cálculo bem comportado, satisfazendo as propriedades de confluência, preservação de tipos ao longo da cadeia de redução, e normalização forte. O sistema λˆ permite codificar muitas definições recursivas que são rejeitadas por outros sistemas com preocupações semelhantes de garantia de terminação. Em particular, prova-se que este cálculo engloba de modo estrito o sistema λς de Giménez, um sistema em que a terminação das expressões tipáveis é assegurada por uma condição sintáctica que restringe as chamadas recursivas de funções. Na segunda parte da tese, apresenta-se um sistema de tipos com subtipagem por construtores e estudam-se as suas propriadades. A subtipagem por construtores é uma forma de subtipagem na qual um tipo indutivo σ é visto como um subtipo de um outro tipo indutivo τ, se τ tiver mais construtores do que σ. Neste trabalho, a subtipagem por construtores está presente no sistema λcs, um cálculo lambda simplesmente tipado, à la Curry, com tipos inductivos paramétricos e mutuamente recursivos, com expressões de ponto fixo e de análise de casos. Demonstra-se que este cálculo é confluente, a tipagem é decidível e a redução preserva tipos. Para garantir a normalização forte, são propostas duas abordagens: satisfação de uma condição sintáctica nas definições recursivas (à semelhança de λς), ou enriquecimento do sistema de tipos com níveis (à semelhança de λˆ) de forma a garantir terminação por tipagem. Esta forma de subtipagem encontra aplicações nos sistemas de prova assistida e nas linguagens funcionais de programação. Em particular, a subtipagem por construtores revela-se adequada para o tratamento de tipos de dados extensíveis. A combinação da subtipagem com a sobrecarga de construtores permite que a definição de novos tipos de dados possa ser feita por restrição ou expansão do conjunto de construtores de um tipo de dados jà definido. Esta flexibilidade na definição de tipos de dados induz uma forma de re-utilização de código adequada às funções recursivas, permitindo que a definição de novas funções se possa fazer também por restrição ou expansão de funções já definidas. Estes mecanismos são estudados no âmbito do sistema λcs+fun, um cálculo lambda com subtipagem por construtores e com definições recursivas sobrecarregadas e extensíveis, definidas por concordância de padrões num ambiente global. Define-se, para este cálculo, o conceito de ambiente bem formado de funções, e demonstra-se que, para estes ambientes, as propriedades de confluência, decidibilidade de tipagem e preservação de tipos são válidas. Também se demonstra que os vários requisitos impostos para garantir a boa formação do ambiente global de funções correspondem a propriedades decidíveis. Finalmente, descreve-se um algoritmo de compilação das funções definidas por concordância de padrões para expressões com análise de casos.