Polymorphisme de type supérieur : Une exploration
Introduction au Polymorphisme de Type Supérieur
Le polymorphisme de type supérieur, qui permet d’abstraire à la fois des types et des constructeurs de types, est essentiel pour exprimer des opérations génériques sur des collections ou pour intégrer des langages spécifiques à un domaine (DSL) typés, notamment dans un style sans balise finale. En général, le constructeur de type abstrait n’est pas aléatoire, mais doit respecter une interface particulière, ce qui est connu sous le nom de polymorphisme borné.
Limitations d’OCaml en matière de Polymorphisme de Type Supérieur
OCaml ne prend pas en charge directement le polymorphisme de type supérieur. En effet, les variables de type dans OCaml se limitent aux types plutôt qu’aux constructeurs de types, et ces derniers ne peuvent pas apparaître dans les expressions de type sans être appliqués au bon nombre d’arguments. Cependant, il est possible d’exprimer le polymorphisme de type supérieur dans OCaml, bien que cela puisse se faire de plusieurs manières, certaines étant plus complexes que d’autres. Les méthodes les moins encombrantes sont souvent moins connues et continuent d’être redécouvertes. Cet article résume les différentes manières d’exprimer, et parfois d’éviter, le polymorphisme de type supérieur, en s’appuyant sur des travaux académiques et des discussions sur des forums spécialisés.
Comprendre le Polymorphisme de Type Supérieur
Le polymorphisme de type supérieur permet d’abstraire des types de manière similaire à l’abstraction des valeurs par les fonctions. Par exemple, la somme de nombres est une opération courante qui peut être généralisée pour fonctionner sur n’importe quelle collection de nombres. Voici un exemple de fonction qui somme une liste d’entiers :
let rec somme : int list -> int = function [] -> 0 | h::t -> h + somme tNous pouvons aller plus loin en abstraire non seulement les nombres, mais aussi l’opération d’addition elle-même, ce qui nous donne une fonction d’ordre supérieur :
let rec plier (f: int -> int -> int) (z: int) : int list -> int =
function [] -> z | h::t -> f h (plier f z t)En généralisant encore, nous pouvons remplacer le type int par une variable de type :
let rec plier_gen (f: 'a -> 'a -> 'a) (z: 'a) : 'a list -> 'a =
function [] -> z | h::t -> f h (plier_gen f z t)Cette fonction polymorphe décrit une opération qui peut être appliquée à des listes de différents types de manière uniforme.
Abstraction des Types et Constructeurs de Types
Nous pouvons également encapsuler l’opération et la valeur dans un enregistrement paramétré :
type 'a monoid = { op: 'a -> 'a -> 'a; unite: 'a }La fonction plier_gen peut alors être réécrite comme suit :
let rec plier_monoid (m: 'a monoid) : 'a list -> 'a =
function [] -> m.unite | h::t -> m.op h (plier_monoid m t)Lorsque nous utilisons plier_monoid sur une liste concrète de type t list, la variable de type 'a est instanciée au type t des éléments de cette liste. Cependant, le type n’est pas totalement arbitraire : il doit exister une valeur t monoid à passer à plier_monoid comme argument. Cela signifie que le type t doit au moins implémenter l’interface 'a monoid, ce qui rend le polymorphisme dans plier_monoid borné.
Alternatives au Polymorphisme de Type Supérieur dans OCaml
Malheureusement, les variables de type supérieur ne sont pas possibles dans OCaml. La section suivante expliquera pourquoi, suivie de plusieurs alternatives que nous pouvons utiliser dans OCaml. Certaines de ces alternatives peuvent aboutir à un code qui ressemble presque exactement à celui du polymorphisme de type supérieur imaginé précédemment.
Conclusion
Le polymorphisme de type supérieur est un concept puissant qui permet une grande flexibilité dans la programmation fonctionnelle. Bien qu’OCaml ne le supporte pas directement, il existe des moyens de contourner cette limitation et d’exprimer des concepts similaires. En explorant ces alternatives, les développeurs peuvent tirer parti des avantages du polymorphisme tout en travaillant dans l’environnement OCaml.
Modules et Types dans OCaml
Examinons les deux modules suivants :
module Arbre=struct
type 'a t=Feuille | Branche of 'a t * 'a * 'a t
end
module ArbreA : dcont=struct
type 'a t=('a * 'a) Arbre.t
end
Dans cet exemple, 'a Arbre.t représente un type de données : un type nouveau, distinct de tous les autres types existants. En revanche, 'a ArbreA.t est un alias : comme l’indique sa déclaration, il est équivalent à un type existant, à savoir ('a * 'a) Arbre.t.
Variables de Type et Équivalences
Imaginons qu’OCaml dispose de variables de type de plus haut niveau, comme 'F évoquées précédemment. La vérification des types consiste finalement à résoudre ou vérifier des égalités de types, telles que 'a 'F='b 'G. Si les variables de type de plus haut niveau ne se limitaient qu’aux constructeurs de types de données, la solution serait simple : 'a='b et 'F='G ; un type de données est unique, donc égal uniquement à lui-même. C’est la situation que l’on retrouve en Haskell. Pour garantir que seuls les constructeurs de types de données peuvent être substitués aux variables de type de plus haut niveau, un compilateur Haskell suit les alias de type, même à travers les frontières des modules. Le système de modules en Haskell est relativement simple, ce qui rend ce suivi peu problématique.
En revanche, le système de modules de ML est plus complexe. Il comprend des foncteurs, des signatures, etc., et s’appuie largement sur les alias de type, par exemple :
module F(T: sig type 'a t val vide: 'a t end)=struct
type 'a ft='a T.t
end
Si nous interdisons la substitution des alias de type pour les variables de type de plus haut niveau, nous limitons considérablement l’expressivité. Par exemple, 'a ft ci-dessus est un alias de type ; par conséquent, F(Arbre).ft ne peut pas être substitué à une variable de type de plus haut niveau, même si l’on pourrait penser que F(Arbre).ft est identique à Arbre.t, qui est substituable.
D’un autre côté, si nous permettons la substitution des alias de type pour les variables de type de plus haut niveau, l’équivalence entre 'a 'F='b 'G et 'a='b, 'F='G s’effondre. En effet, considérons (int*int) 'F=int 'G. Cette équation a maintenant pour solution : 'F=Arbre.t et 'G=ArbreA.t. Les alias de type paramétrés comme 'a ArbreA.t sont des fonctions de type, et les expressions de type comme int ArbreA.t sont des applications de ces fonctions, se développant en la partie droite de la déclaration d’alias avec 'a substitué par int. Ainsi, avec les alias de type, le problème d’égalité des types devient un problème d’unification de plus haut ordre, qui n’est pas décidable.
Fonctions de Type Supérieur comme Foncteurs
Bien qu’OCaml ne prenne pas en charge les variables de type de plus haut niveau, le polymorphisme de type supérieur n’est pas impossible. Il existe d’autres moyens de paramétrer par un constructeur de type : l’abstraction du système de modules (foncteur) est la première qui vient à l’esprit. Cependant, cela s’avère plutôt verbeux et encombrant. Voyons cela de plus près.
Nous allons maintenant réécrire le code OCaml polymorphe hypothétique à la fin de l'[Introduction] en OCaml réel, en élevant le niveau, pour ainsi dire, du niveau terme au niveau module. L’enregistrement hypothétique
type ('a,'F) seq={decon: 'a 'F -> ('a * 'a 'F) option}
deviendra la signature de module
module type seq_i=sig
type 'a t (* type de séquence *)
val decon : 'a t -> ('a * 'a t) option
end
Cette signature représente la variable de type de plus haut niveau 'F, non supportée dans OCaml, avec un constructeur de type ordinaire t (constante de type). Différentes implémentations de seq_i (voir, par exemple, ListeS ci-dessous) instancient 'a t à leur manière ; ainsi, t agit en effet comme une variable. La fonction polymorphe hypothétique de plus haut niveau
let rec plie (m: 'a monoid) (s: ('a,'F) seq) : 'a 'F -> 'a=fun c ->
match s.decon c with None -> m.unite | Some (h,t) -> m.op h (plie m s t)
deviendra le foncteur, paramétré par la signature seq_i :
module PlieS(S:seq_i)=struct
let rec plie (m: 'a monoid) : 'a S.t -> 'a=fun c ->
match S.decon c with None -> m.unite | Some (h,t) -> m.op h (plie m t)
end
Nous avons obtenu ce que nous voulions : une abstraction sur une séquence. Pour l’utiliser afin de définir d’autres fonctions polymorphes de plus haut niveau, telles que somme pour additionner une séquence, nous avons également besoin de foncteurs. Les foncteurs sont contagieux, pourrait-on dire.
module SommeS(S:seq_i)=struct
open S
open PlieS(S)
let somme : int t -> int=plie monoid_plus
end
Enfin, un exemple d’instanciation et d’utilisation de fonctions polymorphes de plus haut niveau : additionner une liste. Tout d’abord, nous avons besoin d’une instance de seq_i pour une liste : le témoin qu’une liste est une séquence.
module ListeS=struct
type 'a t='a list
let decon=function [] -> None | h::t -> Some (h,t)
end
Nous la passons au foncteur SommeS :
let 6=
let module M=SommeS(ListeS) in M.somme [1;2;3]
Le code accompagnant montre un autre exemple : utiliser le même SommeS pour additionner un tableau, qui peut également être considéré comme une séquence. Ainsi, dans cette approche, toutes les fonctions polymorphes de plus haut niveau sont des foncteurs, ce qui entraîne verbosité, awkwardness et code répétitif. Par exemple, nous ne pouvons même pas écrire une application SommeS sous la forme SommeS(ListeS).somme [1;2;3] ; nous devons utiliser l’expression verbeuse ci-dessus.
Références
Jeremy Yallop et Leo White : Polymorphisme léger de type supérieur. FLOPS 2014.
# Polymorphisme et son Réduction
## Introduction au Polymorphisme
Il est intéressant de noter que le polymorphisme de type supérieur peut toujours être réduit au polymorphisme ordinaire, comme l’ont habilement démontré Yallop et White dans leur article de 2014. Leur méthode, qu’ils ont appelée défonctionnalisation, mérite d’être revisitée sous un nouvel angle.
## Comprendre les Types Paramétrés
Prenons le type `a list` comme exemple. Ce type est paramétré : `a` représente le type des éléments, tandis que `list` désigne le nom de la collection. Cette combinaison peut être reformulée, par exemple, en `(‘a, list_name) app`, où `(‘a, ‘b) app` est un type fixe, et `list_name` est le type ordinaire qui indique le nom de base. L’équivalence entre ces deux représentations est confirmée par la bijection suivante :
« `
inj: ‘a list -> (‘a, list_name) app
prj: (‘a, list_name) app -> ‘a list
« `
## Mise en Œuvre de la Bijection
Pour mettre cela en pratique, nous introduisons un type de données dédié appelé `pairing`. Ce type est extensible, permettant de définir autant de paires que nécessaire.
« `
type (‘a, ‘b) app = ..
« `
Pour `a list`, nous avons :
« `
type list_name
type (‘a, ‘b) app += List_name : ‘a list -> (‘a, list_name) app
« `
Dans ce cas, la bijection `a list <-> (‘a, list_name) app` se traduit par :
« `
let inj x = List_name x
let prj (List_name x) = x
« `
Ces deux fonctions sont effectivement des inverses l’une de l’autre.
### Exercice
Il est important de noter que prouver que `inj` et `prj` sont des inverses n’est pas trivial. Cela nécessite une condition supplémentaire, qui est satisfaite dans notre cas. Formulez cette condition.
## Représentation du Polymorphisme
Dans cette nouvelle représentation du polymorphisme de liste comme `(‘a, list_name) app`, le nom de base `list_name` est un type ordinaire (de type `*`). L’abstraction sur celui-ci est simple : il suffit de le remplacer par une variable de type. Ainsi, le polymorphisme basé sur le nom de base devient le polymorphisme ordinaire. Nous pouvons alors écrire la fonction `folds` polymorphe de séquence presque littéralement comme suit :
« `
type (‘a, ‘n) seq = { decon: (‘a, ‘n) app -> (‘a * (‘a, ‘n) app) option }
let rec folds (m: ‘a monoid) (s: (‘a, ‘n) seq) : (‘a, ‘n) app -> ‘a = fun c ->
match s.decon c with None -> m.unit | Some (h, t) -> m.op h (folds m s t)
« `
Au lieu de `a ‘F`, nous écrivons `(‘a, ‘n) app`. C’est tout. Utiliser `folds` dans d’autres fonctions de type supérieur est simple, comme s’il s’agissait d’une fonction polymorphe ordinaire :
« `
let sums s c = folds monoid_plus s c
(* val sums : (int, ‘a) seq -> (int, ‘a) app -> int =
« `
Les annotations de type ne sont pas nécessaires : l’inférence de type fonctionne correctement. Voici un exemple d’utilisation, qui consiste à sommer une liste :
« `
let list_seq : (‘a, list_name) seq =
{ decon = fun (List_name l) ->
match l with [] -> None | h::t -> Some (h, List_name t) }
let result = sums list_seq (List_name [1; 2; 3])
« `
## Automatisation et Simplification
Il reste cependant une certaine complexité : l’utilisateur doit penser au nom de base comme `list_name` et au tag comme `List_name`, tout en garantissant leur unicité. Yallop et White ont automatisé ce processus en utilisant le système de modules, comme le montre le code associé à cette page, ou dans leur article (et le package Opam `higher`).
## Éviter le Polymorphisme de Type Supérieur
Il est parfois possible d’éviter complètement le polymorphisme de type supérieur. En examinant de près, il peut s’avérer que le problème à résoudre ne nécessite pas réellement ce type de polymorphisme. Prenons notre exemple courant.
### Interface de Séquence
Considérons l’interface de séquence, paramétrée à la fois par le type des éléments de la séquence et par la séquence elle-même. La définition qui vient à l’esprit, mais qui ne peut pas être écrite ainsi en OCaml, est :
« `
type (‘a, ‘F) seq = { decon: ‘a ‘F -> (‘a * ‘a ‘F) option }
« `
Cette définition présente une particularité : l’unique opération `decon` consomme et produit des séquences du même type `a F` (c’est-à-dire le même type de séquence avec des éléments du même type). Ainsi, `F` apparaît toujours comme le type `a F`, où `a` est le paramètre de `seq` : `a` et `F` ne varient pas indépendamment. Par conséquent, il n’y a en réalité pas de polymorphisme de type supérieur ici. L’interface de séquence peut être simplement écrite comme :
« `
type (‘a, ‘t) seq = { decon: ‘t -> (‘a * ‘t) option }
« `
Avec `folds` prenant exactement la forme souhaitée :
« `
let rec folds (m: ‘a monoid) (s: (‘a, ‘t) seq) : ‘t -> ‘a = fun c ->
match s.decon c with None -> m.unit | Some (h, t) -> m.op h (folds m s t)
« `
C’est une fonction polymorphe ordinaire. Il n’y a aucun problème à l’utiliser pour définir d’autres fonctions polymorphes de séquence, par exemple :
« `
let sums s c = folds monoid_plus s c
(* val folds : ‘a monoid -> (‘a, ‘t) seq -> ‘t -> ‘a =
« `
Et l’appliquer, par exemple, à une liste :
« `
let list_seq : (‘a, ‘a list) seq =
{ decon = function [] -> None | h::t -> Some (h, t) }
let result = sums list_seq [1; 2; 3]
« `
### Exercice
Considérez l’interface des collections qui peuvent être « mappées », dans un OCaml hypothétique avec des variables de type de type supérieur.# Interfaces Polymorphiques et Collections
## Introduction aux Interfaces Polymorphiques
Dans le domaine de la programmation, la question se pose de savoir si une interface polymorphique peut être exprimée à l’aide de la polymorphie ordinaire ou si une polymorphie de type supérieur est nécessaire. En examinant de près l’interface polymorphique de type supérieur, notée `(‘a,’F) seq`, et l’interface polymorphique ordinaire `(‘a,’t) seq`, on constate que cette dernière est plus vaste. En effet, l’interface de type supérieur ne couvre que les séquences polymorphiques telles que `‘a list`, tandis que `(‘a,’t) seq` s’applique également à d’autres structures comme les fichiers, les chaînes de caractères et les tampons. Cette extension est bénéfique, car elle permet d’appliquer les mêmes opérations de réduction (folds) à des séquences dont la structure est optimisée pour le type de leurs éléments.
## Application des Folds
Prenons un exemple d’application des folds à une chaîne de caractères, qui n’est pas une séquence polymorphique :
« `ocaml
let string_seq : (char,int*string) seq =
{decon=fun (i,s) ->
if i >= String.length s || i < 0 then failwith "Index out of bounds"
else (s.[i], (i+1, s))}
```
Ainsi, nous pouvons utiliser les folds avec n'importe quelle collection, qu'elle soit polymorphique ou non, tant qu'il existe une implémentation de l'interface `('a,'t) seq`. Cette approche illustre un principe ancien mais très utile : élargir le type tout en restreignant l'ensemble de ses valeurs en définissant des "témoins" comme `('a,'t) seq`.
## Exercice Pratique
L'approche de Yallop et White peut également être appliquée aux collections non polymorphiques. Utilisez cette méthode pour implémenter `string_seq`.
## Algebras Technologiques
### Construction de Valeurs
L'exemple en cours, l'interface `seq`, concerne la déconstruction de séquences, c'est-à-dire les co-algèbres. Passons maintenant à la construction, qui consiste à créer des valeurs à l'aide d'un ensemble fixe d'opérations, pouvant être considérées comme un DSL (Domain-Specific Language) intégré. L'abstraction sur une implémentation de DSL donne lieu à de la polymorphie. Si le DSL intégré est typé, la polymorphie devient de type supérieur, comme on le voit souvent dans les intégrations de DSL en style tagless-final.
### Embedding Tagless-Final
Nous allons maintenant examiner comment la polymorphie de type supérieur émerge dans les intégrations de DSL et comment elle peut être dissimulée. L'idée clé est l'algèbre initiale, qui est, par définition, l'abstraction sur toute algèbre concrète ayant la même signature, c'est-à-dire l'abstraction sur les implémentations de DSL.
Prenons comme exemple un langage de programmation simple avec des entiers et des booléens, inspiré du langage utilisé dans le chapitre 3 de l'ouvrage de Pierce, `Types and Programming Languages` (TAPL). Voici l'intégration tagless-final en OCaml, où la grammaire du langage est représentée par une signature OCaml :
```ocaml
module type sym = sig
type 'a repr
val int : int -> int repr
val add : int repr -> int repr -> int repr
val iszero : int repr -> bool repr
val if_ : bool repr -> ‘a repr -> ‘a repr -> ‘a repr
end
« `
### Exemple de Termes
Le langage est typé ; par conséquent, le type `’a repr`, qui représente les termes du DSL, est indexé par le type du terme : un `int` ou un `bool`. La signature `sym` définit également le système de types du DSL, presque comme dans TAPL, mais avec des règles de typage écrites de manière plus concise.
Voici un exemple de terme du DSL :
« `ocaml
module SymEx1(I:sym) = struct
open I
let t1 = add (add (int 1) (int 2)) (int 3) (* liaison intermédiaire *)
let res = if_ (iszero t1) (int 0) (add t1 (int 1))
end
« `
Ce terme est écrit comme un foncteur paramétré par `sym`, ce qui permet d’abstraire l’implémentation du DSL. Le terme est polymorphe par rapport à `sym` et peut donc être évalué dans n’importe quelle implémentation du DSL. Étant donné que `sym` contient un type de type supérieur `repr`, la polymorphie est de type supérieur.
### Abstraction des Termes
Le terme DSL de type `int`, tel que `SymEx1`, peut être considéré comme le foncteur :
« `ocaml
functor (I:sym) -> sig val res : int I.repr end
« `
Pour abstraire sur `int`, nous l’encapsulons dans un module :
« `ocaml
module type symF = sig
type a
module Term(I:sym) : sig val res : a I.repr end
end
« `
Cela peut ensuite être transformé en un type polymorphe ordinaire :
« `ocaml
type ‘a sym_term = (module (symF with type a = ‘a))
« `
Cela nous permet de représenter le foncteur `SymEx1` comme une valeur OCaml ordinaire :
« `ocaml
let sym_ex1 : _ sym_term =
(module struct type a = int module Term = SymEx1 end)
« `
Ici, l’annotation de type est nécessaire, mais nous laissons le type du terme comme `_`, une variable schématique. OCaml l’infère comme `int`. Si nous avons une implémentation de `sym`, par exemple, le module `R`, nous pouvons l’utiliser pour exécuter l’exemple et obtenir la valeur de `sym_ex1` dans l’interprétation de `R` :
« `ocaml
let _ = let module N = (val sym_ex1) in
let module M = N.Term(R) in M.res
« `
### Implémentation de la Signature Sym
Le type `’a sym_term` peut lui-même implémenter la signature `sym` d’une manière « tautologique » :
« `ocaml
module SymSelf : (sym with type ‘a repr = ‘a sym_term) = struct
type ‘a repr = ‘a sym_term
let int : int -> int repr = fun n ->
let module M(I:sym) = struct let res = I.int n end in
(module struct type a = int module Term = M end)
let add : int repr -> int repr -> int repr = fun (module E1) (module E2) ->
let module M(I:sym) =
struct module E1T = E1.Term(I) module E2T = E2.Term(I)
« `
Cette structure permet de manipuler des termes de manière polymorphe tout en préservant la flexibilité et l’abstraction nécessaires pour travailler avec des DSL intégrés.
Comprendre les Types de Haut Niveau
Dans cet article, nous allons explorer la manière dont les types de haut niveau peuvent être simplifiés en utilisant des approches innovantes. En particulier, nous examinerons la méthode proposée par Yallop et White, qui vise à réduire la complexité des types polymorphiques de haut niveau à des types polymorphiques ordinaires.
Types Polymorphiques et Abstraction
Un type polymorphique tel que 'a list représente une collection de types, indexée par un type spécifique (dans cet exemple, les éléments de la liste). D’autre part, une abstraction de type de haut niveau comme 'a 'F utilise une variable de type de haut niveau hypothétique (en OCaml) pour représenter une famille de types tout en conservant un suivi de l’index. Cette abstraction peut être réalisée de différentes manières.
Considérons le type existentiel exists a. a list, qui peut être réalisé en OCaml de plusieurs façons. Ce type existentiel devient alors un type ordinaire de rang * et peut être abstrait à l’aide d’une variable de type, par exemple 'd. Ainsi, le ‘nom de famille’ devient le type de famille avec un index caché. Cependant, nous perdons la trace de cet index, ce qui nous amène à le réintroduire, aboutissant au type ('a,'d) hk. Par conséquent, (t,exists a. a list) hk est censé être équivalent à t list pour tout type t.
Les Défis des Types de Haut Niveau
Un problème majeur réside dans le fait que ('a,'d) hk est un type beaucoup plus vaste. Nous devons nous assurer que dans (t,exists a. a list) hk, l’index t est exactement celui que nous avons caché dans la quantification existentielle. Cela nécessite des paires dépendantes, qui ne sont pas prises en charge en OCaml. Cependant, il existe une solution : tant que nous contrôlons les producteurs de valeurs de ce type, nous pouvons garantir que seules les valeurs satisfaisant cette condition sont créées.
Pour être plus concret, nous devons nous assurer que la seule manière de produire des valeurs de type ('a,'d) hk est d’utiliser des fonctions comme inj: 'a list -> ('a, exists a. a list) hk, qui exposent le même index qu’elles cachent. À un moment donné, le vérificateur de type exigera une preuve lors de l’implémentation de la correspondance inverse ('a, exists a. a list) hk -> 'a list et de l’extraction de la liste du type existentiel. Plusieurs méthodes peuvent être utilisées pour fournir cette preuve.
Implémentation Simple et Efficace
La méthode la plus simple consiste à affirmer que la condition est toujours respectée pour toutes les valeurs de type ('a,'d) hk effectivement produites. Nous pouvons documenter cette preuve sur un document ou dans un fichier .v. Cela conduit à une implémentation remarquablement simple, qui ne fait rien d’autre que d’appliquer l’identité.
module HK : sig
type ('a,'d) hk (* abstrait *)
module MakeHK : functor (S: sig type 'a t end) -> sig
type anyt (* aussi abstrait *)
val inj : 'a S.t -> ('a,anyt) hk
val prj : ('a,anyt) hk -> 'a S.t
end
end=struct
type ('a,'d) hk='d
module MakeHK(S:sig type 'a t end)=struct
type anyt=Obj.t
let inj : 'a S.t -> ('a,anyt) hk=Obj.repr
let prj : ('a,anyt) hk -> 'a S.t=Obj.obj
end
end
Le code ci-dessus montre une autre implémentation simple sans utiliser de magie Obj.
Enrichissement de la Signature DSL
Après avoir enrichi la signature sym de la DSL avec des types de haut niveau fictifs, nous pouvons réécrire l’exemple précédent SymEx1 sous forme de fonction (un terme) plutôt que de functor :
let sym_ex1 (type d) (module I:(sym_hk with type anyt=d)) : (_,d) HK.hk= let open I in let t1=add (add (int 1) (int 2)) (int 3) |> inj in (* terme intermédiaire *) let res=if_ (iszero t1) (int 0) (add t1 (int 1)) in inj res
Cette fonction peut être évaluée simplement comme suit :
sym_ex1
Conclusions sur les Technologies
- Nous avons exploré différentes méthodes pour abstraire un constructeur de type, ou pour rédiger des termes paramétrés par une interface lorsque celle-ci implique un type polymorphe. Même si le langage ne prend pas en charge directement la polymorphie des constructeurs de type, il est possible de réaliser cette paramétrisation d’interface de plusieurs manières :
- Abstraction d’interface sous forme d’abstraction de foncteur
- Réduction de la polymorphie de type supérieur à la polymorphie ordinaire, en établissant une bijection entre les constructeurs de type et les types ordinaires
- Cacher la polymorphie des implémentations de DSL derrière une algèbre initiale (si l’interface est algébrique, ce qui est souvent le cas dans les intégrations DSL sans balise finale)
- Et dans certains cas, la polymorphie de type supérieur n’est pas réellement nécessaire après un examen approfondi
Références
Le code complet avec des tests et un développement détaillé
