From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: weis
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id IAA20147 for caml-redist; Wed, 26 Apr 2000 08:44:23 +0200 (MET DST)
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id CAA08413 for <caml-list@pauillac.inria.fr>; Wed, 26 Apr 2000 02:25:16 +0200 (MET DST)
Received: from shell5.ba.best.com (shell5.ba.best.com [206.184.139.136])
	by concorde.inria.fr (8.8.7/8.8.7) with ESMTP id CAA22755
	for <caml-list@inria.fr>; Wed, 26 Apr 2000 02:25:15 +0200 (MET DST)
Received: from localhost (bpr@localhost)
	by shell5.ba.best.com (8.9.3/8.9.2/best.sh) with ESMTP id RAA07599
	for <caml-list@inria.fr>; Tue, 25 Apr 2000 17:25:10 -0700 (PDT)
Date: Tue, 25 Apr 2000 17:25:09 -0700 (PDT)
From: Brian Rogoff <bpr@best.com>
To: caml-list@inria.fr
Subject: Polymorphic variants question
Message-ID: <Pine.BSF.4.21.0004251643180.11908-100000@shell5.ba.best.com>
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
Sender: weis

Hi,

A long time ago John Prevost posted a nice trick to get a kind of 
downcasting in OCaml

class type ['a] super =
  object
    method downcast : 'a
  end;;

class type ['a] a =
  object
    inherit ['a] super
    method do_a : int
  end;;

class type ['a] b =
  object
    inherit ['a] super
    method do_b : float
  end;;

type objsum = A of objsum a | B of objsum b;; 

Which have types 

#   class type ['a] super = object method downcast : 'a end
#   class type ['a] a = object method do_a : int method downcast : 'a end
#   class type ['a] b = object method do_b : float method downcast : 'a
end
#   type objsum = A of objsum a | B of objsum b

And to show that it works, he gave the following test code:

class test_a =
    object (s)
      method downcast = A (s :> objsum a)
      method do_a = 1
    end;;
  class test_b =
    object (s)
      method downcast = B (s :> objsum b)
      method do_b = 1.0
    end;;

#  class test_a : object method do_a : int method downcast : objsum end
#  class test_b : object method do_b : float method downcast : objsum end

and so on, testing that this meets assumptions. 

If we replace the variant with a polymorphic variant. 
type objsum = [`A of objsum a | `B of objsum b];;

and then we do the same thing as before the type checker complains. 

# class test_a =
    object (s)
      method downcast = `A (s :> objsum a)
      method do_a = 1
    end;;
# Characters 6-103:
# Some type variables are unbound in this type:
# class test_a : object method do_a : int method downcast : #objsum[>`A]
end
# The method downcast has type #objsum[>`A] where 'a is unbound

This is a good error message, and it tells me what to do to fix the
problem right away: I add an annotation to constrain that "#objsum[>`A]" 

# class test_a =
  object (s)
    method downcast : objsum = `A (s :> objsum a)
    method do_a = 1
  end;;
  class test_b =
    object (s)
      method downcast : objsum = `B (s :> objsum b)
      method do_b = 1.0
    end;;

# class test_a : object method do_a : int method downcast : objsum end
# class test_b : object method do_b : float method downcast : objsum end

Now, in order to avoid surprises in the future, can someone tell me why I
should have expected that type "#objsum[>`A]" to be computed, and hence known
that I would need to constrain the type? It makes sense, but I don't yet
have a good mental model for the typing of polymorphic variants
which would have allowed me to write the correct version immediately. How 
do the experts go about mentally inferring the right types in cases like
this?

-- Brian