New paper: Subject reduction in a Curry-style polymorphic type system with a vectorial structure

(Versión en español más abajo)

New paper submitted, with Pablo Arrighi and Benoît Valiron.

Title: Subject reduction in a Curry-style polymorphic type system with a vectorial structure.

Abstract: The algebraic lambda-calculus [Vau09] and the linear-algebraic lambda-calculus [AD08] extend the lambda-calculus with the possibility of making arbitrary linear combinations of lambda-terms. The two foundational works of [ADC09] and [DCP10] describe type systems for this calculus respectively accounting for scalars and sums. Building on these approaches, we devise a typed algebraic lambda-calculus merging the two approaches while keeping a language featuring local confluence and a weak subject reduction. This gives rise to an original and general type theory where types, in the same way as terms, have a vector space-like structure. The main contribution of this paper is a subject reduction result, a problem renowned to be a delicate matter under the presence of union-like type constructs.

Basically the idea of the paper is to present the several-times announced "vectorial type system": we present here a type system with a non-standard subject reduction. We conclude that, in general, to have subject reduction in a vectorial type system we would need to move to Church-style.

I uploaded the paper to arXiv today, so it will appear next Tuesday. I will put the link here. arXiv:1012.4032.

---

Nuevo paper enviado, con Pablo Arrighi y Benoît Valiron.

Título: Subject reduction (ni idea cómo se dice eso en español) en un sistema de tipos polimórfico à la Curry con una estructura vectorial.

Resumen: El lambda-cálculo algebraico [Vau09] y el lambda-cálculo algebraico-lineal [AD08] extienden el lambda-cálculo con la posibilidad de hacer combinaciones lineales arbitrarias de lambda-términos. Los dos trabajos fundacionales de [ADC09] y [DCP10] describen sistemas de tipos para este cálculo respectivamente teniendo en cuenta escalares y sumas. Construido sobre estos enfoques, elaboramos un lambda-cálculo algebraico fusionando ambos, logrando un lenguaje con confluencia local y una subject reducción débil. Esto da lugar a una teoría de tipos original y general donde los tipos, de la misma manera que los términos, tienen una estructura al estilo de un espacio vectorial. La principal contribución de este paper es el resultado de subject reduction, un problema reconocido como complicado en presencia de construcciones de tipo unión.

Básicamente la idea del paper es presentar el muchas veces anunciado "sistema de tipos vectorial": lo que presentamos aquí es un sistema de tipos con un subject reduction no estándar. Concluímos que, en general, para tener subject reduction in sistemas de tipos vectoriales deberíamos pasarnos a Church-style.

Hoy subí el paper a arXiv, así que aparecerá el próximo martes. Pondré el link aquí. arXiv:1012.4032. Y aquí una explicación más amena del paper.