Types dépendants: de la théorie à la pratique

Quand on parle de types dépendants, une approche informelle est souvent faite en tentant d’initier les gens à travers des exemples plus ou moins simples. Le plus immédiat est bien évidemment le vecteur avec sa taille …

Malheureusement, avec une telle approche nous n’abordons pas le sujet en profondeur et l’essence même de ce qu’est la dépendance de type nous passe au dessus de la tête.

Durant cette présentation, nous allons sortir de notre zone de confort dès le départ en partant de la théorie pour aller vers la pratique. Partir de la théorie veut dire lecture de formalise pour mieux apprehender ce qu’est effectivement la dépendance de type !

Nous aborderons: le type fonctionnel dépendant, la paire dépendante, le type somme et si tout va bien l’égalité propositionnelle.

Speaker

Didier Plaindoux

Didier Plaindoux's profile
Senior Software Engineer
Fungus (Freelance)

Who am I

I'm a compulsive designer of strong-typed functional, logical and object-oriented programming languages! The rest of the time, I'm a freelance software developer who works very hard to produce usable and used solutions.