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.0 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE, 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 concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id B1FB5BB83 for ; Wed, 13 Sep 2006 18:10:35 +0200 (CEST) Received: from nf-out-0910.google.com (nf-out-0910.google.com [64.233.182.189]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id k8DGAZaC018475 for ; Wed, 13 Sep 2006 18:10:35 +0200 Received: by nf-out-0910.google.com with SMTP id y38so1956010nfb for ; Wed, 13 Sep 2006 09:10:32 -0700 (PDT) DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:to:subject:mime-version:content-type; b=pHB00cpOJhQ3EhDe0T+1CrpUYFcvWp4jN7llaXp4/h7O2u+kuZwLPl4gWMUtu8h2gJ7fbMiKcuIoIGyXDr5fuSJwk2j5/pIPJy2S8VJ1RF4gJtofEInGia+hNbzphehym1xo2jjuShNCk9Jc3zhiDnyex1ui24uHdJ5XrC1MMTE= Received: by 10.49.55.13 with SMTP id h13mr11081088nfk; Wed, 13 Sep 2006 09:10:32 -0700 (PDT) Received: by 10.49.32.6 with HTTP; Wed, 13 Sep 2006 09:10:31 -0700 (PDT) Message-ID: Date: Wed, 13 Sep 2006 18:10:32 +0200 From: Tom To: caml-list Subject: Type system infering 'a and '_a MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----=_Part_326234_9897186.1158163832397" X-j-chkmail-Score: MSGID : 45082D7B.000 on concorde : j-chkmail score : X : 0/20 1 X-Miltered: at concorde with ID 45082D7B.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; ocaml:01 val:01 val:01 mutable:01 foo:01 foo:01 mutable:01 constructors:01 ocaml:01 constructors:01 polymorphic:01 polymorphic:01 defined:02 defined:02 poly:02 X-Attachments: cset="UTF-8" cset="UTF-8" ------=_Part_326234_9897186.1158163832397 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline I was playing a bit with Ocaml type system the other day... type 'a t1 = Empty1 | Full1 of 'a # let a1 = Empty1;; val a1 : 'a t1 = Empty1 Smart. type 'a t2 = Empty2 of 'a option ref | Full2 of 'a # let a2 = Empty2 (ref None);; val a2 : '_a t2 = Empty2 {contents = None} The type system won't infer a2 as being polymorphic, as it is mutable. Smart. type 'a t3 = Empty3 of string | Full3 of 'a # let a3 = Empty3 "foo";; val a3 : 'a t3 = Empty3 "foo" Even thou a3 is mutable, mutating it can't bind 'a, so a3 is polymorphic. Smart. type ('a, 'b) t4 = Empty4 of 'a option ref | Full4 of 'a * 'b # let a4 = Empty4 (ref None);; val a4 : ('_a, 'b) t4 = Empty4 {contents = None} As only 'a is "contained" in a mutable type, a4 is polymorphic only in 'b. Smart But now... type ('a, 'b) t5 = Empty_a5 of 'a option ref | Empty_b5 of 'b option ref | Full5 of 'a * 'b # let a5 = Empty_a5 (ref None);; val a5 : ('_a, '_b) t5 = Empty_a5 {contents = None} Stupid. Value a5 should be polymorphic in 'b! (And, with a bit of hacking: type 'a t1 = Empty1 | Full1 of 'a # let b1 = Full1 (Obj.magic 0);; val b1 : 'a t1 = Full1 Smart. type ('a, 'b) t4 = Empty4 of 'a option ref | Full4 of 'a * 'b # let b4 = Full4 (Obj.magic 0, Obj.magic 0);; val b4 : ('_a, 'b) t4 = Full4 (, ) Stupid. ) So we see that "mutability" of each type variable is defined for the whole type, not for the individual value constructors only. Is there a theoretical reason (of course, one reason is probably an easier implementation)? - Tom ------=_Part_326234_9897186.1158163832397 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: 7bit Content-Disposition: inline I was playing a bit with Ocaml type system the other day...

  type 'a t1 = Empty1 | Full1 of 'a
 
  # let a1 = Empty1;;
  val a1 : 'a t1 = Empty1

Smart.

  type 'a t2 = Empty2 of 'a option ref | Full2 of 'a
 
  # let a2 = Empty2 (ref None);;
  val a2 : '_a t2 = Empty2 {contents = None}


The type system won't infer a2 as being polymorphic, as it is mutable. Smart.

  type 'a t3 = Empty3 of string | Full3 of 'a
 
  # let a3 = Empty3 "foo";;
  val a3 : 'a t3 = Empty3 "foo"

Even thou a3 is mutable, mutating it can't bind 'a, so a3 is polymorphic. Smart.

  type ('a, 'b) t4 = Empty4 of 'a option ref | Full4 of 'a * 'b
 
  # let a4 = Empty4 (ref None);;
  val a4 : ('_a, 'b) t4 = Empty4 {contents = None}

As only 'a is "contained" in a mutable type, a4 is polymorphic only in 'b. Smart

But now...

  type ('a, 'b) t5 =
      Empty_a5 of 'a option ref
    | Empty_b5 of 'b option ref
    | Full5 of 'a * 'b
 
  # let a5 = Empty_a5 (ref None);;
  val a5 : ('_a, '_b) t5 = Empty_a5 {contents = None}

Stupid. Value a5 should be polymorphic in 'b!

(And, with a bit of hacking:

  type 'a t1 = Empty1 | Full1 of 'a
 
  # let b1 = Full1 (Obj.magic 0);;
  val b1 : 'a t1 = Full1 <poly>

Smart.

  type ('a, 'b) t4 = Empty4 of 'a option ref | Full4 of 'a * 'b
 
  # let b4 = Full4 (Obj.magic 0, Obj.magic 0);;
  val b4 : ('_a, 'b) t4 = Full4 (<poly>, <poly>)

Stupid.

)

So we see that "mutability" of each type variable is defined for the whole type, not for the individual value constructors only. Is there a theoretical reason (of course, one reason is probably an easier implementation)?

- Tom
------=_Part_326234_9897186.1158163832397--