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=2.3 required=5.0 tests=HTML_10_20,HTML_MESSAGE, SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id E2B1ABBC1 for ; Tue, 19 Feb 2008 11:23:17 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAGo8ukfAXQInh2dsb2JhbACCOjeNXAEBAQgKKZYghlg X-IronPort-AV: E=Sophos;i="4.25,375,1199660400"; d="scan'208";a="9339195" Received: from concorde.inria.fr ([192.93.2.39]) by mail3-smtp-sop.national.inria.fr with ESMTP; 19 Feb 2008 11:23:17 +0100 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m1JAN990006198 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Tue, 19 Feb 2008 11:23:17 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAEs9ukdC+VLqmGdsb2JhbACCOjeNXAEBAQEHBAQJChiWIIZa X-IronPort-AV: E=Sophos;i="4.25,375,1199660400"; d="scan'208";a="22780169" Received: from wx-out-0506.google.com ([66.249.82.234]) by mail4-smtp-sop.national.inria.fr with ESMTP; 19 Feb 2008 11:23:16 +0100 Received: by wx-out-0506.google.com with SMTP id h28so3011170wxd.0 for ; Tue, 19 Feb 2008 02:23:15 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from:sender:to:subject:mime-version:content-type:x-google-sender-auth; bh=MU2G5xh2u3G+B05RQ3JTSglgsLvwi9fJpj4ZwtRS4co=; b=f9YAsKl9aGHs+CzoRIV3JVD89aLMrOwiBI+NoBaXxzz69OVS/BoBTVFeWtmGPdzqdziPAN7tWXBiBOQx7WOfB/sufGwSp0tDoPhN5R1Csoy9ux1xCLKsDHqzCm40LZrnJvIfQ4eytybdT8046I+k6DrpEEMpMcTcQnfXwwIyYlU= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:sender:to:subject:mime-version:content-type:x-google-sender-auth; b=e0g2XpZ7owTlcYWrLuV6iPRl2Fzdev8+mU1n/Px/N2KDBMSCIFEMxDxvA7Ji8HGWwVkHGEe5zXzqOABftNv6riRNf/1RUZgUwlKXAH6bnogLQtX7o6EZMDDE2OCfMWmoVnuZ02H6/LehjmrrY99yvBYD/LQJc4Gb+874rxNyXIs= Received: by 10.150.191.10 with SMTP id o10mr2436568ybf.84.1203416595375; Tue, 19 Feb 2008 02:23:15 -0800 (PST) Received: by 10.150.211.21 with HTTP; Tue, 19 Feb 2008 02:23:15 -0800 (PST) Message-ID: <926565e50802190223r456d0ec2we4b8a4f51b134f42@mail.gmail.com> Date: Tue, 19 Feb 2008 11:23:15 +0100 From: "Johannes Kanig" Sender: johannes.kanig@gmail.com To: caml-list@inria.fr Subject: polymorphic variants and promotion MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----=_Part_6602_31352461.1203416595351" X-Google-Sender-Auth: 4fa237a0a0eebd1f X-Miltered: at concorde with ID 47BAAE0D.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; lri:01 variants:01 variants:01 val:01 val:01 a's:01 lri:01 a's:01 polymorphic:01 polymorphic:01 typing:01 typing:01 functions:01 functions:01 int:01 X-Attachments: cset="UTF-8" cset="UTF-8" ------=_Part_6602_31352461.1203416595351 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Content-Disposition: inline Hi, I ran into the following problem using polymorphic variants. Suppose I have 2 functions f and g (the function definitions don't make much sense - they are just there for typing purposes) : # let f (`A a) (`A i) = `A i ;; val f : [< `A of 'a ] -> [< `A of 'b ] -> [> `A of 'b ] = # let g (`A a) = (`B a) ;; val g : [< `A of 'a ] -> [> `B of 'a ] = For simplicity I assume that the type variables all instantiate to "int". Now, I want to construct a function h that takes an accumulator a and a list of `A's (for example [`A 1; `A 2; ...]) that produces either an object of type `A of int or an object of type `B of int in the following way: # let h a = function | [] -> g a | xs -> List.fold_left f a xs;; But this doesn't type: This expression has type [ `A of 'a ] but is here used with type [> `B of 'a ] The first variant type does not allow tag(s) `B I understand that the fold_left fixes the type of f the result of f to [`A of int] instead of [>`A of int]. The example as above can be easily repaired by replacing the second branch of the pattern matching by: let `A _ as x = List.fold_left f a xs in x which is fair enough (thanks to Romain Bardou for pointing this out). What I don't understand is why the promotion of [`A of int] to [> `A of int] is not possible in general: # `A 1;; - : [> `A of int ] = `A 1 # (`A 1 : [`A of int]) ;; - : [ `A of int ] = `A 1 # ((`A 1 : [`A of int]) : [> `A of int]) ;; - : [ `A of int ] = `A 1 Does anyone have an answer? -- Johannes Kanig johannes.kanig@lri.fr ------=_Part_6602_31352461.1203416595351 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: 7bit Content-Disposition: inline Hi,

I ran into the following problem using polymorphic variants. Suppose I have 2 functions f and g (the function definitions don't make much sense - they are just there for typing purposes) :

# let f (`A a) (`A i) = `A i ;;
val f : [< `A of 'a ] -> [< `A of 'b ] -> [> `A of 'b ] = <fun>
# let g (`A a) = (`B a) ;;
val g : [< `A of 'a ] -> [> `B of 'a ] = <fun>

For simplicity I assume that the type variables all instantiate to "int". Now, I want to construct a function h that takes an accumulator a and a list of `A's (for example [`A 1; `A 2; ...]) that produces either an object of type `A of int or an object of type `B of int in the following way:

# let h a = function
    | [] -> g a
    | xs -> List.fold_left f a xs;;

But this doesn't type:

This expression has type [ `A of 'a ] but is here used with type
  [> `B of 'a ]
The first variant type does not allow tag(s) `B

I understand that the fold_left fixes the type of f the result of f to [`A of int] instead of [>`A of int]. The example as above can be easily repaired by replacing the second branch of the pattern matching by:

let `A _ as x = List.fold_left f a xs in x

which is fair enough (thanks to Romain Bardou for pointing this out).

What I don't understand is why the promotion of [`A of int] to [> `A of int] is not possible in general:

# `A 1;;
- : [> `A of int ] = `A 1
# (`A 1 : [`A of int]) ;;
- : [ `A of int ] = `A 1
# ((`A 1 : [`A of int]) : [> `A of int]) ;;
- : [ `A of int ] = `A 1

Does anyone have an answer?

--
Johannes Kanig
johannes.kanig@lri.fr ------=_Part_6602_31352461.1203416595351--