Concrete syntax for pattern synonym type signatures

Wed Nov 5 07:04:46 UTC 2014

One note on the syntax front, 'pattern type' was mentioned as annoyingly
trying to shoehorn the word 'type' in to lean on an existing keyword, even
though its about a term level construction rather than a type level one.

We do have some perfectly serviceable keywords available to us that
indicate a more 'term/pattern' orientation, e.g. 'case' and 'of' come to
mind as things that are viable candidates for similar abuse here.

I'm just digging through the lexical lego bin for parts. I don't quite know
how to put them together to make a nice syntax though.

-Edward

On Tue, Nov 4, 2014 at 5:32 AM, Simon Peyton Jones <simonpj at microsoft.com>
wrote:

> Here is one principle: for GADTs, the pattern type signature should look
> like the GADT data constructor.  So if we have
>
>         data S a where
>         S1 :: p -> q -> S (p,q)
>         S2 :: ...blah...
>
>       pattern P x y = S1 x y
>
> then surely the signature for P should be
>         P :: p -> q -> S (p,q)
>
> The same goes for constraints in the constructor's type. Thus, using your
> example:
>
> |       data T a b where
> |         MkT :: (Eq a, Ord b, Show c) => a -> (b, b) -> c -> T a b
>
> If I say
>         pattern P x y z = MkT x y z
> then the signature for P should be identical to that of MkT.
>
>
> -----------
>
> It gets a bit more interesting when you have nested patterns that
> instantiate the type.  For example, with the same type T, consider
>
>         pattern P x y z = MkT (x,y) (False,True) [z]
>
> the "right" signature for P must presumably be
>         P :: (Eq (p,q), Show [r]) => p -> q -> r -> T (p,q) Bool
>
> We don't need to distinguish 'r' as existential, any more than we do in
> the original signature for MkT.
>
> Note that we must retain the instantiated but un-simplified constraints
> (Eq (p,b), Show [r]), because when pattern-matching against P, those are
> the constraints brought into scope.
>
> ---------
>
> The general story, for both data constructors and pattern synonyms, is
> that if the type is
>         D :: forall abc. (C1, C2...) => blah
> then the constraints (C1, C2...) are
>  - *required* when using D in an expression,
>  - *provided* (i.e. brought into scope) pattern matching against D.
>
> The tricky case comes when the pattern synonym involves some constraints
> that are *required* during *pattern-matching*.  A simple example is
>
>         pattern P1 x = (8, x)
>
> Here we *require* a (Num a) dictionary *both* when using P1 in an
> expression (to build the value 8), *and* when using P in pattern matching
> (to build a value 8 to compare with the value being matched).  I'll call
> the constraints that are *required* when matching the "match-required
> constraints".
>
> The same happens for view patterns:
>
>       gr :: Ord a => a -> a -> Maybe a
>         gr v x | x > v = Just v
>              | otherwise = Nothing
>
>         pattern P2 x = (gr 8 -> Just x)
>
> Here, (Ord a, Num a) are match-required.  (P2 is uni-directional, so we
> can't use P2 in expressions.)
>
> We can't give a signature to P1 like this
>         P1 :: forall a. Num a => b -> (a,b)
> because that looks as if (Num a) would be *provided* when pattern matching
> (see "general story" above), whereas actually it is required.  This is the
> nub of the problem Gergo is presenting us with.
>
> Notice that P1 is bidirectional, and can be used in expressions, where
> again we *require* (Num a), so P1's "term type" really is something like
> (Num a) => b -> (a,b).
>
> The more I think about this, the more I think we'll just have to bite the
> bullet and adapt the syntax for constraints in pattern types, to
> distinguish the match-required and match-provided parts. Suppose we let
> pattern signatures look like this:
>
>   pattern P :: forall tvs. (match-provided ; match-required) => tau
>
> The "; match-required" part is optional, and the "match-provided" part
> might be empty.  So P1 and P2 would look like this:
>
>   pattern P1 :: forall a. (; Num a) => b -> (a,b)
>   pattern P2 :: forall a. (; Num a, Ord a) => a -> a
>
> Because the "match-required" part is optional (and relatively rare) the
> common case looks just like an ordinary data constructor.
>
>
> None of this addresses the bidirectional/unidirectional question, but
> that's a pretty separate matter.
>
> Simon
>
> |  -----Original Message-----
> |  From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Dr.
> |  ERDI Gergo
> |  Sent: 03 November 2014 10:13
> |  To: GHC Devs
> |  Subject: RFC: Concrete syntax for pattern synonym type signatures
> |
> |  Background
> |  ----------
> |
> |  As explained on
> |  https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms#Staticsemantics
> |  the type of a pattern synonym can be fully described with the
> |  following pieces of information:
> |
> |  * If the pattern synonym is bidirectional
> |  * Universially-bound type variables, and required constraints on them
> |  * The type of the pattern itself, closed over the universially-bound
> |  type variables
> |  * Existentially-bound type variables, and the constraints provided by
> |  them
> |  * The types of the arguments, closed over the universially and
> |     existentially bound type variables
> |
> |  Here's an example showing all of these axes in action:
> |
> |       data T a b where
> |         MkT :: (Eq a, Ord b, Show c) => a -> (b, b) -> c -> T a b
> |
> |       pattern P x y = MkT 5 (y, True) x
> |
> |  In this case:
> |
> |  * The name of the pattern synonym is `P`
> |  * The pattern synonym is bidirectional
> |  * The universially-bound tyvars/required constraints are `forall a.
> |  Num a`
> |  * The type of the pattern is `T a Bool`
> |  * The existentially-bound tyvars/provided constraints are
> |     `forall c. (Eq a, Ord Bool, Show c)`
> |  * The type of the arguments are `c` and `Bool`.
> |
> |  The problem, then, is finding a concrete syntax that captures all of
> |  this information. This syntax is needed for at least two purposes:
> |
> |  * Showing pattern synonym type information in Haddock/GHCi
> |  * Pattern synonym type signatures (#8584)
> |
> |  Current state of things
> |  -----------------------
> |
> |  GHCi 7.8.3 shows the type above as:
> |
> |  pattern (Eq t, Ord Bool, Show c) => P c Bool :: Num t => (T t Bool)
> |
> |  Not only does it not show directionality, I think this is very
> |  confusing in every other way as well, especially with explicit
> |  foralls:
> |
> |  pattern forall c. (Eq t, Ord Bool, Show c) => P c Bool :: forall t.
> |  Num t => (T t Bool)
> |
> |  I am currently working on implementing #8584, which means I need to
> |  parse these type signatures. I managed to get the above monstrosity to
> |  parse (unambigiously from actual pattern synonym definitions) by
> |  throwing in an extra 'type' keyword:
> |
> |  pattern type (Eq t, Ord Bool, Show c) => P c Bool :: Num t => (T t
> |  Bool)
> |
> |  Request for help
> |  ----------------
> |
> |  Surely we can do better than that! So let's come up with a nice syntax
> |  for pattern synonym type signatures. It will be used in the pattern
> |  synonym type signature annotations of GHC 7.10, and we could also
> |  retrofit it into GHC 7.8.4 and its Haddock, so that documentation
> |  generated with today's tools will look consistent with code you will
> |  be able to enter in tomorrow's version.
> |
> |  Bye,
> |       Gergo
> |  _______________________________________________
> |  ghc-devs mailing list
> |  ghc-devs at haskell.org
> |  http://www.haskell.org/mailman/listinfo/ghc-devs
> _______________________________________________
> 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/20141105/a39698d4/attachment.html>