New GHC feature proposal: Pattern families

[Simon Peyton Jones]

Baldur

(My name is Simon, not Peyton, incidentally.  "Peyton Jones" is my last name.)

I'm glad you are enjoying pattern synonyms. Thanks for identifying #9226, which I guess is you.

I honestly don't understand your pattern family proposal.  Would you like to write a wiki page somewhere describing the 
  syntax
  typing (static semantics)
  desugaring (dynamic semantics)
as clearly and precisely as you can, independent of prisms, and using the simplest possible examples to illustrate.  By all means say that prisms are a more advanced application, and give examples to show how.  But in general to specify a language feature you need a lot more than a couple of examples!

Then you can ask GHC users what they think.

I have to say that I'm cautious about adding further features to pattern synonyms until we've gotten more user experience with what we have.  (Do you think the explicitly bidirectional stuff on the wiki page is important?  To me that seems like the first thing a user might stumble over.)

Incidentally, I'd really like to replace view patterns with https://ghc.haskell.org/trac/ghc/wiki/ViewPatternsAlternative, another thing that is awaiting cycles.

Copying ghc-devs for interest

Thanks

Simon



| -----Original Message-----
| From: Baldur Blöndal [mailto:baldurpet at gmail.com]
| Sent: 18 June 2014 04:31
| To: Simon Peyton Jones; gergo at erdi.hu
| Subject: New GHC feature proposal: Pattern families
| 
| Hello Peyton and Gergo,
| 
| I'm a master's student at Chalmers, a minor GHC contributor and have
| written about the pattern synonyms extension
| (https://www.fpcomplete.com/user/icelandj/Pattern%20synonyms) and
| included is a proposal for an extension I call “pattern families”
| allowing users to create patterns parameterized by an expression. I feel
| like patterns don't get nearly as much attention as the type system and
| this is my attempt to balance things out :)
| 
| I discussed the proposal with Edward Kmett who suggested an example with
| prisms and that I contact you two for comments. The syntax is still in
| flux.
| 
| Some motivating examples for your consideration.
| 
|     PRISM PATTERNS
| 
| Edward suggested a pattern to match a prism which would look like this:
| <edwardk> an example where you want it is if you want to use a pattern
| synonym to match a prism <edwardk> foo (Match _Left a) = ...
| [...]
| <edwardk> the example of a single pattern that can match every prism
| would be a nice example
| 
| which would be quite easy to implement:
| 
| | pattern Match prism a ← ((^? prism) → Just a)
| |
| | bar :: Either c (Either a b) → a
| | bar (Match (_Right._Left) a) = a
| | bar _ = error "Not a Right (Left ...)"
| 
| This can be used for any prism:
| | jsonBlob = "[{\"someObject\": {\"version\": [1,0,3]}}]"
| |
| | foo (Match (nth 0) (Match (key "someObject") (Match (key "version")
| (Match (nth 1) a)))) = a
| | ghci> foo jsonBlob
| | Number 0.0
| 
| and defining more specilized patterns we can make it terser:
| | pattern Get i a ← ((^? nth i) → Just a) pattern Key str a ← ((^? key
| | str) → Just a)
| |
| | baz (Get 0 (Key "someObject" (Key "version" (Get 1 a)))) = a baz (0
| | `Get` "someObject" `Key` "version" `Key` 1 `Get` a) = a baz (a :→
| | "someObject" :⇒ "version" :⇒ 1 :→ a) = a
| where
| | pattern i   :→ a ← Get i a
| | pattern str :⇒ a ← Key str a
| 
| So this is excellent for pattern matching on any sort of nested
| structure: records, JSON, XML, HTML, ASTs, … Since this also supports
| pattern matching on any value that satisfies a predicate.
| 
|     N+K PATTERNS
| Generalizing n+k patterns: We create a pattern family indexed by its
| first argument:
| 
| | pattern (a :+) :: Num a ⇒ a → a
| |               k :+ n ← (unSucc k → Just n) -- [1] unSucc defined below
| 
| where (a :+) indicates that 'k' is an index of the pattern family
| allowing it to be supplied to the view pattern.
| The pattern can be used as follows:
| | fact 0          = 1
| | fact m@(1 :+ n) = m * fact n
| 
|     PATTERN MATCHING REGULAR EXPRESSIONS The pattern (:=~) is inspired
| by the operator (=~) from Text.Regex.Posix.Wrap (regex-posix), note that
| its second argument is the index here:
| | pattern (:=~ String) :: RegexContext Regex a c ⇒ a → c
| |               n :=~ pattern ← ((=~ pattern) → n)
| 
| Used as:
| | vowels :: RegexContext Regex src tgt ⇒ src → tgt vowels (n :=~
| | "[aeiou]") = n
| |
| | ghci> vowels "honorificabilitudinitatibus" ∷ Int
| | 13
| 
| where you can of course pattern match on the resulting value:
| 
| | has5Vowels :: String → Int
| | has5Vowels (5 :=~ "[aeiou]") = True
| | has5Voewls _                         = False
| 
|     TYPE INFERENCE
| Here is an example of a snippet inferring the type of an if expression:
| 
| | infer Γ (If cond t e) =
| |   case (infer Γ cond, infer Γ t, infer Γ e) of
| |     (Just TBool, Just τ₁, Just τ₂)
| |       | τ₁ == τ₂ = Just t₁
| 
| Here is how it might look with pattern families:
| 
| | infer Γ (If (Infer Γ TBool) (Infer Γ τ₁) (Infer Γ τ₂))
| |   | τ₁ == τ₂ = Just τ₁
| 
| (or even nicer if we use (:⇑) = Infer)
| | infer Γ (If (Γ :⇑ TBool) (Γ :⇑ τ₁) (Γ :⇑ τ₂)) …
| 
|     IMPLEMENTATION
| From what I can see this is a relatively straight-forward translation
| into view patterns where a variable bound by a view pattern is an
| “index” to the pattern family and unbound variables are regular
| patterns. In the examples above I use special syntax for the index where
| the type is included but even without any annotation it can be inferred
| from context.
| 
| If the proposal is fine by you I offer to do the implementation work,
| all feedback welcome!
| 
| Best regards,
| Baldur Blöndal
| 
|     APPENDIX
| | unSucc :: Int → Int → Maybe Int
| | unSucc k n
| |     | n - k < 0   = Nothing
| |     | otherwise = Just (n - k)
| |