active patterns

Stream: lean4

[Edward Ayers]

I'm playing with Lean syntax and I was wondering whether you can define your own 'active patterns' like in F#.

There are a few variants, but essentially an active pattern is a function myPattern : A → Option Nat (with some special attribute or syntax to say that this should be treated as a pattern). Then in your match statements you can write:

def myFunc : A → Nat × Nat
  | myPattern b => (b,b)
  | _ => (0,0)

which gets compiled to something like

def myFunc' (a : A) :=
  match myPattern a with
  | some b => (b,b)
  | none => (0,0)

This came up because I was playing with rolling my own json syntax and I wanted to implement some fancy 'spread' patterns like in raw javascript:

def getlemon : Json → Json
  |  jsonPattern% {"orange" : "juicy", "lemon" :  lemon, ...rest} => lemon
  | _ => panic! "bad fruits"

Perhaps there is a pattern syntax category that I can override and also some hooks in the equation compiler to do this?

[Henrik Böving]

@[matchPattern]
def Nat.myAdd := Nat.add

def foo : Nat → Nat
  | 0 => 1
  | Nat.myAdd n 1 => n

like this for example? (notice the matchpattern attribute) However I don't know how far you can go with just this

[Edward Ayers]

No an active pattern runs a user-defined function on the data being matched against first.

[Henrik Böving]

Hmmm, I think considering that we don't even support pattern guards right now it is rather unlikely you'll be able to get this active pattern thing to work either :/ but I might very well be wrong on that.

[Mario Carneiro]

As far as I know this is not possible without replacing the equation compiler itself and any syntaxes that call into it

[Mario Carneiro]

I think it would be nice to have an extension point like this: most likely it would be an elab for terms in pattern position, although I don't know what interface the equation compiler would present to such an elab

[Henrik Böving]

This would make exhaustivity checking quite hard though right?

[Mario Carneiro]

that depends on the interface. It could always be some kind of struct that has functions to answer all the questions that the equation compiler needs to ask about the notation, including exhaustiveness

[Mario Carneiro]

or it could be limited to things that either bind everything or act like pattern guards (i.e. have no effect on exhaustiveness checking), with anything that has to interact directly with exhaustiveness being handled by macro expansion to constructors

[Edward Ayers]

I think exhaustivity checking is ok, since an active pattern on a : α is always equivalent to a non-active match f a with ... for some f : α → β

[Edward Ayers]

(at least for total active patterns in the F# spec). You also have partial active patterns where f : α → Option β which seems ok too because it could be translated to a series of nested matches on options.

[Mario Carneiro]

I'm thinking a bit more generically than just active patterns; you could implement active patterns using elab stuff but this would also allow "tactics" in pattern position

[Mario Carneiro]

which allows things that can't be expressed as plain functions of the type system