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.