💾 Archived View for heyplzlookat.me › articles › gadt-mehari.gmi captured on 2024-05-26 at 14:40:50. Gemini links have been rewritten to link to archived content
⬅️ Previous capture (2024-03-21)
-=-=-=-=-=-=-
En travaillant sur Mehari, notre bibliothèque implémentant le protocole Gemini côté serveur, j’ai été confronté à un problème lorsque j’ai dû réfléchir à comment représenter le status d’une réponse. En effet, il est possible de joindre ou non un _body_ à la réponse en fonction de son status. De manière générale, le message complémentaire présent dans le _header_ (le champ « META ») dépend du status de la réponse. Ainsi, en cas de succès, le _header_ doit contenir le type MIME associé au body joint ; en cas de timeout, le nombre de secondes restantes avant une nouvelle requête ; en cas d’erreur, un message informatif, etc.
J’ai donc d’abord procédé de la manière la plus naturelle, un simple type algébrique :
module Response = struct
type status =
| Input of string
| SensitiveInput of string
| Success of Mime.t * Body.t
| …
| SlowDown of int
| …
let status_of_code meta = function
| 10 -> Input meta
| 11 -> SensitiveInput meta
| …
| 44 -> SlowDown (Int.to_string meta)
| …
let int_of_code = function
| Input _ -> 10
| SensitiveInput _ -> 11
| …
let respond status =
let code = int_of_code status in
let meta, body =
match status with
| Success (m, b) -> (Mime.to_string m, Some b)
| SlowDown n -> (Int.to_string n, None)
| Input msg | SensitiveInput msg | … msg -> (msg, None)
in
let body = Option.fold body ~none:"" ~some:Body.to_string in
Printf.sprintf "%i %s\r\n%s" code meta body
end
Le type `status` possède donc 18 constructeurs représentant chacun des status décris dans la spécification (une implémentation rudimentaire peut cependant se contenter d’en fournir seulement 5 fondamentaux pour des questions de simplicité). De ce fait, il est assez laborieux de récupérer leur contenu dans un motif et je suis alors contraint de faire une longue branche « OU » dans mon _match_.
J’ai donc finalement opté pour une solution faisant appel aux GADTS en réfléchissant à simplifier tout cela :
module Response = struct
type 'a status = int * 'a typ
and _ typ =
| Success : Body.t -> Mime.t typ
| SlowDown : int -> string typ
| Meta : string typ
let respond (type a) ((code, status) : a status) (meta : a) =
let meta, body =
match status with
| Success body -> (Mime.to_string meta, Some body)
| SlowDown n -> (Int.to_string n, None)
| Meta -> (meta, None)
in
let body = Option.fold body ~none:"" ~some:Body.to_string in
Printf.sprintf "%i %s\r\n%s" code meta body
end
module Status = struct
let input = (10, Meta)
let sensitive_input = (11, Meta)
let success body = (20, Success body)
…
let slow_down n = (44, SlowDown n)
…
end
Ici, j’ai transformé le type `status` en un couple composé d’un entier correspondant au code associé et d’un GADT qui contient des informations plus détaillées. J’ai aussi regroupé tous les constructeurs nécessitant un `string` en argument en un seul : `Meta`.
Grâce à ce changement de représentation, j’obtiens une fonction `respond` dont le type est un peu plus complexe. En effet, le type du paramètre `meta` varie en fonction du type qui habite `status`. Je peux ainsi l’utiliser comme ceci :
let _ = Mehari.(respond input "Enter your message") let _ = Mehari.(respond slow_down 4) let _ = Mehari.(respond not_found "Not found!")
En contrepartie, je dois faire une croix sur la fonction `status_of_code` de la précédente implémentation. Effectivement, il est impossible d’écrire une fonction avec le type `int -> 'a status` qui fait varier le type habitant de `status` (`'a`) en fonction d'une valeur entière. Il faudrait pour cela un système de type dépendant, ce qui n’est pas le cas d’OCaml.
Les GADTs sont donc utiles lorsque l’on veut donner des informations de types plus détaillées au compilateur. Il ne faut cependant pas pour autant tomber dans le piège de la complexification et vouloir les utiliser dans des cas qui n’en nécessite pas. À vrai dire, j’étais assez content d’avoir trouvé un cas d’usage au GADT étant très friand d’article qui les présentent comme une solution miracle à tous les problèmes de type complexe. Voulant reproduire (en moindre mesure) ce que des membres de la communauté avaient déjà écrit :
https://blog.mads-hartmann.com/ocaml/2015/01/05/gadt-ocaml.html
https://blog.osau.re/articles/gadt_and_state_machine.html
https://blog.janestreet.com/why-gadts-matter-for-performance/
https://github.com/ocsigen/lwt/blob/master/src/core/lwt.ml#L392
(Malheureusement plus disponnible :( )
Pas encore de commentaires