[Prev][Next][Index][Thread]

Re: Type names vs type structure

> I've pondered upon building a scripting language with an
> orthogonal design much like the one Andrew Kennedy proposes.
> 
>   1. Functions
>   2. Labeled sums and products, with row types (a la Wand et al)
>   3. Full polymorphism (a la Odersky/Laufer or Mark Jones)
>   4. Recursion, allowing any rational tree to describe a type

All ingredients (1), (2 --products only), (3), and (4) were altogether in the
language MLART that I used to program objects in [2]. However, the extended
version with full proofs has never been published.  

One approach to (2) was described in my very first paper [1]. Technically,
variant types are similar to records types.  However, variants differ from
records in a few significant ways and the design of a language with variant
types is slightly more difficult than the design of one with record
types. One inconvenience is that variant values must be polymorphic (in some
row variable), while record values are monomorphic (no row
variable). Another related issue is the distinction between closed switches
and open ones (i.e. with an otherwise clause) that has no counter-part in
records.

Regarding point (3), you might also have a look at the more recent work by
Jacques Garrigue and myself [3].

Regarding point (4), one must be careful.  Type inference in ML reduces to
unification plus an obvious management of polymorphism. The results carry
out to infinite terms rather easily, although I never saw this fully
formalized. I myself have shown this reduction for finite terms in [4]: the
algorithms and proofs were parameterized by an equational theory and written
so that they  extend to infinite terms but I did not actually write the
details for infinite terms.  Let us admit that the problem of type inference
reduces to the problem of unification. Still...

In a free algebra, unification for infinite terms can be done as unification
for finite terms provided the algorithm has been designed to keep all
sharing, as in [5] or, equivalently, using multi-equations.

However, record types are not terms of a free algebra, but those of a sorted
algebra taken modulo an equational theory. The latter is used to describe
permutation of fields and expansion of templates.  The former is used to
restrict the set of types to well-sorted ones.

In general, the extension of an equational algebra with infinite terms is
non trivial (see the example below).  The problem disappears with record
types because the types are so constrained by sorts that recursion cannot
overlap with the axioms any longer. (Intuitively, if you think of the
regular tree rec x. f x as a new constant c with the axiom c = f c, we could
say there is no critical pair.)


RECURSION + EQUATIONS  DO NOT MIX WELL
----------------------------------------

Consider for instance an algebra with two unary symbols f and g.  Variables
are written with letters x,y,z.  Let us quotient the algebra by the
left-commutativity axiom:

        f g x = g f x

With finite terms, the equation y = f y (1) has no solution.  With infinite
terms it has the obvious solution:

        F == rec z. f z

but it also has the unexpected solution g F. Indeed, for any solution t of
the equation (1), we have g t = g f t = f g t.  Thus g(t) is also a
solution.  Hence, F and g F are two solutions of the equation (1).  However,
the terms F and g F are not equal. (The symbol g will always occur in any
equivalence class of any non-trivial truncation of g F, but it never occurs
in any equivalence class of any truncation of F.)  Hence, the solutions F
and g F are incomparable and the unification problem has no principal
unifiers. (Since they are at least an infinite number of incomparable
solutions { g^n F, n >= 0 }, unification is not even finitary.)

        -Didier


Bibliography:
----------------

[1] @inproceedings{
  author       = "Didier R{\'e}my",
  title        = "Records and Variants as a natural Extension of {ML}",
  booktitle    = "Sixteenth Annual Symposium on
                  Principles Of Programming Languages",
  year         = 1989
              }

[2] @InProceedings{
  author     = "Didier R{\'e}my",
  title      = "Programming Objects with {ML-ART}:
                An extension to {ML} with Abstract and Record Types",
  booktitle  = "International Symposium on
                Theoretical Aspects of Computer Software",
  year       = 1994,
  editor     = "Masami Hagiya and John C. Mitchell",
  series     = "Lecture Notes in Computer Science",
  volume     =  789,
  pages      = "321--346",
  publisher  = "Springer-Verlag",
  address    = "Sendai, Japan",
  month      = "April"
  }

[3] @inproceedings{
  author     = "Jacques Garrigue and Didier R{\'e}my",
  title      = "Extending {ML} with Semi-Explicit Higher-Order Polymorphism",
  booktitle  = "International Symposium on
                Theoretical Aspects of Computer Software",
  year       = 1997,
  month      = "September",
  series     = "Lecture Notes in Computer Science",
  publisher  = "Springer",
  volume     =  1281,
  pages      =  "20--46"
  }


[4] @TechReport{
  author     = "Didier R{\'e}my",
  title      = "Extending {ML} Type System with a Sorted
                Equational Theory", 
  institution= "Institut National de Recherche en Informatique et Automatisme",
  address    = "Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France",
  type       = "Research Report",
  number     = 1766,
  year       = 1992
  }

[5] @phdthesis{
  author =       "G{\'e}rard Huet",
  title =        "R\'e\-so\-lu\-tion  d'\'equa\-tions   dans  les  langages
                  d'ordre $1,2,\ldots,\omega$",
  type =         "Th\`e\-se de doctorat d'\'e\-tat",
  school =       "Universit\'e Paris~7",
  year =         "1976"
}