[GHC] #15885: Enhancing COMPLETE pragma to support pattern synonyms with polymorphic (output) types
#15885: Enhancing COMPLETE pragma to support pattern synonyms with polymorphic (output) types -------------------------------------+------------------------------------- Reporter: Shayan-Najd | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- On our work on the [https://ghc.haskell.org/trac/ghc/wiki/ImplementingTreesThatGrow new front-end AST for GHC] based on [https://ghc.haskell.org/trac/ghc/wiki/ImplementingTreesThatGrow/TreesThatGro... TTG], we would like to use [https://ghc.haskell.org/trac/ghc/wiki/ImplementingTreesThatGrow/HandlingSour... a pattern synonym] similar to the following: {{{#!hs 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 a. the totality checker *may* need to track, at least, the set of required constraints of pattern synonyms mentioned in a COMPLETE pragma; and b. 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15885 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15885: Enhancing COMPLETE pragma to support pattern synonyms with polymorphic (output) types -------------------------------------+------------------------------------- Reporter: Shayan-Najd | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15885#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15885: Enhancing COMPLETE pragma to support pattern synonyms with polymorphic (output) types -------------------------------------+------------------------------------- Reporter: Shayan-Najd | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Shayan-Najd): * keywords: => PatternMatchWarnings * cc: alanz, bgamari, RyanGlScott, goldfire, carter, mpickering (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15885#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15885: Enhancing COMPLETE pragma to support pattern synonyms with polymorphic (output) types -------------------------------------+------------------------------------- Reporter: Shayan-Najd | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: | PatternMatchWarnings, | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: PatternMatchWarnings => PatternMatchWarnings, PatternSynonyms -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15885#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15885: Enhancing COMPLETE pragma to support pattern synonyms with polymorphic (output) types -------------------------------------+------------------------------------- Reporter: Shayan-Najd | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: | PatternMatchWarnings, | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15885#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15885: Enhancing COMPLETE pragma to support pattern synonyms with polymorphic (output) types -------------------------------------+------------------------------------- Reporter: Shayan-Najd | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: | PatternMatchWarnings, | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I think this would have to be a [https://github.com/ghc-proposals/ghc- proposals ghc-proposal], no? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15885#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC