From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id TAA25337 for caml-redistribution; Wed, 4 Jun 1997 19:43:08 +0200 (MET DST)
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id TAA25317 for <caml-list@pauillac.inria.fr>; Wed, 4 Jun 1997 19:42:32 +0200 (MET DST)
Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.8.5/8.7.3) with ESMTP id TAA13367; Wed, 4 Jun 1997 19:42:30 +0200 (MET DST)
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id TAA25313; Wed, 4 Jun 1997 19:42:29 +0200 (MET DST)
From: Pierre Weis <Pierre.Weis@inria.fr>
Message-Id: <199706041742.TAA25313@pauillac.inria.fr>
Subject: Re: A propos de "this matching case is unused"
In-Reply-To: <33957EB5.1BA8@irit.fr> from Didier Plaindoux at "Jun 4, 97 04:41:57 pm"
To: plaindou@irit.fr (Didier Plaindoux)
Date: Wed, 4 Jun 1997 19:42:29 +0200 (MET DST)
Cc: caml-list@inria.fr
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Sender: 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/