<CReq> must be the union of the constraints required to match the pattern, 
_plus_ required to build with the pattern -- if it is bidirectional.
I think that is confusing too!  How about this:

  *   ⟨CReq⟩ are the constraints required to match the pattern, in a pattern 
match.
  *   ⟨CProv⟩ are the constraints made available (provided) by a successful 
pattern match.
  *   <CReq> and <CProv> are both required when P is used as a constructor in 
an expression.
That makes the constructor form explicit.
The only mechanism for getting the constraints needed for building is by 
polluting the constraints needed for matching.
Yes I agree that’s bad. It is acknowledge as such in the paper, and is the 
subject of accepted proposal #42.

Simon

PS: I am leaving Microsoft at the end of November 2021, at which point 
simo...@microsoft.com<mailto:simo...@microsoft.com> will cease to work.  Use 
simon.peytonjo...@gmail.com<mailto:simon.peytonjo...@gmail.com> instead.  (For 
now, it just forwards to simo...@microsoft.com.)

From: Anthony Clayden <anthony.d.clay...@gmail.com>
Sent: 06 October 2021 11:42
To: Simon Peyton Jones <simo...@microsoft.com>
Cc: Gergő Érdi <ge...@erdi.hu>; GHC users <glasgow-haskell-users@haskell.org>
Subject: Re: Pattern synonym constraints :: Ord a => () => ...



On Wed, 6 Oct 2021 at 21:24, Simon Peyton Jones 
<simo...@microsoft.com<mailto:simo...@microsoft.com>> wrote:

I suggest the User Guide needs an example where a constraint needed for 
matching (presumably via a View pattern) is not amongst the constraints carried 
inside the data constructor, nor amongst those needed for building. Then the 
limitations in the current design would be more apparent for users.

The user 
manual<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fghc.gitlab.haskell.org%2Fghc%2Fdoc%2Fusers_guide%2Fexts%2Fpattern_synonyms.html%3Fhighlight%3Dpattern%2520syn%23typing-of-pattern-synonyms&data=04%7C01%7Csimonpj%40microsoft.com%7C941ec01fb46743eefb4d08d988b5e64a%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637691137569565464%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000&sdata=B7ZHX1fB5hRZkVuvId1OhnC6j5oYoqeSaD2hByBAPRM%3D&reserved=0>
 does already speak about the type of a builder, here:

...
   How could we make that clearer?

This point in that section of the Guide is wrong/misleading:


·         ⟨CReq⟩ are the constraints required to match the pattern.
<CReq> must be the union of the constraints required to match the pattern, 
_plus_ required to build with the pattern -- if it is bidirectional.


Then thank you Simon, but it's the type of the _matcher_ that's problematic. 
The only mechanism for getting the constraints needed for building is by 
polluting the constraints needed for matching. Here's a (crude, daft) example, 
using guards to 'raise' a required-for-failing-to-build that isn't 
required-for-successful-building nor for-matching

>    pattern TwoNode :: (Show a, Ord a) => () => a -> a -> Tree a             
> -- GHC insists on both constraints as Req'd
>
>    pattern TwoNode x y  <- Node Empty x (Leaf y)   where
>      TwoNode x y | x > y = Node Empty x (Leaf y)
>                  | otherwise = error (show x ++ " not greater " ++ show y)
To quote you from May 1999


>            But when you take a constructor *apart*, the invariant must hold

>            by construction: you couldn't have built the thing you are taking

>            apart unless invariant held.  So enforcing the invariant again is

>            redundant; and in addition it pollutes the type of selectors.


`Show a` must have "held by construction" of the `Node`. But the PatSyn's 
constraints are requiring more than that was true in some distant line of code: 
 it wants evidence  in the form of a dictionary at the point of deconstructing; 
since the build was successful, I ipso facto don't want to `show` anything in 
consuming it. An `instance Foldable Tree` has no mechanism to pass in any such 
dictionaries (which'll anyway be redundant, as you say).


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Reply via email to