Functional Pearl: Type-safe pattern combinators

Functional Pearl: Type-safe pattern combinators, by Morten Rhiger:

Macros still have not made their way into typed higher-order programming languages such as Haskell and Standard ML. Therefore, to extend the expressiveness of Haskell or Standard ML gradually, one must express new linguistic features in terms of functions that fit within the static type systems of these languages. This is particularly challenging when introducing features that span across multiple types and that bind variables. We address this challenge by developing, in a step-by-step manner, mechanisms for encoding patterns and pattern matching in Haskell in a type-safe way.

This approach relies on continuation-passing style for a full encoding of pattern matching. Tullsen's First-Class Patterns relies on a monadic encoding of pattern matching to achieve abstraction over patterns. Given the relationship between CPS and monads, the two approaches likely share an underlying structure.

Abstracting over patterns yields a whole new level of abstraction, which could significantly improve code reuse. The only concern is compiling these more flexible structures to the same efficient pattern matching code we get when the language natively supports patterns. Section 4.9 discusses the efficiency concerns, and suggests that partial evaluation can completely eliminate the overhead.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

CPS and monads

Could someone give me some pointers to the topic, relationship between CPS and Monads?

"Representing monads"

You can check out section 2 of Filinski's Representing Monads.

See also, Compiling with

See also Compiling with Continuations, Continued, which discusses the relationship between monadic and CPS intermediate forms.

Nice

Definitely nice, although, honestly, I fail to see this as revolutionary.

All the basic ideas in the paper have been around for ages. The use of CPS for implementing pattern matching is just standard. Encoding type/value structure with combinators is an ancient idea (as pointed out in the paper). Even the idea of creating a flattened heterogeneous list of values for binding values is old. For example, a page I wrote for the MLton wiki similarly uses an example that generates a kind of heterogeneous list of results for binding values (and it similarly generalizes to disjunctions when you have a monad with plus). (The only reason it uses an infix product type rather than curried cps is that the former is syntactically lighter weight in SML (fn x & y & z => ... vs fn x => fn y => fn z => ...).)

One feature that the technique lacks is exhaustiveness checking.

Programming with Recursion Schemes is also related in intent.

One feature that the

One feature that the technique lacks is exhaustiveness checking.

Do you mean the statically typed pattern matching as presented in this paper is not exhaustive, or that the scheme you used in MLTon is not exhaustive?

Exhaustiveness checking

I mean that the combinator approach described in the paper does not perform exhaustiveness checking.

Right, exhaustiveness

Right, exhaustiveness checking was what I was referring to. I had thought that the monadic approach enforced exhaustiveness via the return type of the pattern matching function (as long as it's not a monad), but section 8.1 says he didn't attempt to make patterns statically checkable for exhaustiveness. I must be missing something.

Exhaustiveness checking

If you make patterns first class values of a language, [static] exhaustiveness checking (can one differentiate between all values with a set of given patterns) becomes undecidable.

Template Haskell

http://www.haskell.org/th/

Nicer types for Type-safe

hallelujiah

super hooray for people who fight the good fight for UX/usability.