Ce contrôle statique ressemble à des types dépendants (un type paramétré par une valeur du langage, ici un int pour la dimension des matrices). Pour ce cas, ça doit pouvoir se faire avec des GADT comme dans les exemples du cours de Jeremy Yallop; mais c'est un usage assez avancé du système de type. Me trompe-je ?
Dans le cas de Abach j'implémente actuellement le calcul matriciel en adoptant un angle un petit peu plus géométrique. Étant donné des espaces vectoriels de dimension finie A et B munis de bases un foncteur décrit Hom(A,B) qui, puisque les espaces ont une base privilégiée, est exactement l'espace vectoriel des matrices représentant une application linéaire de A dans B. Puisque le type est abstrait, c'est la signature de l'application de composition qui garantit qu'on ne compose que des applications linéaires d'une manière qui résulte en une multiplication de matrices aux dimensions compatibles.
Cette méthode oblige à introduire des notations pour les espaces vectoriels manipulés – ce qui est pour moi précisément le but recherché – avec des choses du genre:
module A = Abach_VectorSpace.Make(QQ)(struct let dimension = 5 end)
module B = Abach_VectorSpace.Ker(QQ)(struct let f = ... end)
module M = Abach_VectorSpace.Hom(QQ)(A)(B)
Un "effet de bord" de cette méticulosité est que le système de type permet de contrôler la justesse sémantique des opérations effectuées tout en gardant une notation proche de celles que peuvent utiliser les mathématiciens qui ne fait pas intervenir de notions plus exotiques comme les GADT.
[^] # Re: Module et type abstrait
Posté par Michaël (site web personnel) . En réponse au journal Une petite histoire d'utilisation type fort dans Ocaml. Évalué à 4.
Dans le cas de Abach j'implémente actuellement le calcul matriciel en adoptant un angle un petit peu plus géométrique. Étant donné des espaces vectoriels de dimension finie
AetBmunis de bases un foncteur décritHom(A,B)qui, puisque les espaces ont une base privilégiée, est exactement l'espace vectoriel des matrices représentant une application linéaire deAdansB. Puisque le type est abstrait, c'est la signature de l'application de composition qui garantit qu'on ne compose que des applications linéaires d'une manière qui résulte en une multiplication de matrices aux dimensions compatibles.Cette méthode oblige à introduire des notations pour les espaces vectoriels manipulés – ce qui est pour moi précisément le but recherché – avec des choses du genre:
Un "effet de bord" de cette méticulosité est que le système de type permet de contrôler la justesse sémantique des opérations effectuées tout en gardant une notation proche de celles que peuvent utiliser les mathématiciens qui ne fait pas intervenir de notions plus exotiques comme les GADT.