Dans ce mémoire, je présente une technique pour combiner du code de bas niveau à un
langage purement fonctionnel avec types dépendants. Par code de bas niveau, je veux dire
n’importe quel programme écrit dans un langage qui permet le contrôle direct des ressources
de la machine. En particulier, ce texte s’intéresse à la gestion de la mémoire.
Plus concrètement, un programmeur C contrôle l’endroit et le moment où un bloc de
mémoire est alloué, ainsi que la façon dont l’objet est initialisé. Par exemple, on peut allouer
de l’espace sur la pile pour immédiatement l’initialiser avec un memcpy. Alternativement, on
peut allouer un bloc sur le tas et l’initialiser champ par champ plus tard. Pour certaines
applications où la mémoire est limitée ou la performance importante, ce choix est important.
Un tel niveau de contrôle n’est pas disponible dans les langages de haut niveau, sauf
pour quelques exceptions. Les langages fonctionnels comme OCaml ou Haskell découragent
ou même interdisent de modifier les champs d’un objet. C’est encore plus vrai pour les
langages à types dépendants où la mutation est l’éléphant dans le magasin de porcelaine
de la cohérence. C’est un choix de design intentionnel. Un programme pur est plus facile à
comprendre et analyser, mais comment séparer l’initialisation de l’allocation quand un objet
ne peut pas changer ?
Ce mémoire essaie de démontrer que ce n’est pas parce que c’est impossible, mais parce
que ces langages ne sont pas habituellement utilisés dans un contexte où c’est nécessaire. Par
contre, ce n’est pas facile non plus. Pour garantir la sécurité et la cohérence, il faut modéliser
l’état d’un objet partiellement initialisé au niveau des types, ce que la plupart des langages
ont de la peine à faire. La combinaison du manque de nécessité et de la lourdeur syntaxique
et conceptuelle est la raison pour laquelle cette fonctionnalité est souvent absente.
Pour y parvenir, nous prenons un langage à types dépendants, Typer, et nous y ajoutons
le nécessaire pour récupérer une partie du contrôle abandonné dans le design original. Nous
permettons au programmeur d’allouer des blocs de mémoire et de les initialiser graduellement
plus tard, sans compromettre les propriétés de sécurité du programme. Concrètement, nous
utilisons les monades, un concept de la théorie des catégories déjà utilisé pour la modélisation
d’effets de bord, pour limiter les mutations aux endroits sécuritaires. / In this thesis, I will demonstrate how to combine low-level code with dependent types. By low-level code, I mean any program authored in a language that allows direct control of computer resources. In particular, this text will focus on memory management.
Specifically, a C programmer has control over the location and time when a block of memory is allocated, as well as how it is initialized. For instance, it is possible to allocate stack space to immediately initialize it with an invocation of memcpy. Alternatively, one can allocate heap spate and initialize it field by field later. For some applications where memory is constrained or performance is important, this choice can matter.
This level of control is not available in high-level languages, barring a few exceptions. Functional languages such as OCaml or Haskell discourage or simply forbid the mutation of objects. This is especially the case in dependently typed languages where mutation is the bull in the china shop of consistency. This is a deliberate choice as a pure program is easier to understand and reason about. However, having allocation and initialization done in two distinct steps seems impossible in this situation.
This thesis shows that this is not impossible, it is simply done this way because these kinds of languages are seldom used in a context where such control is necessary. This does not mean though that adding this feature is easy. If we are to guarantee both safety and consistency, we need to keep track of the initialization state at the type level. Most languages struggle to do this. Language designers simply forgo this feature because it is not useful to them in addition to being difficult to use.
To achieve it, we start with a dependently typed language, Typer, and add back the mechanisms necessary to recover the control relinquished in the original design. We let the programmer allocate blocks of memory to initialize later, without compromising the safety properties of the program. Specifically, we use monads, a concept from category theory, a know technique to model side effects, to limit mutation to situations where it is safe.
| Identifer | oai:union.ndltd.org:umontreal.ca/oai:papyrus.bib.umontreal.ca:1866/32087 |
| Date | 12 1900 |
| Creators | Génier, Simon |
| Contributors | Monnier, Stefan |
| Source Sets | Université de Montréal |
| Language | fra |
| Detected Language | French |
| Type | thesis, thèse |
| Format | application/pdf |
Page generated in 0.0025 seconds