[TYPES] records from intersections; variants from unions?

[William Lovas]

Hello all,

I've read several places about a trick whereby you can define a language
with only single-field records, but derive the general n-ary version via
intersection types.  (I first read about it in Reynolds's work, but i've
listed some other references below.)  Does anybody know of any work that
dualizes this trick, recovering n-ary variants from a single-constructor
variety using union types?

Thanks for any pointers!

William


References

[1] John C. Reynolds, Design of the Programming Language Forsythe, Report 
    CMU-CS-96-146, Carnegie Mellon University, 1996.
    http://reports-archive.adm.cs.cmu.edu/anon/1996/CMU-CS-96-146.ps.gz

[2] Alexei Kopylov, Dependent Intersection: A New Way of Defining Records
    in Type Theory, LICS 2003.  http://files.metaprl.org/papers/dinter.pdf

[3] Jan Zwanenburg, Record Concatenation with Intersection Types, Computing
    Science Report CS-95-34, Eindhoven University of Technology, 1995.
    http://www.cs.ru.nl/~janz/publications/concatenation0.ps