From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id RAA17479; Fri, 6 Aug 2004 17:33:46 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id RAA16926 for ; Fri, 6 Aug 2004 17:33:45 +0200 (MET DST) Received: from smtp.cegetel.net (mf00.sitadelle.com [212.94.174.77]) by nez-perce.inria.fr (8.12.10/8.12.10) with ESMTP id i76FXimL003324 for ; Fri, 6 Aug 2004 17:33:44 +0200 Received: from univ-savoie.fr (unknown [80.125.79.136]) by smtp.cegetel.net (Postfix) with ESMTP id 8D64E671F8; Fri, 6 Aug 2004 17:33:41 +0200 (CEST) Message-ID: <4112C744.2000304@univ-savoie.fr> Date: Thu, 05 Aug 2004 19:48:20 -0400 From: Christophe Raffalli User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.6) Gecko/20040115 X-Accept-Language: en-us, en MIME-Version: 1.0 To: Diego Olivier Fernandez Pons Cc: caml-list@inria.fr Subject: Re: [Caml-list] Peut on unifier foncteurs et objets ? References: In-Reply-To: X-Enigmail-Version: 0.83.3.0 X-Enigmail-Supports: pgp-inline, pgp-mime Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit X-Miltered: at nez-perce with ID 4113A4D8.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; raffalli:01 raffalli:01 univ-savoie:01 caml-list:01 foncteurs:01 typage:01 foncteurs:01 semantique:01 typage:01 abandonne:01 precisement:01 implanter:01 specifier:01 specifier:01 savoie:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Pour faire (vraiment trop) simple, OUI: Si on oublie un peu le typage (pas pour longtemps) - Un module c'est un record + des existentiels pour les types abstraits. - Il faut aussi un epsilon de Hilbert pour interpréter le M.t quand t est un type et pour pouvoir ainsi écrire des contraintes de types. - Un foncteurs n'est alors qu'une fonction + des contraintes de types. - Un object n'est qu'un record récursifs (à cause du self) (il faut aussi un peu de sucre syntaxique pour la surcharge et l'héritage et quelques décisions quant à leur sémantique). Le pb c'est le typage, mais si l'on abandonne la décidabilité, il suffit d'une extension de système F: système ST (voir mes deux papiers sur ma page et la thèse a venir (6 mois ?) de Frédérique Ruyer qui sera précisément sur ce sujet). En plus dans le système que l'on propose et que l'on va implanter, on pourra aussi spécifier les programmes (de toutes façons, pour écrire toutes les contraintes de types dont on a besoin, il faut presque tout système ST, et si on prends tout, on peut spécifier et prouver). -- Christophe Raffalli Université de Savoie Batiment Le Chablais, bureau 21 73376 Le Bourget-du-Lac Cedex tél: (33) 4 79 75 81 03 fax: (33) 4 79 75 87 42 mail: Christophe.Raffalli@univ-savoie.fr www: http://www.lama.univ-savoie.fr/~RAFFALLI --------------------------------------------- IMPORTANT: this mail is signed using PGP/MIME At least Enigmail/Mozilla, mutt or evolution can check this signature --------------------------------------------- ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners