New GHC feature proposal: Pattern families

[Edward Kmett]

The main thing Baldur had asked me about was if it makes sense to talk
about patterns that are parameterized by expressions in places.

I agree that the thought is very poorly fleshed out, but as a motivation,
in some sense the previous form of view patterns already do this.

Consider (->), which takes in an expression to apply on the left and a
pattern for what to match against the result of it on the right.

The question then becomes can we allow this for arbitrary patterns?

There are a number of use cases for these. For example,

A pattern to match a regular expression might look like

Foo (x :~= "ab*")

where you want "ab*" to be passed as a parameter to the code for the
pattern synonym (:~=), not be something it is binding.

This then speaks to needing some notion of mode for the different
parameters.

One of the reasons I'm under-excited about pattern synonyms is we already
built all the machinery for working with prisms in lens to generalize them.
=)

In lens we have a combinator 'preview :: Prism' s a -> s -> Maybe a'.

As a straw man proposal:

It'd be nice to be able to do something like

pattern (Match p a) <- (preview p -> Just a)

and have it take the arguments that go to the left hand side of the -> as
expressions, not patterns so that that can compile.

Now, I'm somewhat dubious that it worth the pain to embellish the pattern
language with something this complicated, but in some sense we already have
a lot of the machinery to support it. e.g. IIRC we parse patterns first as
expressions then convert them.

-Edward


On Mon, Jun 23, 2014 at 4:39 AM, Simon Peyton Jones <simonpj at microsoft.com>
wrote:

> 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)
> | |
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140623/fdd53e4b/attachment.html>