[TYPES] Reference to typed first class pattern matching

[Matthias Blume]

Hi Michael,

this might not be as general as you would like, but our ICFP'06 paper  
on first-class cases goes in that direction.  Some of the things you  
seem to be after can be coded up in that system:

   Extensible Programming with First-Class Cases.
   Matthias Blume, Umut A. Acar and Wonseok Chae.
   In Proceedings of the 11th ACM SIGPLAN International Conference on  
Functional Programming (ICFP'06).
   Portland, Oregon. Sep 18-20, 2006.

The type system is based straightforwardly on Remy-style row  
polymorphism, here applied to sums.  It is also quite closely related  
to polymorphic variants as found in OCaml.  (However, one crucial  
difference is that in OCaml one cannot extend a match without knowing  
what is being extended.  If I am guessing correctly, this probably  
means that OCaml-style polymorphic variants won't work for you.)

Matthias


On Sep 9, 2008, at 3:59 AM, 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 ?
>
> Michael Lienhardt
> PhD student.