[TYPES] Reference to typed first class pattern matching

[Edsko de Vries]

On Tue, Sep 09, 2008 at 10:59:25AM +0200, Michael Lienhardt wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Hello,
> 
> I was wondering if there was any existing work on typed first class  
> pattern matching.
> 
> Typically, I have a ML-like calculus with abstraction of the form $ 
> \lambda P.e$, were $P$ is a pattern matching for instance type  
> constructors and tuples.
> Moreover, one can combine abstraction like in $\lambda P.e + \lambda  
> P'.e'$, thus assembling pattern matching branches dynamically.
> One can also define a function $\lambda g.\lambda f.(f + g)$: we have  
> first class pattern matching.
> 
> I am interested to type such a calculus, using for instance  
> intersection types to deal with the $+$ constructor.
> Is there any previous work on first class pattern matching that can  
> help me design such a type system ?

This kind of thing can be done with extensible records:

A polymorphic type system for extensible records and variants (1996)
by Benedict R. Gaster, Mark P. Jones 

See also:

Extensible records with scoped labels. [bib, pdf] Daan Leijen. The 2005
Symposium on Trends in Functional Programming (TFP'05), Tallin, Estonia,
September 2005. Also published in the 3rd volume of Trends in Functional
Programming. 

Edsko