octachron a écrit 36 commentaires

Au niveau du système de module, des annotations de types sont nécessaires pour les arguments des foncteurs:

module F(X:sig type t end (* ← ceci est une annotation de type *)) = 
struct include X end (* mais le type (i.e. la signature) de retour est inferré *)

Les modules récursifs eux ont besoin d'être totalement annoté, par exemple:

module rec M : (* ↓ annotation du type de M *)
sig
  type t = A of S.t  
  val compare: t -> t -> int
end = struct
  let compare = compare
  type t = A of S.t
end
and S : (Set.S with type elt = M.t) (* ← annotation du type de S *) 
= Set.Make(M);;

Ce besoin d'annotation pour les modules peut se propager dans les fonctions à cause
des modules locaux (ou de première classe).

let dedup (type a (* ←soit un type a abstrait*) ) l = 
  (* ici on a besoin d'introduire un type a pour le module S définit ci-dessous *)
  let module S = Set.Make(struct type t = a let compare = compare end) in
  S.elements @@ S.of_list l

Un autre cas classique d'annotation explicite apparaît pour la récursion polymorphique
sur les types récursifs non homogènes:

type 'a arbre_complet = Feuille of 'a | Noeud of ('a * 'a) arbre_complet
let rec hauteur: 'a.(*← ∀a *) 'a arbre_complet -> int = function
  | Feuille _ -> 0
  | Noeud a ->
  (* dans cette branche, hauteur est appliqué à ('a * 'a) arbre_complet *) 
    1 + hauteur a

Dans ce cas, l'annotation 'a.'a arbre_complet -> int qui équivaut à forall 'a.…
est nécessaire car le type du paramètre 'a à l'intérieur de la définition de hauteur et à l'extérieur diffère.

Pour le polymorphisme de second ordre, OCaml ne supporte pas directement les annotations forall à l'intérieur des arguments de fonctions, il faut donc passer soit par des types enregistrements(records):

type id = { f:'a. 'a -> 'a }

ce qui est plus contraignant qu'une annotation directe, soit par le système objet

let pair (id: <f:'a.'a -> 'a>) = id#f 1, id#f []

Sans cette annotation le typeur va essayer d'unifier le type de 1 et [] et renvoyer une erreur.

Les GADTs de leur côté sont toujours lourds en annotations en Haskell ou OCaml

   type 'a monoid =
  | R: float monoid
  | N: int monoid  
  | Pair: 'a monoid * 'b monoid -> ('a * 'b) monoid

  let rec zero: type a. (*← ∀a, a abstrait *) a monoid -> a = function
    | R -> 0. (* ← dans cette branche, a = float *)
    | N -> 0  (* ← a = int *)
    | Pair (a,b) -> zero a, zero b (* a = b * c *)

Enfin, une particularité d'OCaml du aux effets de bords, ce sont les types faiblement polymorphiques, qui ne peuvent pas être exporté par une unité de compilation, ce qui peut nécessiter d'ajouter des annotations de type pour les éliminer. Par exemple, un fichier a.ml

  let x: int list ref = ref []

ne compile pas sans son annotation de type.

C'était pas pour critiquer Haskell, c'était juste pour pour souligner cette différence entre Haskell et OCaml.

Ce n'est pas vraiment une différence entre OCaml et Haskell, en OCaml aussi les usages avancés du système de type requièrent des annotations de type explicite: que ce soit au niveau des modules et foncteurs, des types algébriques généralisés, du polymorphisme de second ordre, ou de la récursion polymorphique.

Il est peut être plus courant de se heurter à ces problèmes en Haskell, mais le problème sous-jacent reste le même: au-delà d'un certain niveau d'expressivité du système de type, l'inférence devient indécidable, et le compilateur a besoin que le programmeur explicite son intention.

juste des gens sensibilisés au design

Et s'ils ne sont pas sensibilisés, on veut juste qu'ils apportent des critiques valables et argumentées

Mais évaluer son niveau d'incompétence dans un domaine est une des choses les plus difficiles à faire, quel que soit le domaine.

Sur un projet qui manque de direction en terme de design, je m'attend justement à ce que la capacité à jauger de la qualité d'un design et prendre des décisions à ce niveau soit tout aussi manquante ou embryonnaire.

Bref, on ne veut pas de traitement de faveur, on veut juste être traité comme les autres contributeurs : que les contributions soient jugées, acceptées ou refusées par des gens au même niveau au moins que ceux qui les soumettent.

Mais dans un projet qui manque de designers, c'est par définition une requête impossible à satisfaire. Exigez de n'être jugé que par d'autres designers pour une contribution à un projet qui n'a pas de designer ; ce n'est même pas un mauvais argument d'autorité, c'est un plan de communication absolument désastreux.

L'intérêt que je vois au type fantôme, c'est qu'ils permettent de rafiner un type de base, en rajoutant potentiellement de l'information connue à la compilation, et ensuite de définir des jeux de fonctions qui utilisent −optionnellement− cette information supplémentaire, le tout en gardant explicite qu'il s'agit du même type de base.

Par exemple, on pourrait imaginer un type liste augmenté d'une information sur le fait qu'elle soit triée ou non

type triee = private Sorted
type non_triee = private Unsorted

type ('a,'sorted_or_not) liste = 'a list

À partir de là, je peux raffiner les fonctions sur les listes pour rajouter de l'information:

 val sort: ('a,'triee_ou_pas) liste -> ('a,triee) liste
(** triée une liste la rend triée *)

 val rev: ('a,'tree_ou_pas) liste -> ('a, non_triee) liste
(** renversée une liste triée ou non, donne une liste non triée *)

Cela permet aussi de définir des fonctions qui requiert en entrée des listes triées, ce que le type fantôme permet de garantir

val affiche_triee:(int,triee) liste -> unit

Mais la grande différence par rapport à avoir deux types abstraits, c'est qu'il est beaucoup plus simple de partager les fonctions entre les différents sous-types dans les cas où ces fonctions n'ont pas besoin de l'information supplémentaire:

val iter: ('a -> unit) -> ('a, 'triee_ou_pas ) liste -> unit

Un autre point sur lesquels des types fantômes peuvent être intéressant, ce sont les bindings avec des bibliothèques extérieures en C. Les types fantômes peuvent permettre d'introduire un typage correct sans trop s'éloigner de la représentation en C. Par exemple, j'avais utilités dans un prototype de bindings OpenGL des types fantômes pour typer les enums et handles opengl, qui sont tous des entiers dans la représentation C. Ce qui permet de transformer

val bindBuffer :  int -> int -> unit

en

type 'a gl_enum = private int
type 'a handle = private int
val bindBuffer :  [>`BufferType] gl_enum -> [`Buffer] handle -> unit

et de s'assurer que système de type d'OCaml vérifiera à notre place que seulement des identifiants valides seront passés à l'API OpenGL; tout en pouvant facilement repasser à des entiers non typés au besoin.

Pour ce cas, ça doit pouvoir se faire avec des GADT

Cela dépend beaucoup ce que tu entends par "ce cas" et pouvoir se faire:
il est possible d'encoder les entiers naturels dans le système de type d'OCaml, avec des GADTs ou des types fantômes; cependant la complexité de l'encodage a tendance à s'accroître rapidement avec l'expressivité dudit encodage.

Par exemple, l'encodage le plus simple

  type z = private Z
  type 'a succ = private Succ
  type 'nat t = Z: z t | S: 'nat t -> 'nat succ t

fonctionne mais à plusieurs limitations majeures:

• la taille du type augmente linéairement avec l'entier, ce qui peut créer des problèmes pour le compilateur assez rapidement ( il avait tendance à planter vers 65000 lors de mes derniers tests? )

• les opérations que l'on peut effectuer sont très limitées.

Mais il peut être suffisant pour encoder un certain nombre d'invariants en algèbre linéaire (par exemple, on peut vérifier que les dimensions des matrices dans le produit matriciel soient correctes). Par contre, si je souhaite concaténer deux vecteurs, j'aurai
besoin d'encoder l'addition d'entier dans mon type 'nat1 t -> 'nat2 t -> ('nat1 + 'nat2) t?

Cependant, avec cet encodage, le système de type n'a pas assez d'information pour construire le type 'nat1 + 'nat2, il faut soit passer par des types auxiliaires, ou modifier l'encodage des entiers. Un exemple qui marche est d'encoder des propositions
de la forme a + b = c:

  type 'nat t = 
  | Z: ('a*'a) t (* 'a + z = 'a*) 
  | S: ('z,'a) t -> ('z,'a succ) t (* si 'n + a = b alors 'n + succ a = succ b *)

À partir de cet encodage, on peut écrire l'addition

  let add: type inf mid sup: (inf * mid) nat -> (mid * sup) nat -> (inf * sup) nat =
  fun a b -> match b with
  | Z -> a
  | S n -> S (add a n)

Cependant, le paramètre de type libre 'a a tendance à créer des problèmes du au fait que le GADT n'est pas covariant, donc la relaxed value restriction ne s'applique plus et
il est très (trop) facile de se retrouver avec des types faibles.

Et la complexité ne fait qu'empirer si on essaie d'implémenter d'autres fonctionnalités (représentation binaire, multiplication, comparaison, etc …) sur les entiers dans le système de types.

Un bon exemple de ce qui peut être fait raisonnablement dans le cadre de l'algèbre linéaire est SLAP.

Un exemple pédagogique pour montrer à quel point le budget de complexité peut exploser facilement serait ma bibliothèque expérimentale tensority.

Utiliser des types fantômes peut fonctionner, il faut faire cependant attention à quelles égalités de types on rend visible.

Effectivement, si on exporte l'égalité complète

type 'a t = int * int

il est possible de jongler entre les différentes valeurs du paramètre fantôme.

let x: int t = 0,1
let y : float t = x

Mais c'est du au fait que le système de type se rappelle qu'au final 'a t ≡ int * int.
Pour éviter ce problème, on peut cacher cette égalité de type, soit partiellement

module P: sig 
  type 'a t = private (int*int)
  val create: int * int -> 'a t 
end = struct
  type 'a t = int * int
  let create x = x
end

soit complètement

module A: sig
  type 'a t
  val create: int * int -> 'a t
  val extract: 'a t -> int * int
end = struct 
  type 'a t = int * int 
  let create x = x 
  let extract x = x
end

Dans les deux cas, l'égalité de type n'est plus visible, et

let x : int P.t = P.create (0,1)
let y : float P.t = x

est rejetée comme invalide.

Faire une traduction en anglais pourrait être intéressant. Mais une bonne partie du contenu existe déjà en version anglaise ; de manière plus dispersée il est vrai. Peut-être qu'un bon compromis serait de traduire le contenu non publié par ailleurs (ou uniquement dans le manuel) : par exemple, la section sur les GADTs, celle sur les attributs et nœud d'extension prédéfinis, ou la longue liste des améliorations mineures.

Je n'ai été jamais complètement convaincu par la notation do comparé à utiliser directement >>= et >>.
La notation do est certainement plus élégante, mais bien moins explicite. Pour en revenir à OCaml, il faut tout de même noter qu'il est parfaitement possible d'utiliser >>= plutôt que bind. De même, il existe de nombreuses extensions de syntaxe qui permettent d'utiliser la notation do en OCaml; j'en compte au moins 4 disponibles directement avec opam.

Un standard supporté par les navigateurs? Dans mon souvenir, le support de MathML a été abandonné dans Chrome et n'est toujours pas planifié pour Internet Explorer.

Pour m'être brièvement intéressé à la question de l'analyse grammaticale, l'analyse syntaxique de langue naturelle est beaucoup plus compliquée que celle pratiquée dans les compilateurs: la plupart des grammaires des langues naturelles sont des grammaires contextuelles fort propices aux ambiguïtés. Pour le peu que je comprend le sujet, il semble exister une recherche fort active sur cette question autour des grammaires d'arbres adjoints et le développement de méta-grammaires pour générer automatiquement des grammaires à partir d'un corpus de texte.

Par contre, les applications pratiques de ces modèles pour faire de la correction grammaticale semblent manquer. Il est d'ailleurs un peu déconcertant de voir grammalecte utiliser des simples expressions régulières pour faire de l'analyse grammaticale. Enfin, le pragmatisme a ses vertus.