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
- the totality checker *may* need to track, at least, the set of required constraints of pattern synonyms mentioned in a COMPLETE pragma; and
- 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
comment:2 Changed 10 months ago by
Cc: | alanz bgamari RyanGlScott goldfire carter mpickering added |
---|---|
Keywords: | PatternMatchWarnings added |
comment:3 Changed 10 months ago by
Keywords: | PatternSynonyms added |
---|
comment:4 Changed 10 months ago by
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!
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 satisfiesHasSrcSpan
, hence checking the completeness of a matching onLL
does not need to consider types at all; all types matcha
andHasSrcSpan a
is already guaranteed to hold by the pattern synonym type checking. I might be wrong about this observation though.