Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Variants recursifs et sous-typage #3147

Closed
vicuna opened this issue Jan 11, 2002 · 4 comments
Closed

Variants recursifs et sous-typage #3147

vicuna opened this issue Jan 11, 2002 · 4 comments
Labels

Comments

@vicuna
Copy link

vicuna commented Jan 11, 2002

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

Bug description

Je ne sais pas si c'est un bug ou si j'ai raté quelque chose:

type nat = [ Z | S of nat ]
type zero = [ Z ] type one = [ S of zero ]

let f (x : one) = (x :> nat)

donne:

This expression cannot be coerced to type nat = [ Z | S of nat];
it has type one = [ S of zero] but is here used with type [< nat] = [< S of nat]
Type zero = [ Z] is not compatible with type nat = [ Z | `S of nat]

Alors que:

let f (x : [< one ]) = (x :> nat)

est accepté.

Est-ce normal ?

Là aussi, je ne comprends pas:

let f (x : [ S of [< Z] ]) =
(x :> ([< Z | S of 'a ] as 'a))

donne
This expression cannot be coerced to type [< S of 'a] as 'a; it has type [ S of [< `Z]]
but is here used with type 'a

(d'où sort ce type ([< `S of 'a] as 'a) ?)

--
Alain

@vicuna
Copy link
Author

vicuna commented Feb 13, 2002

Comment author: administrator

Je ne sais pas si c'est un bug ou si j'ai raté quelque chose:

type nat = [ Z | S of nat ]
type zero = [ Z ] type one = [ S of zero ]

let f (x : one) = (x :> nat)

Les coercions simples ne marchent que dans les cas simples :-)
Pour les variants polymorphes, le type n'est pas ouvert de facon recursive.
(Le bon choix depend du contexte, donc on prend l'option la plus simple)

let f x = (x :> nat);;

val f : [< nat] -> nat =

Sachant que [< nat] = [< Z | S of nat], il est simple de voir que ta
definition force a` unifier nat et zero, ce qui est bien sur impossible.

La bonne solution est

let f x = (x : one :> nat);;

val f : one -> nat =

Là aussi, je ne comprends pas:

let f (x : [ S of [< Z] ]) =
(x :> ([< Z | S of 'a ] as 'a))

donne
This expression cannot be coerced to type [< S of 'a] as 'a; it has type [ S of [< `Z]]
but is here used with type 'a

(d'où sort ce type ([< `S of 'a] as 'a) ?)

Quand tu unifie le premier type au second, tu commence par eliminer le cas Z, creant un type [< S of 'a] as 'a. Il ne peut evidemment pas etre unifie' a[<Z], puisque depuis 3.02 le type vide [< ] est illegal.

Jacques

@vicuna vicuna closed this as completed Feb 13, 2002
@vicuna
Copy link
Author

vicuna commented Feb 13, 2002

Comment author: administrator

On Wed, 13 Feb 2002, Jacques Garrigue wrote:

let f (x : one) = (x :> nat)

Les coercions simples ne marchent que dans les cas simples :-)
...
La bonne solution est

let f x = (x : one :> nat);;

val f : one -> nat =

Ah ok, je pensais que si le contexte donnait un type "( x : one )",
on pouvait toujours s'en passer dans la coercion. Il faudra que je relise
Ctype.build_subtype ... c'est bien là que ça se passe ? Dans typecore.ml,
ne serait-il pas possible d'utiliser Ctype.subtype lorsque l'unification
échoue avec le type renvoyé par Ctype.enlarge ?

let f (x : [ S of [< Z] ]) =
(x :> ([< Z | S of 'a ] as 'a))

donne
This expression cannot be coerced to type [< S of 'a] as 'a; it has type [ S of [< `Z]]
but is here used with type 'a

(d'où sort ce type ([< `S of 'a] as 'a) ?)

Quand tu unifie le premier type au second, tu commence par eliminer le cas Z, creant un type [< S of 'a] as 'a.

C'est cela que je ne comprends pas. Éliminer Z dans [< Z | S of 'a ] as 'a, j'aurais dit que ça donnait [ S of ([< Z | S of 'a ] as 'a)].

Alain

@vicuna
Copy link
Author

vicuna commented Feb 13, 2002

Comment author: administrator

From: frisch@clipper.ens.fr

On Wed, 13 Feb 2002, Jacques Garrigue wrote:

let f (x : one) = (x :> nat)

Les coercions simples ne marchent que dans les cas simples :-)
...
La bonne solution est

let f x = (x : one :> nat);;

val f : one -> nat =

Ah ok, je pensais que si le contexte donnait un type "( x : one )",
on pouvait toujours s'en passer dans la coercion. Il faudra que je relise
Ctype.build_subtype ... c'est bien là que ça se passe ? Dans typecore.ml,
ne serait-il pas possible d'utiliser Ctype.subtype lorsque l'unification
échoue avec le type renvoyé par Ctype.enlarge ?

Euh... Ca supposerait qu'on sache defaire l'unification, ce qu'on ne
fait pas actuellement: apres un echec, il faut imperativement renvoyer
une erreur.

Plus important: ca n'est bien sur pas principal. Il faudrait savoir
d'ou vient l'information qu'on utilise pour Ctype.subtype. Le seul cas ou on pourrait faire ca sans risque est quand le type
infere' est generique et ne contient pas de variables. Alors on est
sur que Ctype.subtype sera toujours meilleur que Ctype.enlarge.
Mais ca manque un peu de generalite'.

let f (x : [ S of [< Z] ]) =
(x :> ([< Z | S of 'a ] as 'a))

donne
This expression cannot be coerced to type [< S of 'a] as 'a; it has type [ S of [< `Z]]
but is here used with type 'a

(d'où sort ce type ([< `S of 'a] as 'a) ?)

Quand tu unifie le premier type au second, tu commence par eliminer le cas Z, creant un type [< S of 'a] as 'a.

C'est cela que je ne comprends pas. Éliminer Z dans [< Z | S of 'a ] as 'a, j'aurais dit que ça donnait [ S of ([< Z | S of 'a ] as 'a)].

Je vois ton probleme: (x :> [< ... ]) est equivalent a (x : [< ... ]). En effet, il n'existe pas de sous-type propre d'un type polymorphe ouvert vers le bas (cad, qui peut perdre des cas). Quand on calcule le sous-type d'un variant polymorphe, on se base sur l'instance qui a le moins de cas (si elle n'est pas le variant vide, comme dans ton cas). Donc (x :> [> ...]) donne a x le meme type que
(x :> [...]). Mais ca ne marche que pour les types ouverts vers le
haut.

Jacques

@vicuna
Copy link
Author

vicuna commented Feb 13, 2002

Comment author: administrator

Erratum:

Je vois ton probleme: (x :> [< ... ]) est equivalent a (x : [< ... ]). En effet, il n'existe pas de sous-type propre d'un type polymorphe ouvert vers le bas (cad, qui peut perdre des cas). Quand on calcule le sous-type d'un variant polymorphe, on se base sur l'instance qui a le moins de cas (si elle n'est pas le variant vide, comme dans ton cas). Donc (x :> [> ...]) donne a x le meme type que
(x :> [...]). Mais ca ne marche que pour les types ouverts vers le
haut.

Je melangeais avec Ctype.subtype. (x : [< t] :> [> t]) est une
coercion valide, mais (x : [> t]) ne donne pas le type [< t] a` x, car
il n'est pas clair en quoi ce type serait "meilleur" que [> t].

  • enlarge t fait ce qu'il peut pour trouver un type plus general que t
    (et par consequent unifiable a` t) qui soit un de ses sous-types.
    Aucune garantie dans le cas general, mais certains cas particuliers
    sont presentes dans le tutorial.

  • subtype t1 t2 s'assure que t1 est un sous-type de t2, eventuellement
    forcant des unifications. t1 et t2 eux-memes n'ont pas a` etre
    unifiables.

Jacques

@vicuna vicuna added the bug label Mar 19, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant