Implémentation d'un langage fonctionnel orienté vers la méta programmation

Abstract

Ce mémoire présente l'implémentation d'un nouveau langage de programmation nommé Typer. Typer est un langage fonctionnel orienté vers la méta programmation. Il a été conçu pour augmenter la productivité du programmeur et lui permettre d'écrire des applications plus fiables grâce à son système de types.

Pour arriver à ses fins, Typer utilise l'inférence de types et implémente un puissant système de macros. L'inférence de types permet à l'utilisateur d'omettre certains éléments, le système de macros, quant à lui, permet de compléter le programme pendant la compilation lorsque l'inférence n'est pas suffisante ou pour générer du code.

Typer utilise les types dépendants pour permettre à l'utilisateur de créer des types très expressifs pouvant même être utilisés pour représenter des preuves formelles. De plus, l'expressivité des types dépendants permet au compilateur d'effectuer des vérifications plus approfondies pendant la compilation même.

Ces mécaniques permettent au code source d'être moins verbeux, plus concis et plus simple à comprendre, rendant, ainsi l'écriture de programmes ou/et de preuves plus plaisante. Ces fonctionnalités sont implémentées dans l'étape que nous appelons l'élaboration, à l'intérieur de laquelle de nombreuses transformations du code source ont lieu. Ces transformations incluent l'élimination des aides syntaxiques, la résolution des identificateurs, l'expansion des macros, la propagation et l'inférence des types.

This dissertation present the implementation of a new programming language named Typer Typer is a functional programming language oriented towards meta programming. It has been created to increase the programmer productivity and enable him to write safer programs thanks to his type system.

To achieve his goal, Typer use type inference and a powerful macro system. Type inference enable to user to elide some elements while the macro system enable us to complete the program during compilation.

Typer use dependent type which enable the user to create very expressive types which can even be used to represent formal proofs. Furthermore, dependent type's expressivity enable the compiler to perform a in-depth checks during compilation.

Those mechanics enable the source code to be less verbose, shorter and easier to understand, making the writing of new programmes more enjoyable. Those functionalities are implemented during the step we call the elaboration in which numerous transformations occur. Those transformations include the removal of syntactic sugar, identifier resolution, macro expansion and the propagation and the inference of types.