define-metafunction does not check type signature on LHS

[digama0]

#lang racket
(require redex)

(define-language A (N ::= 0 1 2))

(define-metafunction A
  flip : N -> N
  [(flip 1) ()]
  [(flip ()) 1])

(term (flip 1))
; flip: codomain test failed for (), call was (flip 1) [,bt for context]
(term (flip ()))
; flip: (flip ()) is not in my domain [,bt for context]

Ideally, the clauses in the definition of flip would be rejected because () does not match the grammar N, so they can never be used correctly. Checking #:pre and #:post conditions would also be great, but I'm not sure this is possible. (Also I wouldn't be too surprised if it is possible to write expressions that can't be typechecked at function declaration time, but there are lots of examples like this one where the pattern definitely has empty intersection with the grammar, so an error message seems warranted.)

[rfindler]

Thanks for the interest in Redex!

Unfortunately, the signatures on metafunctions (and similar things in other places) aren't something that redex can reason about statically in a definitive manner. That is, redex currently can only checks that a particular term matches a pattern, not the relationship between two patterns.

I suppose it would be possible, when discovering that flip is called with a value that doesn't match N to still check it against all left-hand sides and see if any of those do match, but I think that this would be overly restrictive (e.g., an "else" case might be written with the any pattern and that would be disallowed but is probably both used and useful).

In the fully general case, the question of what the relationship between two patterns (do they have an empty intersection, is one a subset of the other?) are not things that I know how to compute. If you have ideas on what such an algorithm would look like, I'd be interested! There is already some code (see the overlapping-patterns? helper function) for a related problem, namely determining if a pattern matches the same expression in two different ways, and a subproblem of that is determining if two patterns have a non-empty intersection (the problem you're asking for here). That code, however is approximate in the sense that it might say "yes there is an intersection" when there isn't really (if it says there isn't an intersection, then there really isn't one (modulo bugs)).

[digama0]

That overlapping-patterns? function sounds perfect for the job. I think it is fine to be an overapproximation here, since people are allowed to be loose with the pattern matching (e.g. any) and the main intent of this feature would be to catch typos in metafunctions (which are unfortunately very common when working with a big model).

I don't think it changes anything to check one LHS against all the other LHSs, since this is still a pattern-pattern check. My recommendation would be to check the LHSs against the function signature if provided, and otherwise just allow everything. Errors only occur if it is possible to prove that the function signature pattern has empty intersection with the LHS. (You can also do the same checks in RHSs, where clauses and probably many other places.)

The part I struggled with when poking around the code was whether it is possible to run this check at "compilation time" because it seems like define-language only really runs at run time so I'm not sure if it's possible to get the necessary pattern information. This is probably me just being new to racket and there isn't a problem though.

[rfindler]

Well, trying to use overlapping-patterns will quickly lead to an understanding of what's insufficient about it. 😄

The way Redex works, you'd extract all the patterns and turn them into the internal format of the patterns at compile time. But then it is probably simplest to do the actually checking when the metafunction definition is evaluated.

And just in the interest of clarity, I'm not sure this is something I'm really ready to take on as I don't see it as the major problem with redex currently, but it is also a non-trivial project.