[TYPES] Reference to typed first class pattern matching

[Morten Rhiger]

In an article that is going to appear as a Functional Pearl in the
Journal of Functional Programming, I present a library of typed first
class pattern combinators implemented in Haskell.  Using this library,
one can, among other things, construct both or-patterns and clauses
dynamically, so the $+$ that Michael wants is within reach.

The article is available at

   http://www.itu.dk/people/mir/typesafepatterns.pdf

-- Morten

On Thu, Sep 11, 2008 at 11:23 AM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Another work that may be relevant is:
>
>   Noam Zeilberger: Focusing and higher-order abstract syntax. POPL
> 2008: 359-369
>
> Yours,  -- P
>
> On 10 Sep 2008, at 20:13, eduardo at sol.lifia.info.unlp.edu.ar wrote:
>
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/
>> types-list ]
>>
>> Dear Micheal,
>>
>>       There are a number of references that are related to your
>> question and that you might find useful (listed in no particular
>> order):
>>
>>       1) Old (1990) work by Vincent van Oostrom on a lambda calculus
>> allowing one to abstract over arbitrary terms ("Lambda calculus with
>> patterns"). Untyped setting. [1]
>>       2) Previous work revised and extended (joint with Klop and De
>> Vrijer)[2]
>>       3) Work by Gilles Barthe et al on PTS with patterns [3]
>>       4) Work of Barry Jay on his Bondi programming language (see
>> his homepage)
>>       5) Delia Kesner and Barry Jay's First-Class Patterns (see Delia
>> Kesner's homepage)
>>       6) The rho calculus (see Horatiu Cirstea's homepage)
>>
>>       Regards,
>>       E.
>>
>>
>> [1] Vincent van Oostrom
>> Lambda Calculus with Patterns
>> Technical Report IR-228, Vrije Universiteit, Amsterdam, 40 pages,
>> November 1990
>>
>> [2] Jan Willem Klop, Vincent van Oostrom, and Roel de Vrijer
>> Lambda Calculus with Patterns
>> Theoretical Computer Science, Volume 398, Issues 1-3, 28 May 2008,
>> pages 16-31, Elsevier
>>
>> [3] Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori:
>> Pure patterns type systems. POPL 2003: 250-261
>>
>>
>> Quoting Michael Lienhardt <michael.lienhardt at inrialpes.fr>:
>>
>>> [ 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.
>>>
>>
>>
>>
>> ----------------------------------------------------------------
>> Este mensaje ha sido enviado utilizando IMP desde LIFIA.
>>
>
>
> --
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>

________________________________
Morten Rhiger
http://www.itu.dk/people/mir/