From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <garrigue@math.nagoya-u.ac.jp>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: 
X-Spam-Status: No, score=0.4 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE 
	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 6506DBBAF
	for <caml-list@yquem.inria.fr>; Thu, 10 Sep 2009 16:21:10 +0200 (CEST)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: ApoEADeoqEqCNhAB/2dsb2JhbADeW4QYBYI4
X-IronPort-AV: E=Sophos;i="4.44,364,1249250400"; 
   d="scan'208";a="32533585"
Received: from kurims.kurims.kyoto-u.ac.jp ([130.54.16.1])
  by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 10 Sep 2009 16:21:08 +0200
Received: from localhost (orion [130.54.16.5])
	by kurims.kurims.kyoto-u.ac.jp (8.13.8/8.13.8) with ESMTP id n8AEL2XW029715;
	Thu, 10 Sep 2009 23:21:02 +0900 (JST)
Date: Thu, 10 Sep 2009 23:21:02 +0900 (JST)
Message-Id: <20090910.232102.112610940.garrigue@math.nagoya-u.ac.jp>
To: guillaume.yziquel@citycable.ch
Cc: caml-list@inria.fr
Subject: Re: [Caml-list] polymorphic method.
From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
In-Reply-To: <4AA8F986.1060206@citycable.ch>
References: <4AA8F16F.1040009@citycable.ch>
	<20090910.214827.104047449.garrigue@math.nagoya-u.ac.jp>
	<4AA8F986.1060206@citycable.ch>
X-Mailer: Mew version 6.2.51 on Emacs 22.3 / Mule 5.0 (SAKAKI)
Mime-Version: 1.0
Content-Type: Text/Plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
X-Spam: no; 0.00; guillaume:01 guillaume:01 recursion:01 doable:01 principality:01 'self:01 'self:01 typable:01 typable:01 val:01 val:01 annotations:01 polymorphism:01 compiler:01 inference:01 

From: Guillaume Yziquel <guillaume.yziquel@citycable.ch>
> By the way, I do not exactly understand the "you might end up with
> types more polymorphic than you expected" part.

This is actually the main problem.
At some point, I actually considered generating automatically
polymorphic method types where possible.
The idea would be simply to first give all the methods in a class
monomorphic types (to avoid the undecidability of polymorphic recursion), 
and then generalize all type variables that do not "escape": i.e. do
not appear in class parameters, value fields, or global references.
Technically this is perfectly doable.
Theoretically, there are problems with principality, as there is no
most generic type for a polymorphic method (all types are incompatible
with each other).
It is easier to see that on a practical example.
Say that I defined lists:

class ['a] cons x l = object (_ : 'self)
  method hd : 'a = x
  method tl : 'self = l
end

class nil = object
  method hd = raise Empty
  method tl = raise Empty
end

Now, both cons and nil would be typable (cons is already typable), and
the inferred types would be:
class ['a] cons : 'a -> 'b ->
  object ('b) method hd : 'a method tl : 'b end

class nil : object
  method hd : 'a
  method tl : 'b
end

At first glance, it seems that the type of nil being completely
polymorphic, we could pass it as second argument to cons.
However, it is not the case. cons has two monomorphic methods, while
nil has two polymorhic methods, and their types are incomparable.
If we look at object types,

type 'a cons = < hd : 'a; tl : 'b > as 'b
type nil = < hd : 'a.'a ; tl : 'b.'b >

Of course, you could argue that what is wrong is the definition of
nil. But basically there is no way to decide what is the right type
for nil as soon as we allow inferring polymorphic methods.

Interestingly, currently you can define nil as an immediate object
and have immediately the right type without any annotation:

exception Empty
let nil = object
  method hd = raise Empty
  method tl = raise Empty
end ;;
val nil : < hd : 'a; tl : 'b > = <obj>

let l = new cons 3 nil ;;
val l : int cons = <obj>

So, the current approach is to privilege the monomorphic case,
requiring type annotations for the polymorphic case. Your suggestion
of allowing to give a hint that you want a polymorphic type makes
sense, but it does not say which polymorphic type: there might be
several, with different levels of polymorphism, with no way to choose
between them. Probably it would be ok to choose the most polymorphic
one, but one can always find counter-examples. So the meaning of your
"polymorphic" keyword would be: "give me the most polymorphic type for
this method, I hope I understand what it will be, but if I'm wrong and
it breaks my program I won't complain". This may be practically ok,
but this is a hard sell as a language feature. Particularly when you
think that future versions of the compiler may be able to infer more
polymorphic types, thanks to improvements in type inference, and
suddenly break your program.

Jacques Garrigue