type faible et covariance #8151

vicuna · 2003-05-19T15:31:30Z

Original bug ID: 1692
Reporter: administrator
Status: closed
Resolution: fixed
Priority: normal
Severity: minor
Category: ~DO NOT USE (was: OCaml general)

Bug description

Bonjours,

Suite a un message récent sur la mailing list, j'ai voulue trouver ce
qu'il fallait pour qu'une application partielle de kprintf donne un
type polymorphe, et je suis tombé sur une étrangeté :

    Objective Caml version 3.06+31 (2003-05-02)

type (-'a, 'b, 'c, 'd) my_format;;

type (-'a, 'b, 'c, 'd) my_format

let from_my (x: ('a, 'b, 'c, 'd) my_format) =

(Obj.magic x :('a, 'b, 'c, 'd)format);;

val from_my : ('a, 'b, 'c, 'd) my_format -> ('a, 'b, 'c, 'd) format =

let to_my (x :('a, 'b, 'c, 'd)format) =

(Obj.magic x:('a, 'b, 'c, 'd) my_format);;

val to_my : ('a, 'b, 'c, 'd) format -> ('a, 'b, 'c, 'd) my_format =

let mykprintf k fo = Printf.kprintf k (from_my fo);;

val mykprintf : (string -> 'a) -> ('b, unit, string, 'a) my_format -> 'b =

let m = mykprintf (fun s -> prerr_endline s);;

val m : ('_a, unit, string, unit) my_format -> '_a =

type 'a t = ('a, unit, string, unit) my_format -> 'a;;

type 'a t = ('a, unit, string, unit) my_format -> 'a

let (m: 'a t) = mykprintf (fun s -> prerr_endline s);;

val m : 'a t =

On voit que l'application partielle de mykrintf donne un type
polymorphique faible alors que si on la type explicitement, à l'aide
d'un type nommé, cela devient un type polymorphique complet.

Il semble donc que l'algorithme utilisé pour détecter la covariance ne
soit pas le même pour décider de la distinction typage fort/typage
faible dans le cas d'une application partielle que dans le cas d'une
définition du type.

Ps: mon message n'implique en aucun cas que je pense que format
devrais être contravariant en son premier argument. J'en sais rien,
c'était juste un test

--
Rémi Vanicat
vanicat@labri.u-bordeaux.fr
http://dept-info.labri.u-bordeaux.fr/~vanicat

The text was updated successfully, but these errors were encountered:

vicuna · 2003-05-20T07:56:39Z

Comment author: administrator

From: vanicat@labri.u-bordeaux.fr

Suite a un message recent sur la mailing list, j'ai voulue trouver ce
qu'il fallait pour qu'une application partielle de kprintf donne un
type polymorphe, et je suis tombe sur une etrangete' :
    Objective Caml version 3.06+31 (2003-05-02)
type (-'a, 'b, 'c, 'd) my_format;;

type (-'a, 'b, 'c, 'd) my_format
[...]
val mykprintf : (string -> 'a) -> ('b, unit, string, 'a) my_format -> 'b =

let m = mykprintf (fun s -> prerr_endline s);;

val m : ('_a, unit, string, unit) my_format -> '_a =

type 'a t = ('a, unit, string, unit) my_format -> 'a;;

type 'a t = ('a, unit, string, unit) my_format -> 'a

let (m: 'a t) = mykprintf (fun s -> prerr_endline s);;

val m : 'a t =

On voit que l'application partielle de mykrintf donne un type
polymorphique faible alors que si on la type explicitement, a` l'aide
d'un type nomme', cela devient un type polymorphique complet.

Ce comportement est effectivement decrit dans le papier sur le
polymorphisme "relaxe'" disponible sur ma page.
Pour preserver la principalite' de l'inference on est amene' a`
prendre une definition restrictive de la covariance, interdisant le
passage par une branche contravariante. Donc le premier cas n'est pas
generalisable. Dans le second cas le constructeur de type masque la
branche contravariante et 'a devient generalisable.
Probleme cependant: dans le cas d'une abbreviation, ce n'est
probablement pas principal (l'exemple du papier utilise un type
somme). Je m'etais promis d'etudier la question...

Ps: mon message n'implique en aucun cas que je pense que format
devrais etre contravariant en son premier argument. J'en sais rien,
c'etait juste un test

La variance des parametres de format reste pour moi un grand
mystere...

Jacques

vicuna · 2003-05-21T09:18:44Z

Comment author: administrator

Fixed by JG (2003-05-21)

vicuna · 2003-05-21T16:16:50Z

Comment author: administrator

From: vanicat@labri.u-bordeaux.fr

Suite a un message recent sur la mailing list, j'ai voulue trouver ce
qu'il fallait pour qu'une application partielle de kprintf donne un
type polymorphe, et je suis tombe sur une etrangete' :

Ce comportement etant incorrect dans le cas d'une abbreviation (il est
correct pour un type construit ou abstrait), j'ai ajoute' un
information de variance faible pour les abbreviations.
L'exemple que tu decris n'est plus accepte'.

      Jacques

vicuna closed this as completed May 21, 2003

vicuna added the bug label Mar 19, 2019

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

type faible et covariance #8151

type faible et covariance #8151

vicuna commented May 19, 2003

vicuna commented May 20, 2003

type (-'a, 'b, 'c, 'd) my_format;;

let m = mykprintf (fun s -> prerr_endline s);;

type 'a t = ('a, unit, string, unit) my_format -> 'a;;

let (m: 'a t) = mykprintf (fun s -> prerr_endline s);;

vicuna commented May 21, 2003

vicuna commented May 21, 2003

type faible et covariance #8151

type faible et covariance #8151

Comments

vicuna commented May 19, 2003

Bug description

type (-'a, 'b, 'c, 'd) my_format;;

let from_my (x: ('a, 'b, 'c, 'd) my_format) =

let to_my (x :('a, 'b, 'c, 'd)format) =

let mykprintf k fo = Printf.kprintf k (from_my fo);;

let m = mykprintf (fun s -> prerr_endline s);;

type 'a t = ('a, unit, string, unit) my_format -> 'a;;

let (m: 'a t) = mykprintf (fun s -> prerr_endline s);;

vicuna commented May 20, 2003

type (-'a, 'b, 'c, 'd) my_format;;

let m = mykprintf (fun s -> prerr_endline s);;

type 'a t = ('a, unit, string, unit) my_format -> 'a;;

let (m: 'a t) = mykprintf (fun s -> prerr_endline s);;

vicuna commented May 21, 2003

vicuna commented May 21, 2003