Opened 10 months ago

Last modified 9 months ago

#15885 new task

Enhancing COMPLETE pragma to support pattern synonyms with polymorphic (output) types

Reported by: Shayan-Najd Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.6.2
Keywords: PatternMatchWarnings, PatternSynonyms Cc: alanz, bgamari, RyanGlScott, goldfire, carter, mpickering
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

On our work on the new front-end AST for GHC based on TTG, we would like to use a pattern synonym similar to the following:

pattern LL :: HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a
pattern LL s m <- (decomposeSrcSpan -> (m , s))
  where
        LL s m =  composeSrcSpan (m , s)

We know that any match on LL patterns, makes the pattern matching total, as it uses a view pattern with a total output pattern (i.e., in decomposeSrcSpan -> (m , s), the pattern (m , s) is total).

As far as I understand, currently COMPLETE pragmas cannot be used with such a polymorphic pattern synonym. I believe we need to enhance COMPLETE pragmas to support such pattern synonyms.

This can be done either syntactically, or (preferably) type-directed.

For example, we should be able to write {-# COMPLETE LL #-} or {-# COMPLETE LL :: HasSrcSpan a => a #-}.

In the type-directed approach

  1. the totality checker *may* need to track, at least, the set of required constraints of pattern synonyms mentioned in a COMPLETE pragma; and
  2. the order of pattern synonyms mentioned in a pragma should be taken into account (as noted by @carter).

For example, in the case of LL, HasSrcSpan a is a required type constraint.

Change History (6)

comment:1 Changed 10 months ago by Shayan-Najd

It is worth mentioning that the combination of the ordered set of pattern synonym names in the pragma and the type of the pattern synonyms themselves often guarantees abstraction (currently, I don't know of any situation that does not): the pattern matching totality checker does not need to know the implementation details of pattern synonyms (e.g., such details can be omitted from the interface files). I noticed the required type constraints guarantee that a pattern synonym mentioned in a COMPLETE ordered set is always used in a setting where, well, the required constraints hold. This fact immediately implies that, for example in {-# COMPLETE LL :: HasSrcSpan a => a #-}, a always satisfies HasSrcSpan, hence checking the completeness of a matching on LL does not need to consider types at all; all types match a and HasSrcSpan a is already guaranteed to hold by the pattern synonym type checking. I might be wrong about this observation though.

comment:2 Changed 10 months ago by Shayan-Najd

Cc: alanz bgamari RyanGlScott goldfire carter mpickering added
Keywords: PatternMatchWarnings added

comment:3 Changed 10 months ago by RyanGlScott

Keywords: PatternSynonyms added

comment:4 Changed 10 months ago by carter

reproducing my remarks from email

off hand, once we're in in viewpattern/ pattern synonym land, ORDER of the abstracted constructors matters!

consider

foo,bar,baz,quux,boom :: Nat -> String

plus some pattern synonyms i name "PowerOfTwo", "Even" and "Odd"

foo (PowerOfTwo x) = "power of two"
foo (Even x) = "even"
foo (Odd x) = "odd"

bar (Even x) = "even"
bar (Odd x) = "odd"

baz (PowerOfTwo x) = "power of two"
baz (Odd x) = "odd"

quux (Even x) = "even"
quux (Odd x) = "odd"
quux (PowerOfTwo) = "power of two"

boom (Even x) = "even"
boom (PowerOfTwo x) = "power of two"
boom (Odd x) = "odd"

foo and bar are both total definitions with unambiguous meanings, even though bar's patterns are a suffix of foos! baz is partial!

both boom and quux have a redudant overlapping case, power of two!

so some thoughts

1) order matters! 2) pattern synonyms at type T are part of an infinite lattice, Top element == accept everything, Bottom element = reject everything

3) PowerOfTwo <= Even in the Lattice of patterns for Natural, both are "incomparable" with Odd

4)

for a simple case on a single  value  at type T, assume c1 <= c2
                     , then  if   c1 x -> ... is before c2 x -> in the cases, 
                    then both are useful/computationally meaningful / not irrelevant
                    OTHERWISE
                      when its  roughly
                  case x :: T of 
                         c2 x -> ...
                         c1 x -> ...
then the 'c1 x'  is redundant

this is slightly orthogonal to other facets of this discussion so far, but i realized that Richard's Set of Sets of patterns model misses some useful/ meaningful examples/extra structure from a) the implicit lattice of different patterns possibly being super/subsets (which is still something of an approximation, but with these example I shared above I hope i've sketched out some motivation ) b) we can possibly model HOW ordering of clauses impacts coverage/totality / redundancy of clauses

I'm not sure if it'd be pleasant/good from a user experience perspective to have this sort of partial ordering modelling stuff, but certainly seems like it would help distinguish some useful examples where the program meaning / coverage is sensitive to clause ordering

i can try to spell this out more if theres interest, but I wanted to share while the iron was hot

best!

comment:5 Changed 10 months ago by goldfire

I think this would have to be a ghc-proposal, no?

comment:6 Changed 9 months ago by bgamari

Milestone: 8.6.3

Ticket retargeted after milestone closed

Note: See TracTickets for help on using tickets.