Dependent pattern matching

[mikeday]

struct {
    tag: u32,
    data: F tag
}

Processing this struct often requires code like this:

match s.tag {
    val1 => { f1 s.data },
    val2 => { f2 s.data },
    _ => { ... }
}

However in order for this to type check, the type of s.data must be different in each branch of the match as it depends on s.tag, so matching the value of one field may refine the type of another.

Dependent pattern matching is a well-known concept that we do not currently support.

[brendanzab]

I've been trying to get my head around this one for Pikelet: Elaborating dependent (co)pattern matching (Fullt text PDF is available through that link - thanks ICFP). It's a bit intense!

[brendanzab]

Of course we may only need a subset of that paper to be useful for the DDL. But untangling which subset that is could be a little tricky.

[mikeday]

More resources!

Pattern Matching With Dependent Types http://www.cse.chalmers.se/~coquand/pattern.ps (Coquand's original paper on the subject from 1992)

Eliminating Dependent Pattern Matching http://cs.ru.nl/~james/RESEARCH/goguen2006.pdf (Goguen, McBride, McKinna compiling pattern matching to eliminators)

Pattern matching without K https://core.ac.uk/download/pdf/34616674.pdf (brief note showing subset of pattern matching that doesn't assume axiom K)

A New Elimination Rule for the Calculus of Inductive Constructions http://pauillac.inria.fr/~herbelin/articles/types-BarCorGreHerSac08-dep-matching.pdf (interesting?)

[mikeday]

The other consideration is that while any dependently typed proof assistant will require some form of dependent pattern matching, the DDL may not. An alternative approach would be to look to refinement types / liquid types and allow if expressions and match expressions to add to a constraint store that can be used to reduce types within the conditional branches and discharge proof obligations automatically.

Given that we may need something like this anyway for reasoning about array lengths and indices it could be worth giving this approach more thought.

[mikeday]

The original example is not actually dependent pattern matching, since the type of each match branch is the same:

match s.tag {
    val1 => { f1 s.data },
    val2 => { f2 s.data },
    _ => { ... }
}

Compiling this as written would require substituting any matched values (assuming they were fully bound) everywhere they occur in other typing contexts within each branch, but I don't know if that's something that is commonly done; it seems to require an additional set of substitutions attached to the typing context.

[brendanzab]

I think Flow and Typescript do something similar I think.

I think I was expecting to support something more like:

match tag {
    struct { tag = val1, data } => { f1 data },
    struct { tag = val2, data } => { f2 data },
    _ => { ... }
}

But it does kind of make sense to try to support matching on a projection.

Given that we may need something like [refinement types / liquid types] anyway for reasoning about array lengths and indices it could be worth giving this approach more thought.

Agreed that looking towards refinements might be handy. I'm thinking I'll push forward trying to learn non-dependent pattern matching for now, and we can either use that as a base for our constraint solving stuff, or as just 'training wheels' for me. 😆