A reasonably exceptional type theory: a type theory with exceptios

Abstract

Los asistentes de pruebas son una herramienta de software donde es posible desarrollar pro- gramas sobre los cuales se pueden demostrar propiedades y as ́ı certificarlos. Esto es posible a trav ́es de teor ́ıas de tipo altamente expresivas que sirven como marcos de trabajo lo ́gicos, donde pruebas y programas coexisten. Por otro lado, los lenguajes de programaci ́on modernos y sus sistemas de tipo asociados soportan, de alguna forma u otra, el manejo de excepciones. Sin embargo, los asistentes de pruebas no proveen un mecanismo de excepciones debido a la naturaleza de estos: las excepciones pueden producir sistemas inconsistentes (las pruebas no son v ́alidas), lo que invalida el objetivo de un asistente de pruebas. De esta forma, no es posible utilizar excepciones en programas. Para el caso del Calculus of Inductive Construc- tions (CIC), la teor ́ıa de tipos usada por el asistente de pruebas Coq, existen trabajos previos que han an ̃adido excepciones la teor ́ıa. Sin embargo, estas extensiones resultan inc ́omodas debido a que se pierden propiedades importantes de la teor ́ıa, como es la consistencia de la teor ́ıa, o no es posible razonar sobre excepciones de manera directa. El presente trabajo crea una nueva teor ́ıa de tipo, la Reasonably Exceptional Type Theory (RETT), donde es posible trabajar con excepciones y razonar sobre ellas de forma simple, directa y consistente. Esta teor ́ıa diferencia entre sus los elementos computacionales y sus los elementos proposicionales (o teoremas), donde los elementos computacionales siempre pueden ser excepciones mientras que los teoremas siempre son puros (no son excepciones). Adicionalmente, la teor ́ıa provee un mecanismo que permite expresar que un elemento computacional debe ser puro. La val- idacio ́n de esta teor ́ıa se realiza por una traduccio ́n sinta ́ctica hacia CIC. Esta traduccio ́n provee buenas propiedades meta te ́oricas, lo que permite su uso como teor ́ıa subyacente para un asistente de pruebas con excepciones. Adem ́as, se desarroll ́o un plugin para Coq, el cua ́l hace disponible la teor ́ıa a los programadores. De esta forma, RETT es la primera teor ́ıa de tipos con excepciones consistente que permite el razonamiento sobre estas, con una implementacio ́n para Coq.