From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.4 required=5.0 tests=DNS_FROM_RFC_ABUSE, DNS_FROM_RFC_WHOIS autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 072D5BBAF for ; Sat, 10 Jan 2009 12:34:50 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtYCAHcWaEmK54gDgWdsb2JhbACUEAEBFiK8K4Vv X-IronPort-AV: E=Sophos;i="4.37,243,1231110000"; d="vcf'?scan'208";a="19396155" Received: from rouge.crans.org ([138.231.136.3]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 10 Jan 2009 12:34:49 +0100 Received: from localhost (localhost.crans.org [127.0.0.1]) by rouge.crans.org (Postfix) with ESMTP id 19CDC8175 for ; Sat, 10 Jan 2009 12:34:49 +0100 (CET) X-Virus-Scanned: Debian amavisd-new at crans.org Received: from rouge.crans.org ([10.231.136.3]) by localhost (rouge.crans.org [10.231.136.3]) (amavisd-new, port 10024) with LMTP id yhzfQ8SLeIEZ for ; Sat, 10 Jan 2009 12:34:48 +0100 (CET) Received: from [138.231.138.177] (krypton.crans.org [138.231.138.177]) (using TLSv1 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (No client certificate requested) by rouge.crans.org (Postfix) with ESMTP id E8CF38063 for ; Sat, 10 Jan 2009 12:34:48 +0100 (CET) Message-ID: <496887BE.8030804@dptinfo.ens-cachan.fr> Date: Sat, 10 Jan 2009 12:34:22 +0100 From: Antoine Delignat-Lavaud Organization: ENS Cachan User-Agent: Mozilla/5.0 (Windows; U; Windows NT 6.0; fr; rv:1.8.1.19) Gecko/20081209 Lightning/0.9 Thunderbird/2.0.0.19 Mnenhy/0.7.5.666 MIME-Version: 1.0 To: caml-list@yquem.inria.fr Subject: Why does value restriction not apply to the empty list ? Content-Type: multipart/mixed; boundary="------------060903000509040108050300" X-Spam: no; 0.00; undergrad:01 ocaml:01 ocaml:01 ocaml's:01 bool:01 polymorphic:01 polymorphic:01 integer:01 ens-cachan:01 int:01 int:01 expression:02 expression:02 caml:02 string:02 X-Attachments: cset="utf-8" name="antoine_delignat-lavaud.vcf" name="antoine_delignat-lavaud.vcf" This is a multi-part message in MIME format. --------------060903000509040108050300 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Dear caml experts, While completing a project for my undergrad programming course, I have tumbled on a behavior in ocaml (my version is 3.10) that I don't quite understand. We are required to write a polymorphic Hindley-Milner type inferer in Ocaml for a dialect of ML with references and lists. I chose to solve the problem of polymorphic references by adding value restriction* to my inferer, using ocaml to check my results. Not knowing whether the empty list should be considered a value or an expression, I copied Ocaml's behavior and made it a value. As a result, my inferer gave the following expression the integer type : let el = [] in if hd el then 1 else hd el ;; which is the expected result since el has polymorphic type 'a list but does not look right because it is used as both a bool list and an int list. In Ocaml, the program let el = [] in if List.length el > 0 then (List.hd el)+(int_of_string (List.hd el)) else 0 ;; yields not type error and returns 0 despite the use of el as both an int list and a string list. Thus, I am wondering why does value restriction not apply to the empty list in Ocaml. I don't think it's possible to do a cast with the empty list (it is empty after all) but I don't see any benefit in doing so. Thanks for any tip. With regards, Antoine Delignat-Lavaud * see "A syntatic approach to type soundness", A. Wright, 1992 or "Relaxing the value restriction", J. Garrigue --------------060903000509040108050300 Content-Type: text/x-vcard; charset=utf-8; name="antoine_delignat-lavaud.vcf" Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename="antoine_delignat-lavaud.vcf" begin:vcard fn:Antoine Delignat-Lavaud n:Delignat-Lavaud;Antoine org;quoted-printable:ENS Cachan;=C3=89l=C3=A8ve au d=C3=A9partement d'informatique adr;dom:;;M310;Cachan email;internet:antoine.delignat-lavaud@dptinfo.ens-cachan.fr tel;cell:0608401862 version:2.1 end:vcard --------------060903000509040108050300--