A propos de "this matching case is unused"

A propos de "this matching case is unused"

[Didier Plaindoux]

N'ayant pas entrevu de message a ce propos je me permet
de poser la question suivante : 

Soit le code suivant (stupide soit mais pas pour le typage)

# fun x -> x
#   | x -> 1 + x
#;;

La reponse est la suivante :

Toplevel input:
>  | x -> 1 + x
>    ^
Warning: this matching case is unused.
- : int -> int = <fun>

Ma question est la suivante : pourquoi prendre en compte
cette branche lors du typage, qui de ce fait instancie le
type de 'x' par 'int' ? 

D. Plaindoux

-- 
o----------o---------------------------------------o
|S.L.O.O.P.|           Didier PLAINDOUX            |
+----------+        mailto:plaindou@irit.fr        |
|  |\_/|   |  http://www.irit.fr/~Didier.Plaindoux |
|  (o O)   |  Tel : 05 61 55 [ 63 56 | 82 09 ]     |    
|   ( )    |  @   : IRIT,UPS 118 route de Narbonne |
|    O     |        31062 Toulouse France          |
o--------------------------------------------------o

Re: A propos de "this matching case is unused"

[Pierre Weis]

> N'ayant pas entrevu de message a ce propos je me permet
> de poser la question suivante : 
> 
> Soit le code suivant (stupide soit mais pas pour le typage)
> 
> # fun x -> x
> #   | x -> 1 + x
> #;;
> 
> La reponse est la suivante :
> 
> Toplevel input:
> >  | x -> 1 + x
> >    ^
> Warning: this matching case is unused.
> - : int -> int = <fun>
> 
> Ma question est la suivante : pourquoi prendre en compte
> cette branche lors du typage, qui de ce fait instancie le
> type de 'x' par 'int' ? 

1) Parceque la de'tection du ``cas inutile'' n'est pas de la
responsabilite' du contro^leur de type, c'est le compilateur qui en
fait l'analyse, apre`s le passage du typeur.

2) C'est une proprie'te' se'mantique du programme qui n'est pas du ressort
de conside'rations de typage. De la me^me manie`re

(function x -> if true then x else 1)

aura le type int -> int, quand il est clair que cette fonction est
e'quivalente a` (function x -> x) qui a le type 'a -> 'a.

Conclusion: le contro^leur de types traite votre programme, tout votre
programme, rien que votre programme. Il de'tectera une erreur me^me
s'il existe un programme simplifie' e'quivalent au vo^tre qui pourrait
e^tre correctement type'. (L'analyseur syntaxique fait de me^me et
conside`re if false then + - * else 1 comme syntaxiquement incorrect,
alors qu'il pourrait jetter la branche then sans changer la
se'mantique du programme.)

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://pauillac.inria.fr/~weis/