From mboxrd@z Thu Jan  1 00:00:00 1970
Received: by pauillac.inria.fr; Wed, 1 Dec 93 14:09:34 +0100
Received: from margaux.inria.fr by pauillac.inria.fr; Wed, 1 Dec 93 11:57:20 +0100
Received: from pauillac.inria.fr by margaux.inria.fr, Wed, 1 Dec 93 11:57:14 +0100
Received: by pauillac.inria.fr; Wed, 1 Dec 93 11:57:12 +0100
Message-Id: <9312011057.AA16359@pauillac.inria.fr>
Subject: Existential types variables (unix patch)
To: caml-list@margaux.inria.fr
Date: Wed, 1 Dec 1993 11:57:11 +0100 (MET)
From: Michel.Mauny@inria.fr (Michel Mauny)
Reply-To: Michel.Mauny@inria.fr
Organization: INRIA, BP 105, F-78153 Le Chesnay Cedex, France
Phone: (+33) 1 39 63 57 96 -- Fax: (+33) 1 39 63 53 30
X-Mailer: ELM [version 2.4 PL21]
Content-Type: text/plain
Sender: weis@pauillac.inria.fr

Hi,

A patch introducing a simple form of existential types (following
Laufer and Odesky's proposal) is now available for Caml-Light 0.6 on
ftp.inria.fr [192.93.2.54], file
~ftp/lang/caml-light/cl6existpatch.tar.Z

This extension provides a very simple form of abstract types and should
be suseful (at least) for teaching.

Since there is no machine-specific code in the patch, patched files
should compile on all Caml-Light 0.6 ports.

The archive essentially contains a README file, a diff file (to be given
as input to `patch'), and some documentation about this new feature.

To install it, follow the instructions given in the README file in the
archive. You'll have build a new Caml-Light system, expected to be
compatible with the old one.

What follows is an extract of the file exist.doc from the archive, to
give you an idea of the extension. More interesting examples can be
found in the archive.

Sincerely,

Michel Mauny and Francois Pottier
(Michel.Mauny@inria.fr, Francois.Pottier@ens.fr)

-----------------------------------------------------------------------------

1. What do we have more?
=========================

In this extension, type variables occuring free in type definitions
aren't errors any longer. They are considered as existentially
quantified. For instance, the following type definition is accepted:

   #type key = Key of 'a * ('a -> int);;

This means that it is now possible to build values such as:

   #let k1 = Key([1;2;3], list_length)
   #and k2 = Key(5, succ);;
   k1 : key = Key (<abstract>, <fun>)
   k2 : key = Key (<abstract>, <fun>)

The typechecker made sure that in a value "Key(x,f)", x is a valid
argument to f.

Also, we are able to decompose values of type key as:

   #let (Key(r1,f1)) = k1;;
   f1 : ?A -> int = <fun>
   r1 : ?A = <abstract>

The types of r and f have existential type variables (written "?a"),
and f can be applied to r:

   #f1 r1;;
   - : int = 3

Now, if we decompose k2, f and r (from k1) cannot be mixed with k2's
components:

  #let (Key(r2,f2)) = k2;;
   f2 : ?B -> int = <fun>
   r2 : ?B = <abstract>

   #f2 r1;;
   > Toplevel input:
   >f2 r1;;
   >   ^^
   > Expression of type ?A
   > cannot be used with type ?B

If we decompose k1 again, we obtain values f'1 and r'1 whose types are
incompatible with f1 and r1:

   #let (Key(r'1, f'1)) = k1;;
   f'1 : ?C -> int = <fun>
   r'1 : ?C = <abstract>

   #f'1 r1;;
   > Toplevel input:
   >f'1 r1;;
   >    ^^
   > Expression of type ?A
   > cannot be used with type ?C

-----------------------------------------------------------------------------