[TYPES] records from intersections; variants from unions?

Sam TH samth at ccs.neu.edu
Sat Jul 11 08:05:43 EDT 2009


On Sat, Jul 11, 2009 at 8:10 AM, William Lovas<wlovas at stwing.upenn.edu> wrote:
> 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?

In Typed Scheme [1,2], this is exactly how variants are implemented.
Here's an example of a tree type:

#lang typed-scheme
(define-struct: Node ([l : Tree] [r : Tree]))
(define-struct: Leaf ([v : Number]))
(define-type-alias Tree (U Node Leaf))

[1] http://docs.plt-scheme.org/ts-reference/
[2] Sam Tobin-Hochstadt and Matthias Felleisen, the Design and
Implementation of Typed Scheme, POPL 2008,
http://www.ccs.neu.edu/scheme/pubs/#popl08-thf
-- 
sam th
samth at ccs.neu.edu


More information about the Types-list mailing list