On Fri, 2005-08-19 at 06:51 +0900, Jacques Garrigue wrote:
> From: nr@eecs.harvard.edu (Norman Ramsey)
> 
> > I'm trying to write a small, extensible interpreter, and I'd like to
> > use polymorphic variants as the extension mechanism. 

> > Is there some way to define a recursive, *extensible* type using
> > polymorphic variants?  
> 

> "Code reuse through polymorphic variants" at
> http://www.math.nagoya-u.ac.jp/~garrigue/papers/

This paper is good but very skimpy .. :)

Open recursion is used, and types are inferred from functions.
It is possible to use the same techniques to define the
required types explicitly too, basic Felix bound term type
definition uses this:

(** value typing *)
type 't b0typecode_t' = 
  [
  | `BTYP_inst of bid_t * 't list 
  | `BTYP_tuple of 't list         
  | `BTYP_unitsum of int
  | `BTYP_sum of 't list 
  | `BTYP_function of 't * 't
  | `BTYP_pointer  of 't 
  | `BTYP_lvalue  of 't 
  | `BTYP_array of 't * 't 
  | `BTYP_void                       
  | `BTYP_fix of int      
  | `BTYP_var of int     
  ]

(** meta typing *)
type 't b1typecode_t' =
  [
  | `BTYP_apply of 't * 't 
  | `BTYP_typefun of (int * 't) list * 't * 't
  | `BTYP_type
  | `BTYP_type_tuple of 't list
  | `BTYP_type_match of 't * ('t * 't) list
  ]

(** general typing *)
type 't btypecode_t' =
  [
  | 't b0typecode_t'
  | 't b1typecode_t'
  ]

type b0typecode_t = 't b0typecode_t' as 't
type btypecode_t = 't btypecode_t' as 't

Unfortunately, whilst I could use this technique for many terms
other than typecodes, I haven't because it is somewhat clumbsy
to write out terms with all the required added parameters and
then close the recursions. For just one extension over one variable
we have a 1 parameter overhead in the type definitions, and 9 lines
for the closure.

Inference removes the need to write out the types, but it makes
debugging virtually impossible. In addition, type inference isn't
strong enough to deduce the "correct" typing for all expressions,
coercions are sometimes required, and in practice to write them
abbreviations are necessary.

Having warned you .. I would never go back to ordinary variants
after using polymorphic ones: Felix uses them almost exclusively,
and even though I don't use the features heavily, knowing that
it is possible to refine the typing later seems a major software
engineering plus.

-- 
John Skaller <skaller at users dot sourceforge dot net>