Concrete syntax for pattern synonym type signatures

[Simon Peyton Jones]

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