
. et les modules¶Redéfinissons, pour l'exemple, une partie du module List.
module LList = struct
type 'a llist = Empty | Cons of 'a cell
and 'a cell = {hd: 'a; tl: 'a llist}
let empty = Empty
let cons x l = Cons {hd=x; tl=l}
exception Empty_list
end
module LList :
sig
type 'a llist = Empty | Cons of 'a cell
and 'a cell = { hd : 'a; tl : 'a llist; }
val empty : 'a llist
val cons : 'a -> 'a llist -> 'a llist
exception Empty_list
end
Je pourrais définir la fonction hd à l'intérieur du module LList
module LList_possible = struct
[...]
let hd = function
| Empty -> raise Empty_list
| Cons cell -> cell.hd
[...]
end
Mais je peux aussi vouloir définir la fonction hd à l'extérieur du module.
Comment faire?
Il me faut parler des constructeurs Empty et Cons, de l'exception Empty_list, qui sont définis dans l'espace de nom du module LList.
Comme je veux définir hd à l'extérieur du module LList, je n'ai pas accès directement à cet espace de nom,
je dois utiliser la notation LList.
let hd = function
| LList.Empty -> raise LList.Empty_list
| LList.Cons cell -> cell.LList.hd
val hd : 'a LList.llist -> 'a = <fun>
open et let open¶Il est possible de charger l'espace de noms d'un module M en ajoutant open M. Toutes les définitions de M sont accessibles sans la notation M. dans la suite.
C'est un peu le from/import de Python...
module M = struct let x = 1 end
let _ = M.x
open M
let _ = x
module M : sig val x : int end
- : int = 1
- : int = 1
Le risque d'utiliser open est le même que celui avec from/import en Python: on risque d'écraser des définitions existantes.
let s = "Charlie"
module M = struct let s = "Fred" end
open M
(* on a perdu Charlie! *)
let _ = s
val s : string = "Charlie"
module M : sig val s : string end
- : string = "Fred"
Si l'on pouvait "refermer" le open M, on retrouverait Charlie!
Comment faire?
Solution 1 la syntaxe let open M in ...
let hd l =
let open LList in
match l with
| Empty -> raise Empty_list
| Cons cell -> cell.hd
val hd : 'a LList.llist -> 'a = <fun>
Empty (* erreur: on a "refermé" MList *)
File "[68]", line 1, characters 0-5:
1 | Empty (* erreur: on a "refermé" MList *)
^^^^^
Error: Unbound constructor Empty
Solution 2 la syntaxe M.(...)
let rec somme l = match l with
| LList.Empty -> raise LList.Empty_list
| LList.Cons cell -> LList.(cell.hd + somme cell.tl)
val somme : int LList.llist -> int = <fun>
Revenons sur la notion de signature - ou interface, quand il s'agit de modules-fichiers.
Nous avons vu que la signature détermine ce qui est exporté par le module, ce qui est public.
Ce qui n'est pas annoncé dans la signature est à usage interne au module, donc privé.
module type S = sig val x : int end
(* tout module signé par S exporte un entier x, ET RIEN D'AUTRE *)
module type S = sig val x : int end
module M : S = struct (* un module signé avec S *)
let x = 1 (* public *)
let y = 2 (* privé *)
end
module M : S
let _ = M.x (* x est public, je peux en parler en dehors du module *)
- : int = 1
Au contraire, je ne peux pas parler des définitions privées à l'extérieur du module.
Et ce n'est pas parce que j'ouvre un module que j'accède à ses définitions "privées"
open M
let _ = y
File "[12]", line 2, characters 8-9:
2 | let _ = y
^
Error: Unbound value y
La signature d'un module peut permettre d'exporter une déclaration de type sans dire à quoi ce type est égal. On parle alors de type opaque, ou de type abstrait.
module type MAILER = sig
type address (* <- type opaque *)
type message = string (* <- type public *)
val send_mail : address -> message -> unit
exception IllegalMailAddress of string
val address_of_string : string -> address
val string_of_address : address -> string
end
module type MAILER =
sig
type address
type message = string
val send_mail : address -> message -> unit
exception IllegalMailAddress of string
val address_of_string : string -> address
val string_of_address : address -> string
end
Un type opaque t s'accompagne souvent de fonctions permettant de construire des objets de type t.
Dans l'exemple précédent, c'est la fonction address_of_string qui permet de construire une adresse. Il n'y a aucun autre moyen de construire une adresse (sauf à l'intérieur du module).
Je vais maintenant définir un module qui implémente la signature MAILER.
module Mailer : MAILER = struct (* <- notez le ":" *)
type address = string (* <- définition privée du type opaque *)
type message = string
let send_mail dst title =
Format.sprintf "mail -s %s %s" title dst |> Unix.system |> ignore
exception IllegalMailAddress of string
let address_of_string str =
if String.contains str '@'
then str
else raise (IllegalMailAddress str)
let string_of_address addr = addr
end
module Mailer : MAILER
A l'extérieur du module, j'ignore que address est un alias du type string. Je ne peux donc pas passer directement une chaîne de caractères en paramètre à sendmail. Je dois "construire" une addresse en utilisant la fonction address_of_string.
let () = Mailer.send_mail "titi@unice.fr" "hello!"
File "[15]", line 1, characters 26-41:
1 | let () = Mailer.send_mail "titi@unice.fr" "hello!"
^^^^^^^^^^^^^^^
Error: This expression has type string but an expression was expected of type
Mailer.address
let () =
Mailer.send_mail (Mailer.address_of_string "titi@unice.fr") "hello!"
Null message body; hope that's ok
Comme précédemment, ouvrir le module avec open ne change rien au problème: open M ne fait rentrer dans l'espace de nom que les définitions exportées par le module M, celles qui sont cachées restent cachées.
open Mailer
let () = Mailer.send_mail "titi@unice.fr" "hello!"
File "[17]", line 2, characters 26-41:
2 | let () = Mailer.send_mail "titi@unice.fr" "hello!"
^^^^^^^^^^^^^^^
Error: This expression has type string but an expression was expected of type
Mailer.address
On utilise souvent les modules pour représenter des structures de données comme des listes, des arbres, des "ensembles", des piles, des files, etc.
Ces structures de données sont des "conteneurs" de données. Le type des données contenues est un paramètre ajustable.
On veut pouvoir manipuler de la même façon des listes d'entiers et des listes de flottants.
Il y a deux façons de gérer cette paramétricité:
Pour illustrer ces deux formes de paramétricité, nous allons prendre un exemple simple: les piles.
Rappelons qu'une pile est un conteneur LIFO (last in, first out):

Pile avec type polymorphe¶Je commence par déclarer une signature pour mon module. En plus des fonctions qui permettent de manipuler une pile, mon module devra contenir :
module type PILE = sig
type 'a pile (* le type d'une pile d'objets de type 'a *)
val pile_vide : 'a pile (* la constante pile vide *)
val empile : 'a -> 'a pile -> 'a pile
exception Pile_vide (* levée par depile et sommet *)
val depile : 'a pile -> 'a pile
val sommet : 'a pile -> 'a
end
module type PILE =
sig
type 'a pile
val pile_vide : 'a pile
val empile : 'a -> 'a pile -> 'a pile
exception Pile_vide
val depile : 'a pile -> 'a pile
val sommet : 'a pile -> 'a
end
Je dois maintenant implémenter cette signature.
Il y a plusieurs possibilités, mais la plus naturelle consiste à représenter une pile à l'aide d'une liste.
Je vais donc écrire un module qui définira le type 'a pile comme égal à 'a list.
module Pile = struct
type 'a pile = 'a list (* <- je concrétise le type opaque abstrait 'a pile *)
let pile_vide = []
let empile x p = x :: p
exception Pile_vide
let depile p = match p with
| [] -> raise Pile_vide
| _ :: p2 -> p2
let sommet p =
try List.hd p
with Failure _ -> raise Pile_vide
end
module Pile :
sig
type 'a pile = 'a list
val pile_vide : 'a list
val empile : 'a -> 'a list -> 'a list
exception Pile_vide
val depile : 'a list -> 'a list
val sommet : 'a list -> 'a
end
include¶Je voudrais maintenant rajouter des fonctions to_string, sort, et sum à mon module pour pouvoir afficher, trier, ou sommer une pile.
Le type polymorphe 'a pile me pose un problème: en effet, je ne sais pas à l'avance comment je dois afficher un objet de type 'a, ni comment je dois comparer ou sommer deux objets de type 'a.
La solution, déjà vue avec les listes, consiste à rajouter des paramètres aux fonctions to_string, sort, et sum pour fixer comment je dois gérer mes objets de type 'a.
Plus précisément, si j'ai une pile pile1 de type int pile, à l'aide de mon module Pile, je pourrai
Pile.to_string string_of_int pile1Pile.sort compare pile1 Pile.sum (+) 0 pile1Je vais définir une nouvelle signature PILE2 pour mon module de piles imprimables, triables, et sommables.
Pour éviter de recopier le début de la signature PILE, je vais utiliser le mot-clé include.
module type PILE2 = sig
include PILE (* copier-collé du contenu de la signature PILE *)
val to_string : ('a -> string) -> 'a pile -> string
val sort : ('a -> 'a -> int) -> 'a pile -> 'a pile
val sum : ('a -> 'a -> 'a) -> 'a -> 'a pile -> 'a
end
module type PILE2 =
sig
type 'a pile
val pile_vide : 'a pile
val empile : 'a -> 'a pile -> 'a pile
exception Pile_vide
val depile : 'a pile -> 'a pile
val sommet : 'a pile -> 'a
val to_string : ('a -> string) -> 'a pile -> string
val sort : ('a -> 'a -> int) -> 'a pile -> 'a pile
val sum : ('a -> 'a -> 'a) -> 'a -> 'a pile -> 'a
end
Attention à ne pas confondre open et include
open change l'espace de noms, mais il n'introduit pas de déclarationsinclude ajoute des déclarations; c'est une sorte de "copier-collé"
De la même façon, je vais définir un module Pile2 qui implémente la signature PILE2.
module Pile2 = struct
include Pile
let to_string f pile = (String.concat "|" (List.map f pile)) ^ "]"
let sort cmp pile = List.sort cmp pile
let sum plus zero pile = List.fold_left plus zero pile
end
module Pile2 :
sig
type 'a pile = 'a list
val pile_vide : 'a list
val empile : 'a -> 'a list -> 'a list
exception Pile_vide
val depile : 'a list -> 'a list
val sommet : 'a list -> 'a
val to_string : ('a -> string) -> 'a list -> string
val sort : ('a -> 'a -> int) -> 'a list -> 'a list
val sum : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
end
let p = Pile2.(pile_vide |> empile 1 |> empile 2 |> empile 3) in
Pile2.to_string string_of_int p
- : string = "3|2|1]"
Pile avec foncteur¶Dans l'exemple précédent, on avait besoin d'avoir quelques opérations élémentaires sur les objets de type 'a que l'on allait mettre dans les piles.
Dans cette deuxième approche, je vais commencer par regrouper toutes les opérations élémentaires dont j'ai besoin dans une signature.
module type EMPILABLE = sig
type t (* <- le type 'a de tout à l'heure, maintenant opaque *)
(* les opérations élémentaires sur des objets empilables *)
val to_string : t -> string (* afficher *)
val compare : t -> t -> int (* comparer *)
val add : t -> t -> t (* ajouter *)
val null : t (* neutre de l'addition *)
end
module type EMPILABLE =
sig
type t
val to_string : t -> string
val compare : t -> t -> int
val add : t -> t -> t
val null : t
end
Ceci fait, je peux maintenant définir un foncteur Pile qui prend en paramètre un module E d'objets empilables.
Je vais utiliser la syntaxe module Pile (E:EMPILABLE) = ....
Ce foncteur Pile n'est pas encore un module: il faudra que je fixe le module E pour obtenir un module.
C'est une sorte de "moule" pour fabriquer des modules "pile de ...".
Par exemple, une fois que j'aurai défini un module EntierEmpilable, je pourrai fabriquer un module
Pile_Entiers en utilisant mon foncteur et en instanciant E avec EntierEmpilable.
À l'intérieur du module Pile, pour afficher un objet empilable, j'utiliserai E.to_string. Ma fonction
Pile.to_string n'aura donc plus besoin du paramètre de type 'a -> string de tout à l'heure, c'est le choix du module E qui fixera la fonction d'affichage des objets empilés.
Assez parlé, voyons ce que cela donne...
module Pile3 (E : EMPILABLE) = struct
type pile = E.t list (* <- le type des piles n'est plus un type polymorphe *)
let empile x p = x :: p let depile = List.tl let sommet = List.hd
let to_string pile = (String.concat "|" (List.map E.to_string pile)) ^ "]"
let sum pile = List.fold_left E.add E.null pile
let sort pile = List.sort E.compare pile
end
module Pile3 :
functor (E : EMPILABLE) ->
sig
type pile = E.t list
val empile : 'a -> 'a list -> 'a list
val depile : 'a list -> 'a list
val sommet : 'a list -> 'a
val to_string : E.t list -> string
val sum : E.t list -> E.t
val sort : E.t list -> E.t list
end
module EntierEmpilable : EMPILABLE = struct
type t = int (* <- le type opaque de EMPILABLE doit être "instancié" *)
let to_string = string_of_int
let compare = compare
let add = (+)
let null = 0
end
module Pile_Entiers = Pile3(EntierEmpilable)
module EntierEmpilable : EMPILABLE
module Pile_Entiers :
sig
type pile = EntierEmpilable.t list
val empile : 'a -> 'a list -> 'a list
val depile : 'a list -> 'a list
val sommet : 'a list -> 'a
val to_string : EntierEmpilable.t list -> string
val sum : EntierEmpilable.t list -> EntierEmpilable.t
val sort : EntierEmpilable.t list -> EntierEmpilable.t list
end
Set.Make de la librairie standard¶Vous aurez peut-être l'occasion d'écrire des foncteurs, mais vous aurez aussi, et surtout, l'occasion d'avoir à les utiliser.
La librairie standard comporte un certain nombre de foncteurs; en particulier, si vous voulez une structure de données efficace pour représenter un "ensemble de ...", vous pourrez utiliser le module Set, mais il vous faudra en passer par un foncteur...
En effet, de même qu'en Python un ensemble ne pouvait contenir que des données "hashables", les modules ensembles d'OCaml ne peuvent accueillir que des objets "ordonnables".
Pour créer un module "ensemble de truc", je vais donc devoir créer un module Truc puis générer un module EnsembleTruc en appelant le foncteur Set.Make. Au final, vous écrirez quelque chose comme
module EnsembleTruc = Set.Make(Truc)
let paire truc1 truc2 =
EnsembleTruc.(union (singleton truc1) (singleton truc2))
Si on consulte le manuel de référence, on voit en effet que le module Set contient les déclarations suivantes
module Set = struct
module type S = sig ... end
(* la signature d'un module "ensemble de trucs" *)
module type OrderedType = sig ... end
(* la signature d'un module "ordonnable" *)
module Make (Elt:OrderedType) : S = struct ... end
(* le foncteur OrderedType -> S *)
end
Ainsi, mon module Truc devra avoir la signature Set.OrderedType
Toujours dans le manuel de référence, on trouve la définition de la signature Set.OrderedType
module type OrderedType = sig
type t (* the type of set elements *)
val compare : t -> t -> int (* a total ordering function over the set elements *)
end
Supposons que je veuille faire des ensembles de couples d'entiers qui représentent des fractions.
Pour comparer le couple (a,b) et le couple (c,d), je vais donc regarder le signe de $ad - bc$.
module CoupleEntiers = struct
type t = int * int
let compare (a,b) (c,d) = a * d - b * c
end
module EnsembleFractions = Set.Make(CoupleEntiers)
module CoupleEntiers : sig type t = int * int val compare : int * int -> int * int -> int end
module EnsembleFractions :
sig
type elt = CoupleEntiers.t
type t = Set.Make(CoupleEntiers).t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val disjoint : t -> t -> bool
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val map : (elt -> elt) -> t -> t
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val min_elt_opt : t -> elt option
val max_elt : t -> elt
val max_elt_opt : t -> elt option
val choose : t -> elt
val choose_opt : t -> elt option
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val find_opt : elt -> t -> elt option
val find_first : (elt -> bool) -> t -> elt
val find_first_opt : (elt -> bool) -> t -> elt option
val find_last : (elt -> bool) -> t -> elt
val find_last_opt : (elt -> bool) -> t -> elt option
val of_list : elt list -> t
val to_seq_from : elt -> t -> elt Seq.t
val to_seq : t -> elt Seq.t
val add_seq : elt Seq.t -> t -> t
val of_seq : elt Seq.t -> t
end
let s = EnsembleFractions.of_list [(1,2); (3,4); (6,8)]
let l = EnsembleFractions.elements s
val s : EnsembleFractions.t = <abstr>
val l : EnsembleFractions.elt list = [(1, 2); (3, 4)]
C'est assez lourd pour manipuler des ensembles, certes...
Astuce
Je peux économiser du code. Par exemple, je peux fabriquer le module IntSet des ensembles d'entiers en une seule ligne, en n'introduisant pas un module Int qui serait d'usage très limité.
module IntSet = Set.Make(struct type t = int let compare = compare end)
module IntSet :
sig
type elt = int
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val disjoint : t -> t -> bool
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val map : (elt -> elt) -> t -> t
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val min_elt_opt : t -> elt option
val max_elt : t -> elt
val max_elt_opt : t -> elt option
val choose : t -> elt
val choose_opt : t -> elt option
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val find_opt : elt -> t -> elt option
val find_first : (elt -> bool) -> t -> elt
val find_first_opt : (elt -> bool) -> t -> elt option
val find_last : (elt -> bool) -> t -> elt
val find_last_opt : (elt -> bool) -> t -> elt option
val of_list : elt list -> t
val to_seq_from : elt -> t -> elt Seq.t
val to_seq : t -> elt Seq.t
val add_seq : elt Seq.t -> t -> t
val of_seq : elt Seq.t -> t
end
Comment savoir quelles opérations existent sur les ensembles?
Il suffit d'aller voir la documentation de la signature Set.S dans le manuel de référence.
Nous avons vu deux façons de déclarer un module Pile "paramétré" par le type des éléments qui seront empilés
'a pilet à la place de la variable de type 'a.Dans les deux cas, le but recherché est le polymorphisme paramétrique.
OCaml s'assure que le typage paramétrique ne casse pas les règles de typage. Certaines situations nécessitent un peu plus de travail que ce que nous avons vu pour arriver à satisfaire les contraintes de type, et requièrent l'emploi du mot-clé with, que nous verrons plus loin.
Nous avons fait un module Pile qui manipule des piles sans les modifier: quand on empile un élément sur une pile p, on obtient une pile p' qui contient le résultat de l'opération, mais la pile p reste inchangée.
empile : 'a -> 'a pile -> 'a pile
On parle de structure de données "fonctionnelle" ou plus justement de structure de données persistante.
Une autre approche consiste à modifier la pile passée en paramètre plutôt que de renvoyer une nouvelle pile.
empile : 'a -> 'a pile -> unit
On parle alors de structure de donnée "mutable", ou "impérative", ou plus justement de structure de données non persistante.
Chaque approche a ses avantages, mais un programmeur rigoureux évitera de mélanger les deux en général.
Remarque: persistant ne veut pas forcément dire immutable; certaines structures de données persistantes "font comme si" elles étaient immutables, mais utilisent en interne des mutations (voir le livre programmer avec Ocaml pour de nombreux exemples).
Nous allons maintenant écrire un module qui implémente des piles non persistantes. Commençons par fixer la signature.
module type PILE_IMP =
type 'a pile
with¶Le mot-clé with permet de créer une nouvelle signature en instanciant un type opaque dans une signature.
module type T = sig
type t (* <- opaque *)
val null : t
end
module type T = sig type t val null : t end
module type INT = T with type t = int (* <- j'instancie t avec int *)
module type INT = sig type t = int val null : t end
module Int : INT = struct
type t = int
let null = 0
end
module Int : INT
Int.null
- : Int.t = 0
Si j'avais signé Int avec T, Int.null s'afficherait comme <abstr>.
Nous allons maintenant définir quelques structures algébriques que certains ont dû rencontrer dans leurs cours de math:
Avertissement Le but premier est d'illustrer l'utilisation des modules, des foncteurs et quelques usages du mot-clé with. Nous nous inspirons des structures algébriques que vous verriez en mathématiques, mais les axiomes que satisfont ces structures algébriques ne vont pas être modélisés dans OCaml... il nous faudrait un langage plus riche. On verra à la fin comment tester ces axiomes de manière automatique pour les structures algébriques finies.
Commençons par les monoides: un monoïde définit une loi de composition interne qui admet un élément neutre.
module type MONOIDE = sig
type t (* le type des éléments du monoide *)
val compose : t -> t -> t (* la loi de composition interne *)
val neutre : t (* l'élément neutre *)
end
module type MONOIDE = sig type t val compose : t -> t -> t val neutre : t end
Définissons quelques monoides pour illustrer cette notion.
module N_Add = struct (* les entiers avec l'addition et le neutre 0 *)
type t = int
let compose n m = n + m
let neutre = 0
end
module N_Add : sig type t = int val compose : int -> int -> int val neutre : int end
module N_Mult = struct (* les entiers non nuls avec la multiplication et le neutre 1 *)
type t = int
let compose n m = n * m
let neutre = 1
end
module N_Mult : sig type t = int val compose : int -> int -> int val neutre : int end
module Mots = struct (* les mots avec la concaténation et le mot vide *)
type t = string
let compose s1 s2 = s1 ^ s2
let neutre = ""
end
module Mots :
sig
type t = string
val compose : string -> string -> string
val neutre : string
end
module Bool_Xor = struct (* les booléens avec le "ou exclusif" *)
type t = bool
let compose b1 b2 = b1 <> b2
let neutre = false
end
module Bool_Xor : sig type t = bool val compose : 'a -> 'a -> bool val neutre : bool end
module Bool_And = struct (* les booléens avec le "et" *)
type t = bool
let compose b1 b2 = b1 && b2
let neutre = true
end
module Bool_And : sig type t = bool val compose : bool -> bool -> bool val neutre : bool end
Passons maintenant aux anneaux.
Un anneau est la donnée de deux lois de composition interne sur le même ensemble, chacune définissant un monoïde.
module type ANNEAU = sig
type t
val add : t -> t -> t
val mult : t -> t -> t
val zero : t
val un : t
end
module type ANNEAU =
sig
type t
val add : t -> t -> t
val mult : t -> t -> t
val zero : t
val un : t
end
Traduisons l'idée qu'un anneau est constitué de deux monoides par un foncteur. Toute la difficulté est d'exprimer que les monoides portent "sur un même ensemble".
module Make_Anneau (Add: MONOIDE) (Mult: MONOIDE with type t = Add.t)
: ANNEAU with type t = Add.t
= struct
type t = Add.t
let add = Add.compose
let mult = Mult.compose
let zero = Add.neutre
let un = Mult.neutre
end
module Make_Anneau :
functor
(Add : MONOIDE) (Mult : sig
type t = Add.t
val compose : t -> t -> t
val neutre : t
end) ->
sig
type t = Add.t
val add : t -> t -> t
val mult : t -> t -> t
val zero : t
val un : t
end
module N = Make_Anneau(N_Add)(N_Mult)
module N :
sig
type t = N_Add.t
val add : t -> t -> t
val mult : t -> t -> t
val zero : t
val un : t
end
module Bool = Make_Anneau(Bool_Xor)(Bool_And)
module Bool :
sig
type t = Bool_Xor.t
val add : t -> t -> t
val mult : t -> t -> t
val zero : t
val un : t
end
module MalForme = Make_Anneau(N_Add)(Mots)
File "[58]", line 1, characters 37-41:
1 | module MalForme = Make_Anneau(N_Add)(Mots)
^^^^
Error: Signature mismatch:
...
Type declarations do not match:
type t = string
is not included in
type t = N_Add.t
File "[55]", line 1, characters 54-68: Expected declaration
File "[51]", line 2, characters 3-18: Actual declaration
On pourrait continuer ainsi et définir l'anneau des polynomes, l'anneau des matrices, etc. Vous le ferez peut-être en TP?
Pour conclure, nous allons simplement indiquer comment on peut formaliser les axiomes d'un monoïde et les tester à l'aide d'un foncteur de test.
Rappelons ces axiomes
l'axiome d'associativité $$\forall x,y,z\in M. (xy)z~=~x(yz)$$
l'axiome de l'élément neutre $$\forall x\in M. xe = ex = x$$
Pour pouvoir écrire nos axiomes, nous avons donc besoin de quantifier sur les éléments de l'ensemble.
module type MONOIDE_TESTABLE = sig
include MONOIDE
val forall : (t -> bool) -> bool
end
module Test_Monoide(M : MONOIDE_TESTABLE) = struct
let ( * ) = M.compose
let () = (* test de l'axiome d'associativité *)
assert (M.forall (fun x -> (M.forall (fun y -> M.forall (fun z ->
(x*y)*z = x*(y*z)
)))))
let e = M.neutre
let () = (* test de l'axiome du neutre *)
assert (M.forall (fun x ->
x*e=x && e*x=x
))
end
module type MONOIDE_TESTABLE =
sig
type t
val compose : t -> t -> t
val neutre : t
val forall : (t -> bool) -> bool
end
module Test_Monoide :
functor (M : MONOIDE_TESTABLE) ->
sig val ( * ) : M.t -> M.t -> M.t val e : M.t end
module Bool_Xor_Testable = struct
include Bool_Xor
let forall enonce = (enonce false) && (enonce true)
end
module Bool_Xor_Testable :
sig
type t = bool
val compose : 'a -> 'a -> bool
val neutre : bool
val forall : (bool -> bool) -> bool
end
module Test_Bool = Test_Monoide(Bool_Xor_Testable)
(* pas d'erreur: le xor est bien associatif et admet bien l'élément neutre false *)
module Test_Bool :
sig
val ( * ) :
Bool_Xor_Testable.t -> Bool_Xor_Testable.t -> Bool_Xor_Testable.t
val e : Bool_Xor_Testable.t
end
Exercice d'algèbre assistée par ordinateur (requis: la notion de groupe)