Comment limiter un paramètre à une seule variante d'un type de variante

Question

Supposons que j'aie deux types, Vector2D et Vector3D et qu'ils soient étiquetés (c'est le terme correct, non ?), et je veux écrire une fonction qui opère UNIQUEMENT sur Vector2D (ou est-ce que vector(two) est plus correct ici ?), comme ceci :

type two;
type three;
type vector('a) = 
  | Vector2D(float, float): vector(two)
  | Vector3D(float, float, float): vector(three);

let first = (a: vector(two)) => {
  switch(a) {
    | (x, y) => x +. y
  }
}

let second = (Vector2D(x, y)) => {
  x +. y
}

let third = ((x, y): vector(two)) => {
  x +.y
}

Les fonctions first et second interdisent de passer un Vector3D, comme je le souhaite, mais elles soulèvent un avertissement "Ce pattern matching n'est pas exhaustif".

Pour first, j'aimerais savoir pourquoi ce n'est pas exhaustif, n'ai-je pas limité les options possibles à Vector2D ici ? Pour second, je suppose que la raison est la même que pour first, mais comment serait-il même possible de résoudre le problème avec cette syntaxe ?

Quant à third, celui-ci ne compile pas parce que "Ce pattern correspond à ('a, 'b) mais vector(two) était attendu". Pourquoi le compilateur s'attend-il à un tuple ici ? N'est-il pas possible d'utiliser la destructuration dans les paramètres de fonction ?

ÉDIT :
Il s'avère qu'il y a un problème encore plus simple pour démontrer ce que je veux

type state = Solid | Liquid
let splash = (object) => {
  switch(object) {
    | Liquid => "bruits d'éclaboussures. Je suppose."
    | Solid => "" // cela ne devrait même pas être possible dans le contexte de cette fonction, et je veux que le compilateur l'applique
}

Answer 1

Concerning the GADT part, the issue here is that you are using bucklescript and its ancient 4.02.3 compiler version. For instance, the following code works perfectly fine in OCaml 4.03 :

type two = Two ; 
type three = Three ;
/* Never define abstract types when you want to use them as type level tags, your code will only works inside the module defining them, and then fail due to injectivity problems. */

type vector('a) = 
  | Vector2D(float, float): vector(two)
  | Vector3D(float, float, float): vector(three);

let sum_2 = (Vector2D(x,y)) => x +. y
let sum_3 = (Vector3D(x,y,z)) => x +. y +. z 
let sum_any = (type a, x: vector(a) ) => switch (x) {
  | Vector2D(x,y) => x +. y;
  | Vector3D(x,y,z) => x +. y +. z
}

Mais ça échouera sur la version 4.02.3 avec un avertissement d'exhaustivité (qui devrait être traité comme une erreur), car la vérification de l'exhaustivité pour les GADT avec des clauses de réfutation n'a été ajoutée qu'en 4.03.

Answer 2

Vous pouvez accomplir ce que vous voulez en utilisant les variantes polymorphes :

type vector = [
  | `Vector2D(float, float)
  | `Vector3D(float, float, float)
];

let first = (a: [`Vector2D(float, float)]) => {
  switch(a) {
    | `Vector2D(x, y) => x +. y
  }
}

let second = (`Vector2D(x, y)) => {
  x +. y
}

Cela vous donnera une erreur de type si vous essayez de passer un `Vector3D à l'une ou l'autre de ces fonctions :

               ^^^^^^^^^^^^^^^^^^^^^
Error: This expression has type [> `Vector3d(float, float, float) ]
       but an expression was expected of type [< `Vector2D(float, float) ]
       The second variant type does not allow tag(s) `Vector3d

Notez d'abord que Vector2D et Vector3D dans votre exemple ne sont pas des types. Ce sont des constructeurs qui construisent des valeurs du type vector('a). Ils sont parfois aussi appelés "tags", comme vous l'avez souligné, et le type est parfois appelé un "union taguée" au lieu de "variante" parce que les valeurs contiennent un tag qui spécifie quel constructeur a été utilisé pour la construire. Le tag est ce qui est vérifié lorsque vous faites une correspondance de motifs en utilisant un motif de constructeur.

Ce que vous utilisez dans votre exemple n'est pas une variante ordinaire, mais un Type de Données Algébriques Généralisées (GADT) (qui aurait peut-être été plus justement nommé "Variante Généralisée" en OCaml/Reason), et la raison pour laquelle cela ne fonctionne pas est que, bien qu'un GADT vous permette d'attribuer un type spécifique à un constructeur, cela ne fonctionne pas dans l'autre sens. Vous pouvez avoir plusieurs constructeurs qui spécifient vector(two) par exemple. (Edit : Cela semble être incorrect, voir la réponse de @octachron)

Aucune des fonctions first ou third dans votre exemple ne compile, Le compilateur attend un tuple car vous utilisez un motif de tuple au lieu d'un motif de constructeur. (x, y) n'est pas la même chose que Vector2D(x, y). Sinon, vous ne pourriez pas différencier Vector2D(float, float) de Line(point, point), par exemple, qui contient des données d'un type entièrement différent.