diff options
Diffstat (limited to 'content')
| -rw-r--r-- | content/Informatique/2017-01-01-gadt.rst | 594 | ||||
| -rw-r--r-- | content/images/catalog/catalog.jpg | bin | 0 -> 25782 bytes | |||
| -rw-r--r-- | content/images/catalog/catalog_75.jpg | bin | 0 -> 8301 bytes | |||
| -rw-r--r-- | content/resources/catalog.ml | 196 | 
4 files changed, 790 insertions, 0 deletions
| diff --git a/content/Informatique/2017-01-01-gadt.rst b/content/Informatique/2017-01-01-gadt.rst new file mode 100644 index 0000000..ce34ad5 --- /dev/null +++ b/content/Informatique/2017-01-01-gadt.rst @@ -0,0 +1,594 @@ +.. -*- mode: rst -*- +.. -*-  coding: utf-8 -*- + +=================================================== +Écrire un catalogue dynamique de fonctions en OCaml +=================================================== + +:date: 2017-01-01 +:tags: OCaml +:logo: /images/catalog/catalog_75.jpg +:summary: |summary| + +.. default-role:: literal + +.. figure:: {filename}/images/catalog/catalog.jpg +    :figwidth: 250 +    :figclass: floatright +    :alt: Furniture + +    Image : `Adam mayer`_ (creativecommons_) + +.. _Adam mayer: https://www.flickr.com/photos/phooky/12687690/in/photostream/ +.. _creativecommons: https://creativecommons.org/licenses/by-sa/2.0/ + +|summary| + +.. |summary| replace:: + +  J'ai commencé à écrire un tableur. Je présenterai le résultat une autre fois, +  quand le sujet aura plus avancé, et je vais ici me focaliser sur une partie du +  code de ce tableur : le catalogue de fonction, en expliquant comment stocker +  ensemble des fonctions prenant des paramètres différents, et comment mettre en +  place l'appel à ces fonctions. + +Le code est téléchargeable à la fin de l'article. + +.. contents:: \ +  :depth: 1 +  :backlinks: top + +Présentation +============ + +Un tableur donc, comprend un mini langage. Quand on écrit dans une cellule +`= 2 + 2` ou `sum(A1:C2)` on exécute une instruction et pour obtenir un +résultat. Ce langage contient : + +:des valeurs: +    `2` + +:des fonctions: +    `+` ou `sum` + +:des références: +    `A1` (qui contient à son tour le résultat d'un autre calcul) + + +Tout cela peut être combiné, il est ainsi possible d'écrire `A2 + 1` ou +`sum(C3:E4) + A2`, et le nombre de fonctions disponibles s'approche de la +centaine. Dans le tableur, je souhaitai pouvoir enrichir les fonctions +disponibles en en ajoutant sans avoir à recompiler l'application (par exemple +avec un système de *plugin*). + +En quelque sorte, mon but est de pouvoir enregistrer la fonction dans un +catalogue, et que celle-ci soit appelée automatiquement. Par exemple on peut +imaginer quelque chose comme : + +.. code-block:: ocaml + +    (* Enregistrer la fonction + dans le catalogue : +        la fonction prend deux paramètres, tous les deux de type int +        elle renvoie une valeur également de type int +    *) +    Catalog.register2 "+"  (t_int, t_int) t_int (fun x y -> x + y); + +    (* Enregistrer la fonction sum dans le catalogue +        la fonction prend un paramètre, qui est une liste une int +        elle renvoie une valeur, qui est de type int +    *) +    register1 "sum" (t_list t_int) t_int (fun x ->  List.fold_left (+) 0 x); + +    (* Appeler la fonction "+" avec deux paramètres *) +    let arg1 = … +    and arg2 = … in +    eval2 "+" arg1 arg2; + +Je vais montrer comment y parvenir à travers une méthode qui *garantie* à la +compilation que les fonctions font bien ce que l'on attend d'elles. + +Les garanties d'un compilateur +============================== + +Du point de vue d'un programmeur, on s'attend à avoir certaines garanties de la +part du compilateur du programme : + +1. La cohérence des types. + +   .. code-block:: ocaml + +    let ajoute_2 (x:int) = x + 2 + +   Dans la ligne écrite ci-dessus, nous avons déclaré que la variable `x` était +   de type `int`. Il est donc inutile de tester si c'est bien le cas (en OCaml +   du moins, mais certains langages ne permettent pas d'ajouter cette +   information). + +   Si le programme a été compilé, alors on peut avoir l'assurance que la +   fonction sera appelée uniquement avec des variables de type `int`. + +   Cette contrainte peut être vérifiée au moment de la compilation du programme. + +2. La cohérence durant l'exécution. + +   Si le langage permet d'avoir plusieurs fonctions avec le même +   nom, (par exemple une fonction `+` qui ajoute deux nombres, et une fonction +   `+` qui ajoute un nombre à une date, alors je dois être sûr qu'au moment où +   j'appelle `date_du jour + 2`, je n'appelle pas la même fonction qu'au moment +   où j'appelle `2 + 2`. + +   Puisque l'on ne sait pas à l'avance quelle fonction sera appelée (puisque +   cela est réalisé de manière dynamique), il est nécessaire de mettre en place +   un contrôle à chaque appel de fonction. + +Et maintenant, quelle fonction vais-je devoir appeler quand j'écris `A2 + 2`. +On ne sait pas quelle est la valeur de `A2`, et l'on ne peut donc pas savoir +quelle est la fonction à appeler. Il nous faut donc avoir une information pour +être sûr de pouvoir garantir ces deux contraintes à tout moment dans le +programme : le type. + +Typons nos données +================== + +Dans un langage de programmation typé, la nature de chaque variable est +connue (liste, booléen, nombre entier…), le compilateur est donc capable de +savoir quelle est la fonction à appeler à partir de cette information. Eh bien +pour s'en sortir, nous allons devoir faire pareil, et, à tout moment, conserver +cette information. + +Par exemple dans `A2 + 2`, on ne sait pas quelle est la fonction `+` à +appeler, mais on connait le contenu de la variable `A2`. En suivant le fil des +valeurs, on est ainsi capable de trouver les bonnes informations (et lever une +erreur en disant qu'il n'est pas possible d'appeler la fonction `+` en lui +donnant des arguments de types `bool` et `int`). + +Quels sont les types dont nous avons besoin ? Je propose que nous fassions +notre exemple avec deux seulement pour commencer : les `int` et les `bool`. + +.. code-block:: ocaml + +    (*On définit un type générique, qui peut être paramétré*) +    type 'a typ + +    (*Et deux variantes*) +    val t_bool: bool typ +    val t_int:  int  typ + + +Ici, nous venons de déclarer un type nommé `typ` (quelle originalité !) qui +peut être d'un type quelconque. Cette information est destinée au compilateur +(elle ne sera plus disponible après), et lui permet de mettre en place des +contraintes dans les signatures (par exemple une fonction qui prend en +paramètre un `bool typ` ne pourra pas être appelée avec un argument de type +`int typ`). + +Ce type est proposé sous forme de deux déclinaisons, qui correspondent aux deux +variantes que nous souhaitons prendre en charge dans notre application. + +En utilisant cette définition, il devient facile de donner la signature de la +fonction `register2` que nous avons cité au début de l'article : + +.. code-block:: ocaml + +    val register2: +      string ->           (* Le nom de la fonction à enregistrer *) +      ('a typ * 'b typ) ->(* Sa signature *) +      'c typ ->           (* Le type de retour *) +      ( 'a -> 'b -> 'c)   (* La fonction en elle-même*) +      -> unit + +Il faut ici prêter attentions aux `a` `b` `c` qui apparaissent. Le `a` et le +`b` qui apparaissent dans la signature signifient que la fonction prend en +paramètre un type `a` et `b`. Si ces valeurs ne correspondent pas, le +compilateur OCaml va rejeter le programme en indiquant que les valeurs sont +différentes. + +Cette solution permet de répondre au problème de la *cohérence des types* que +nous avons expliqué plus haut : les contrôles sont désormais à la charge du +compilateur. + +Et concrètement ? +================= + +En présentant notre type de données `'a typ`, j'ai précisé que le `'a` était +destiné au compilateur et n'était plus disponible après. Si l'on souhaite juste +s'en servir pour mettre en place des contrôles à la compilation, alors il est +possible de l'implémenter sous la forme d'un `type fantôme (en)`_. Mais dans +notre utilisation, cela n'est pas suffisant : il faut conserver cette +information pour contrôler au moment d'un appel que les paramètres donnés +correspondent à ceux attendus. + +.. _type fantôme (en): https://wiki.haskell.org/Phantom_type + +C'est là qu'interviennent les GADTs. Cette syntaxe nous permet d'écrire un type +somme, et d'associer à chaque élément un type différent : + +.. code-block:: ocaml + +    type _ typ = +      | Bool: bool typ +      | Int: int typ + +Nous venons ici de créer un constructeur `Bool` (sans paramètres), ayant pour +type `bool typ` et un second constructeur `Int` ayant pour type `int typ`. Armé +de ces deux constructeurs, il est facile d'écrire les types `t_bool` et `t_int` +que nous avons défini dans notre signature : + +.. code-block:: ocaml + +    let t_bool = Bool +    and t_int = Int + +Pourquoi mettre en place un type somme ? +---------------------------------------- + +Cela permet de fermer la liste des types possibles : dans notre interface, nous +avons déclaré un type abstrait `'a typ` ouvert, mais en interne, nous aurons +juste à faire du *pattern matching* sur les constructeurs `Bool` et `Int`. On +peut ainsi tester l'exhaustivité des cas à chaque fois que l'on souhaite faire +une opération sur les types disponibles. + +Comment on l'utilise ? +---------------------- + +Alors, là il va falloir compliquer un peu l'écriture de notre code. En effet, +la fonction qui reçoit en paramètre notre GADT doit être capable de traiter des +paramètres de types différents, ce que le compilateur OCaml ne tolère pas par +défaut. Il faut explicitement déclarer nos paramètres (ce qui rend l'écriture +un peu plus verbeuse). + +Si l'on souhaite écrire une fonction qui retourne le nom de chaque type il va +falloir écrire notre fonction comme cela : + +.. code-block:: ocaml + +  let print_typ: type a. a typ -> string = begin function +    | Bool -> "Bool" +    | Int  -> "Int" +  end + + +Revenons en à nos données +========================= + +Maintenant que nos types sont posés, nous allons pouvoir traiter nos données de +la même manière. Pour commencer, nous allons créer un type de données qui sera +le *miroir* de celui utilisé pour déclarer nos types : + +.. code-block:: ocaml + +  type _ value = +    | Bool: bool -> bool value +    | Int:  int  -> int value + +La déclaration est similaire à celle du type `'a typ`, mais cette fois, les +constructeurs prennent chacun un paramètre (qui est en accord avec le type de +chaque valeur). + +Avec nos deux types `value` et `typ`, nous allons pouvoir faire des choses +intéressantes : + +Déduire le type à partir d'une valeur +------------------------------------- + +La fonction est assez simple (elle tient en quelques lignes), mais elle montre +comment il est possible de transposer l'information contenue dans la structure de +données : en effet, comme nos deux types peuvent être mis en correspondance — +l'information qu'ils portent est la même. Il est donc possible pour tout `a +value` de fournir un `a typ`, tout en conservant la cohérence de l'information +: + +.. code-block:: ocaml + +  (* Extract the type from a boxed value *) +  let type_of_value: type a. a value -> a typ = begin function +    | Bool b -> Bool +    | Int n -> Int +  end + +Dans le cadre de notre catalogue, cette fonction va permettre de transformer +les arguments donnés à l'appel de la fonction, pour les comparer avec la +signature de la fonction enregistrée. + +Construire une valeur à partir d'un type +---------------------------------------- + +Cette fois, il s'agit de l'opération inverse, mais nous avons besoin d'une +information supplémentaire (puisque le type `'a typ` est un type somme sans +paramètre). Par contre, nous pouvons demander au compilateur de s'assurer que +les valeurs données en paramètre de la fonction sont les bons : + +.. code-block:: ocaml + +  let build_value: type a. a typ -> a -> a value = fun typ content -> +    begin match typ, content with +        | Bool, x -> Bool x +        | Int, x  -> Int x +    end + +La signature de la fonction oblige à donner en paramètre un `a typ`, un `a` et +donne en retour un `a value`, et ce *quel que soit* le type de `a`. + +Dans notre catalogue de fonction, cette fonction nous permet de reconstruire +notre données, une fois que l'on a appelé la fonction enregistrée, en effet, on +connait le type de retour de la fonction, et la valeur est en accord avec ce +type. Avec ces deux informations, il est facile de reconstruire notre résultat. + +Construire un type existentiel +------------------------------ + +Jusqu'à présent, nous avons toujours créé des fonctions qui prenaient +l'information du type à traiter en paramètre. Si nous souhaitons créer une +fonction qui puisse retourner un résultat *de n'importe quel type* nous ne +pouvons procéder ainsi. + +Notre fonction `eval` doit être en mesure de retourner une donnée inconnue +(puisque cela dépend de la fonction appelée), et OCaml n'autorise pas une +fonction à retourner un type inconnu : + +.. code-block:: ocaml + +  TODO + +Pour pouvoir faire ce que l'on souhaite, il faut encapsuler notre retour dans +un type existentiel. Il s'agit d'un type qui ne porte pas l'information de la +donnée qu'il contient : + +.. code-block:: ocaml + +  type result = +    | Result : 'a value -> result + + +Avec ce type, il devient possible de coder le retour de nos fonctions +d'évaluations, (qui retourneront une valeur de type `result`) : + +.. code-block:: ocaml + +  (** Create a result from a known type and a value *) +  let inject: type a. a typ -> a -> result = fun typ res -> +    Result (build_value typ res) + +Cet type ne contient pas d'information sur son contenu, mais puisqu'il a été +créé à partir d'une valeur valide, il est possible de décomposer cette valeur. +Par exemple : + +.. code-block:: ocaml + +  (* Décompose le retour d'un appel *) +  let Result r = … in +  let type_of = type_of_value r in +  … + +Récupérer la valeur +------------------- + +La dernière chose dont nous avons besoin est de pouvoir extraire la valeur qui +est contenu dans notre type. Là encore le code est vraiment simple puisqu'il +s'agit de faire du *pattern matching* : + +.. code-block:: ocaml + +  (** Get the value out of the box *) +  let get_value_content: type a. a value -> a = function +    | Bool b -> b +    | Int n -> n + +On constate en lisant la signature que là encore, aucune information de type +n'est inventée, tout est déjà déduit à partir des données déjà existantes. + +Et notre dictionnaire ? +======================= + +Maintenant que les concepts sont posés, il ne reste qu'à les mettre en œuvre. +Nous allons représenter notre dictionnaire sous la forme d'une table +associative, dont la clef sera un couple `nom de la fonction * signature`, et +la valeur associée sera un triplet `signature * type de retour * fonction à +appeler`. + +Nous avons besoin de stocker la signature de la fonction pour la comparer avec +les paramètres donnés en arguments. Par contre, il sera là encore nécessaire de +l'encapsuler dans un type existentiel pour pouvoir l'utiliser de manière +générique : + + +.. code-block:: ocaml + +  type _ sig_typ = +    | T1: 'a typ -> 'a sig_typ +    | T2: 'a typ * 'b typ -> ('a * 'b) sig_typ + +  type t_signature = +    | Sig : 'a sig_typ -> t_signature + +`T1` est la signature d'une fonction n'ayant qu'un argument, `T2` est une +signature à deux paramètres. + +En présente de la même manière nos fonctions : + +.. code-block:: ocaml + +  type t_function = +    | Fn1: 'a typ * 'b typ * ('a -> 'b) -> t_function +    | Fn2: ('a * 'b) sig_typ * 'c typ * ('a -> 'b -> 'c) -> t_function + + +Une fonction peut se présenter comme ayant 1 ou 2 paramètres, et est dans tous +les cas, enregistrée avec : + +- Le type des arguments qu'elle reçoit +- Le type de retour +- La fonction à exécuter + +Remplissons notre catalogue +--------------------------- + +Avec ces nouveaux types, nous pouvons construire notre dictionnaire de données, +et y insérer nos fonctions à appeler : + +.. code-block:: ocaml + +  let (catalog:t_function Catalog.t ref) = ref Catalog.empty + +  let register name signature f = begin +    let name' = String.uppercase_ascii name in +    catalog := Catalog.add (name', signature) f !catalog +  end + +  let register2: type a b c. string -> (a typ * b typ) -> c typ -> ( a -> b -> c) -> unit = begin +    fun name (typ1, typ2) result f -> +      let signature = T2(typ1, typ2) in +      register name (Sig signature) (Fn2 (signature, result, f)) +  end + +La fonction `register2` correspond exactement à l'implémentation de celle +donnée dans l'introduction. Le catalogue est conservé comme une référence +mutable et mis à jour à à chaque appel de la fonction `register`. + +Appelons les fonctions +---------------------- + +L'appel d'une fonction va se décomposer en deux étapes : + +1. La recherche dans le catalogue d'une fonction ayant le même nom et la même +   signature que les arguments d'appels +2. Le contrôle que la fonction que l'on a pu obtenir présente bien la même +   signature que les arguments d'appels. + +Pourquoi ces deux étapes ? Car même si notre fonction `register2` empêche que +l'on écrive n'importe quoi dans notre catalogue, la structure du catalogue +autorise d'y insérer des données incohérentes. Le compilateur OCaml nous oblige +à faire le contrôle pour que l'on puisse appeler la fonction. + +Et comment fait-on ce contrôle ? Me direz-vous ? En contrôlant `l'égalité des +types`_ : le type `eq` présenté dans les exemples avancés est exactement ce +dont nous avons besoin, il suffit juste d'adapter la fonction `eq_type` donné +dans l'exemple pour tester un type de signature et le résultat est présenté +ci-dessous : + +.. _l'égalité des types: https://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec238 + +.. code-block:: ocaml + +  let find_function name signature = begin +    Catalog.find (String.uppercase_ascii name, (Sig signature)) !catalog +  end + +  let eval2 name (Result p1) (Result p2) = begin +    (* Construit la signature à partir des paramètres *) +    let signature = T2 ((type_of_value p1), (type_of_value p2)) in +    try +      (* Recherche dans le catalogue *) +      begin match find_function name signature with +      | Fn2 (fn_sig, returnType, f) -> +          (* Réalise le contrôle de type sur la signature de la fonction *) +          begin match eq_sig_typ signature fn_sig with Eq -> +            (* Appelle la fonction *) +            let result = f (get_value_content p1) (get_value_content p2) in +            (* Injecte le résultat de notre appel. *) +            inject returnType result +          end +      | _ -> raise Not_found +      end +    with Not_found -> +      print_error name signature; +      raise Not_found +  end + +La ligne la plus importante est celle-ci : + +.. code-block:: ocaml + +  begin match eq_sig_typ signature fn_sig with Eq -> + +La fonction `eq_sig_typ` prend en paramètres deux signatures, et renvoie `Eq` si +et seulement si les deux signatures sont identiques. Cette information est +déduite par le compilateur OCaml, et c'est seulement grâce à la présence de ce +contrôle qu'il autorise l'appel à une fonction inconnue à la compilation, avec +des paramètres également inconnus au moment de la compilation. + +.. note:: + +  Il est possible de se passer de ce double contrôle en réécrivant nous-même +  notre type `Map` pour garantir que les valeurs portent les même informations +  de type que les clefs, mais cela sort du cadre de cet article. + +Terminons +========= + +Tout est en place, il ne reste plus qu'à enregistrer les fonctions dans notre +catalogue : + +.. code-block:: ocaml + +  (*        nom   signature       retour fonction *) +  register2 "="  (t_int, t_int)   t_bool (=); +  register2 "<>" (t_int, t_int)   t_bool (<>); + +  register2 "+"  (t_int, t_int)   t_int  (+); +  register2 "*"  (t_int, t_int)   t_int  ( * ); +  register2 "/"  (t_int, t_int)   t_int  (/); +  register2 "-"  (t_int, t_int)   t_int  (-); + +  (*        nom   signature       retour fonction *) +  register2 "="  (t_bool, t_bool) t_bool (=); +  register2 "<>" (t_bool, t_bool) t_bool (<>); + +  register1 "not" t_bool          t_bool not; +  register2 "and"(t_bool, t_bool) t_bool (&&); +  register2 "or" (t_bool, t_bool) t_bool (||); + + +Et enfin testons : + + +.. code-block:: ocaml + +  let i2 = inject t_int 2 +  and i3 = inject t_int 3 +  and b1 = inject t_bool true in +  let r1 = eval2 "=" i2 i3 in         (* r1 vaut Bool false *) +  let r2 = eval1 "not" r1 in          (* r2 vaut Bool true *) +  let r3 = C.eval2 "=" b1 r2 in       (* r3 vaut Bool true *) +  let Result value = r3 in            (* Extrait la valeur *) +  match value with                    (* Teste le résultat *) +  | Int  n -> Printf.printf "%d\n" n +  | Bool b -> Printf.printf "%b\n" b  (* Doit afficher true *) + +.. code-block:: console + +  $ ocaml catalog.ml +  true + +Nous avons appelé ici la fonction `=` une fois sur des entiers, une fois sur +des booléens, et à chaque fois, la fonction à appeler a été déduite des +arguments passés en paramètres. En cas d'appel avec de mauvais types, l'erreur +n'est pas détectée à la compilation, mais à l'exécution : + +.. code-block:: console + +  $ ocaml wrong_catalog.ml +  There is no function '=' with signature (Int, Bool) + + +.. figure:: {filename}/images/package-x-generic.png +    :figclass: floatleft +    :alt: get the file +    :target: {filename}/resources/catalog.ml + +    Télécharger + +J'espère avoir été assez clair dans les explications. Le code à télécharger +reprend la totalité des exemples présentés ici. + +Pour aller plus loin, il reste à enrichir les différents types (en introduction +j'ai présenté le type `t_list` qui n'a pas été décrit, mais qui peut également +s'intégrer dans ce schéma), et gérer une plus grande arité dans les fonctions +(dans le tableur, il existe des fonctions qui ne prennent pas de paramètres, +telle `rand()` ou `true()` ou davantage que deux). + + +On pourrait également mettre en place une généricité des types (la fonction `=` +peut s'appliquer quel que soit le type de paramètres passés en arguments), mais +cela dépasse le simple catalogue que je présente ici. + diff --git a/content/images/catalog/catalog.jpg b/content/images/catalog/catalog.jpgBinary files differ new file mode 100644 index 0000000..f13a03a --- /dev/null +++ b/content/images/catalog/catalog.jpg diff --git a/content/images/catalog/catalog_75.jpg b/content/images/catalog/catalog_75.jpgBinary files differ new file mode 100644 index 0000000..b72f00a --- /dev/null +++ b/content/images/catalog/catalog_75.jpg diff --git a/content/resources/catalog.ml b/content/resources/catalog.ml new file mode 100644 index 0000000..e624315 --- /dev/null +++ b/content/resources/catalog.ml @@ -0,0 +1,196 @@ +exception TypeError
 +exception RegisteredFunction
 +
 +(*** Type definitions *)
 +
 +type _ typ =
 +  | Bool: bool typ
 +  | Int: int typ
 +
 +let t_bool= Bool
 +let t_int = Int
 +
 +(* Encode type equality *)
 +type (_,_) eq = Eq : ('a,'a) eq
 +
 +let eq_typ: type a b. a typ -> b typ -> (a, b) eq = fun a b ->
 +  begin match a, b with
 +  | Bool, Bool -> Eq
 +  | Int, Int -> Eq
 +  | _ -> raise TypeError
 +end
 +
 +let print_typ: type a. Buffer.t -> a typ -> unit = fun printer typ -> match typ with
 +  | Bool -> Printf.bprintf printer "Bool"
 +  | Int  -> Printf.bprintf printer "Int"
 +
 +(*** Values definitions *)
 +
 +type 'a value =
 +  | Bool: bool -> bool value
 +  | Int: int   -> int  value
 +
 +(** Get the value out of the box *)
 +let get_value_content: type a. a value -> a = function
 +  | Bool b -> b
 +  | Int n -> n
 +
 +(** Create a value from a known type and an unboxed value *)
 +let build_value: type a. a typ -> a -> a value = begin fun typ content ->
 +  match typ, content with
 +    | Bool, x -> Bool x
 +    | Int, x -> Int x
 +end
 +
 +(* Extract the type from a boxed value *)
 +let type_of_value: type a. a value -> a typ = function
 +  | Bool b -> Bool
 +  | Int n -> Int
 +
 +type result =
 +  | Result : 'a value -> result
 +
 +(** Create a result from a known type and a value *)
 +let inject: type a. a typ -> a -> result = fun typ res ->
 +  Result (build_value typ res)
 +
 +(** Catalog for all functions *)
 +module C = struct
 +
 +  type _ sig_typ =
 +    | T1: 'a typ -> 'a sig_typ
 +    | T2: 'a typ * 'b typ -> ('a * 'b) sig_typ
 +
 +  let eq_sig_typ: type a b. a sig_typ -> b sig_typ -> (a, b) eq = fun a b ->
 +    begin match a, b with
 +    | T1(a), T1(b) -> eq_typ a b
 +    | T2(a, b), T2(c, d) ->
 +        begin match (eq_typ a c), (eq_typ b d) with
 +          | Eq, Eq -> Eq
 +        end
 +    | _ -> raise TypeError
 +    end
 +
 +  let print_sig_typ: type a. Buffer.t -> a sig_typ -> unit = begin fun printer typ -> match typ with
 +    | T1 a -> Printf.bprintf printer "(%a)"
 +        print_typ a
 +    | T2 (a, b) -> Printf.bprintf printer "(%a, %a)"
 +        print_typ a
 +        print_typ b
 +  end
 +
 +  type t_signature =
 +    | Sig : 'a sig_typ -> t_signature
 +
 +  type t_function =
 +    | Fn1: 'a typ * 'b typ * ('a -> 'b) -> t_function
 +    | Fn2: ('a * 'b) sig_typ * 'c typ * ('a -> 'b -> 'c) -> t_function
 +
 +  module Catalog = Map.Make(
 +    struct
 +      type t = string * t_signature
 +      let compare = Pervasives.compare
 +
 +    end
 +  )
 +
 +  let (catalog:t_function Catalog.t ref) = ref Catalog.empty
 +
 +  let register name signature f = begin
 +    let name' = String.uppercase_ascii name in
 +    catalog := Catalog.add (name', signature) f !catalog
 +  end
 +
 +  let find_function name signature = begin
 +    Catalog.find (String.uppercase_ascii name, (Sig signature)) !catalog
 +  end
 +
 +  let print_error: type a. string -> a sig_typ -> unit = begin fun name signature ->
 +    let buffer = Buffer.create 16 in
 +    print_sig_typ buffer signature;
 +
 +    Printf.printf "There is no function '%s' with signature %s\n"
 +      name
 +      (Buffer.contents buffer);
 +  end
 +
 +  let eval1 name (Result p1) = begin
 +    let signature = type_of_value p1 in
 +    try
 +      begin match find_function name (T1 signature) with
 +      | Fn1 (fn_sig, returnType, f) ->
 +        (* We check the type equality between the function signature and the parameters type *)
 +        begin match eq_typ fn_sig signature with Eq ->
 +          inject returnType (f (get_value_content p1))
 +        end
 +      | _ -> raise Not_found
 +      end
 +    with Not_found ->
 +      print_error name (T1 signature);
 +      raise Not_found
 +  end
 +
 +  let eval2 name (Result p1) (Result p2) = begin
 +    let signature = T2 ((type_of_value p1), (type_of_value p2)) in
 +    try
 +      begin match find_function name signature with
 +      | Fn2 (fn_sig, returnType, f) ->
 +          (* We check the type equality between the function signature and the parameters type *)
 +          begin match eq_sig_typ signature fn_sig with Eq ->
 +            inject returnType (
 +              f (get_value_content p1) (get_value_content p2)
 +            )
 +          end
 +      | _ -> raise Not_found
 +      end
 +    with Not_found ->
 +      print_error name signature;
 +      raise Not_found
 +  end
 +
 +end
 +
 +let register1: type a b. string -> a typ -> b typ -> (a -> b) -> unit = begin
 +  fun name typ1 returnType f ->
 +    let signature = C.T1(typ1) in
 +    C.register name (C.Sig signature) (C.Fn1 (typ1, returnType, f))
 +end
 +
 +let register2: type a b c. string -> (a typ * b typ) -> c typ -> ( a -> b -> c) -> unit = begin
 +  fun name (typ1, typ2) result f ->
 +    let signature = C.T2(typ1, typ2) in
 +    C.register name (C.Sig signature) (C.Fn2 (signature, result, f))
 +end
 +
 +(* Register the standard functions *)
 +
 +let () = begin
 +
 +  register2 "="  (t_int, t_int) t_bool (=);
 +  register2 "<>" (t_int, t_int) t_bool (<>);
 +
 +  register2 "+"  (t_int, t_int) t_int (+);
 +  register2 "*"  (t_int, t_int) t_int ( * );
 +  register2 "/"  (t_int, t_int) t_int (/);
 +  register2 "-"  (t_int, t_int) t_int (-);
 +
 +  register2 "="  (t_bool, t_bool) t_bool (=);
 +  register2 "<>" (t_bool, t_bool) t_bool (<>);
 +
 +  register1 "not" t_bool           t_bool not;
 +  register2 "and"(t_bool, t_bool)  t_bool (&&);
 +  register2 "or" (t_bool, t_bool)  t_bool (||);
 +
 +
 +  let i2 = inject t_int 2
 +  and i3 = inject t_int 3
 +  and b1 = inject t_bool true in
 +  let r1 = C.eval2 "=" i2 i3 in
 +  let r2 = C.eval1 "not" r1 in
 +  let r3 = C.eval2 "=" b1 r2 in
 +  let Result value = r3 in
 +  match value with
 +  | Bool b -> Printf.printf "%b\n" b
 +  | Int  n -> Printf.printf "%d\n" n
 +
 +end
 | 
