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 <[email protected]> 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:[email protected]] 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 > | [email protected] > | http://www.haskell.org/mailman/listinfo/ghc-devs > _______________________________________________ > ghc-devs mailing list > [email protected] > http://www.haskell.org/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-devs
