subtyping variants

• To: types@dcs.gla.ac.uk
• Subject: subtyping variants
• From: Radu Grosu <grosu@informatik.tu-muenchen.de>
• Date: Tue, 12 Oct 1993 19:45:29 +0100
• Approved: types@dcs.gla.ac.uk

What is the current state of art in (sub)typing variants?
For example consider the following data type declaration:

data I1 = Xcoord | Ycoord | Mv(Real,Real)

I would like to write something like

data I2 = Color | I1

instead of

data I3 = Color | Coerce(I1)

If one considers only non-recursive (polymorphic) data type 
declarations then:

1) Are type reconstruction algorithms awailable to compute 
   the principal type of functions defined by using the 
   constructors of I2?

2) Is there any functional of the form:

   I2-w :: x -> (I1 -> x) -> I2 -> x

   I2-w (a)(f)(x) = case x of
      Color     => a
      otherwise => f x

   corresponding to the functional obtained for I3:

   I3-when :: x -> (I1 -> x) -> I3 -> x

   I3-when (a)(f)(bottom)   = bottom
   I3-when (a)(f)(Color)    = a
   I3-when (a)(f)(Coerce u) = f u

What about recursive data type declarations?

I would be grateful for relevant references.
I will post a summary if interest is shown.

radu

------------------------------------------------------------------------
Radu Grosu
Institut fuer Informatik
Technische Universitaet Muenchen
Arcisstrasse 21                   Email: grosu@informatik.tu-muenchen.de
D-80290 Muenchen                  Phone: ++49-89-2105-2398
Germany.                          Fax:   ++49-89-2105-8183

• Prev: paper available
• Next: proof terms for classical logic in natural deduction formulation
• Index(es):
  • Main
  • Thread