Petite question sur les types.

[carlesup3]

Bonjour,
Qu'est-ce qu'un type forcé en Caml?
Cordialement

[Ptival]

Bonjour,

Où as-tu lu ça ? Dans quel contexte ?

Le terme ne m'évoque pas quelque chose en particulier.

On peut parler de forcer le type d'un terme quand on écrit une signature de type pour essayer de forcer le polymorphisme ou le monomorphisme.

On peut parler de forcer une valeur paresseuse, auquel cas le type forcé serait le type normal, non-paresseux.

Mais peut-être qu'il y a un autre usage de l'adjectif forcé qui m'échappe.

[jurik42]

Voici un exemple simple pour comprendre facilement :

Code :

1
2
3
4
# [];; (* liste polymorphique *)
- : 'a list = []
# ([] : int list);;
- : int list = [] (* liste monomorphique (typage forcé) *)

[gasche]

On peut ajouter des annotations à un terme pour obtenir un type moins général qu'il ne serait inféré sinon. Mais quelle est ta question, au juste ?

[Cacophrene]

Bonsoir,

Et une question subsidiaire : si, éventuellement, tu souhaites réduire le niveau de généralité du typage d'un code OCaml, c'est que tu dois avoir de bonnes raisons de le faire. Je dis ça parce que, de façon générale, on essaie justement de gagner en généralité pour factoriser le code.

Cordialement,
Cacophrène

[jurik42]

Envoyé par Cacophrene

Et une question subsidiaire : si, éventuellement, tu souhaites réduire le niveau de généralité du typage d'un code OCaml, c'est que tu dois avoir de bonnes raisons de le faire. Je dis ça parce que, de façon générale, on essaie justement de gagner en généralité pour factoriser le code.

Personnellement, je vois deux raisons :
- utiliser des types "abréviations". Par exemple :

Code :

1
2
type t = int list
let empty = ([] : t)

Notamment à l'intérieur des foncteurs ou des objets, on veut un type abstrait (non affecté ans le *.mli) que l'on nomme 't'. On veut également que toutes les opérations qui utilisent ce type opèrent bien sur ce type 't', et non, pour reprendre mon exemple précédent, le type 'int list'.

- garantir des données valides, sur un module en amont

En effet, si on souhaite écrire un module contenant des fonctions qui opèrent sur des éléments donnés par un code en aval, on souhait avoir la garantie d'une bon typage.
Ce cas de figure est arrivé lorsque je voulais faire un module qui appelait deux autres modules : ces modules étaient écrits par des candidats qui implémentaient une IA à travers des fonctions appelées depuis mon module, qui s'occupe d'héberger la partie et de faire confronter les deux IA.

Bien sûr, l'intérêt du typage forcé ne s'arrête pas là, mais sont exposés ci-dessus les deux cas qui m'arrivent personnellement le plus souvent

[gasche]

En général on fait plutôt ces vérifications-là au niveau de l'interface du module (le fichier .mli ou la signature d'un sous-module), plutôt qu'en utilisant des annotations dans les termes.

[SpiceGuid]

Comme Cacophrène, j'essaie de gagner en généralité pour factoriser le code.
Comme gasche, je préfère placer les restrictions de type au niveau de l'interface du module.
Comme Ptival et gasche j'annote une variable/expression à l'aide d'un type ou bien je fourni un type explicite. Je force un type (transtypage) quand je programme dans un langage à typage laxiste.

Malgré toutes ces précautions, dans le top-level, il peut rester encore deux cas où le typage doit être explicite.

Cas n°1: OCaml ne voit pas une certaine propriété "évidente"

OCaml ne voit pas que cmp est un ordre total sur 'a :

Code OCaml :

1
2
3
4
5
6
7
8
9
let rec lexicographical (cmp:'a -> 'a -> int) l1 l2 =
  match l1,l2 with
  | [],[] -> 0
  | [],_ -> -1
  | _,[] ->  1
  | h1::t1,h2::t2 ->
      let c = cmp h1 h2 in
      if c = 0 then lexicographical cmp t1 t2
      else c

Cas n°2: les nested-datypes et autre récursion polymorphe

Ce qu'il ne faut pas faire :

Code OCaml :

1
2
3
let rec f : 'a.'a -> 'a = fun x -> x 
and g y = f 3

Ce qu'il faut faire :

Code OCaml :

1
2
3
let f = fun x -> x 
and g y = f 3

D'ailleurs voilà pourquoi il y a un mot clé rec : parce qu'il ne faut pas en abuser.

[gasche]

Je ne comprends pas le cas 1. On gagne en flexibilité en laissant "lexicographical" utiliser deux types différents, d'ailleurs on utilise dans certaines situations un ordre lexicographique comme un produit de deux ordres différents.

Enfin, ça permet de repérer des bugs. Si tu avais écrit (cmp h1 h1) par erreur, tu aurais repéré un typage plus restreint qu'attendu.