> I'm afraid none of this is apparent from the User Guide -- and I even > contributed some material to the Guide, without ever understanding that. > Before this thread, I took it that 'Required' means for building -- as in for > smart constructors.
No, that's not what the required/provided distinction means at all! You should think of both Provided and Required in the context of matching, not in the context of building. To be able to use a pattern synonym to match on a scrutinee of type T, not only does T have to match the scrutinee type of the pattern synonym, but you also must satisfy the constraints of the Required constraints -- they are "required" to be able to use the pattern synonym. On the flipside, once you do use the pattern synonym, on the right-hand side of your matched clause you now get to assume the Provided constraints -- in other words, those constraints are "provided" to you by the pattern synonym. It is true that the builder could have entirely unrelated constraints to either (as in the proposal). The current implementation basically assumes that the Provided constraints can be provided because the builder put them in. Does this make it clearer? On Wed, Oct 6, 2021 at 10:13 AM Anthony Clayden <anthony.d.clay...@gmail.com> wrote: > > > Thank you. Yes that proposal seems in 'the same ball park'. As Richard's > already noted, a H98 data constructor can't _Provide_ any constraints, > because it has no dictionaries wrapped up inside. But I'm not asking it to! > > The current PatSyn signatures don't distinguish between Required-for-building > vs Required-for-matching (i.e. deconstructing/reformatting to the PatSyn). > This seems no better than 'stupid theta': I'm not asking for any reformatting > to pattern-match, just give me the darn components, they are what they are > where they are. > > I'm afraid none of this is apparent from the User Guide -- and I even > contributed some material to the Guide, without ever understanding that. > Before this thread, I took it that 'Required' means for building -- as in for > smart constructors. So PatSyns aren't really aimed to be for smart > constructors? I should take that material out of the User Guide? > > > AntC > > > On Wed, 6 Oct 2021 at 10:53, Richard Eisenberg <li...@richarde.dev> wrote: >> >> You're right -- my apologies. Here is the accepted proposal: >> https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-bidir-constr-sigs.rst >> >> Richard >> >> On Oct 5, 2021, at 12:38 PM, David Feuer <david.fe...@gmail.com> wrote: >> >> To be clear, the proposal to allow different constraints was accepted, but >> integrating it into the current, incredibly complex, code was well beyond >> the limited abilities of the one person who made an attempt. Totally >> severing pattern synonyms from constructor synonyms (giving them separate >> namespaces) would be a much simpler design. >> >> On Tue, Oct 5, 2021, 12:33 PM Richard Eisenberg <li...@richarde.dev> wrote: >>> >>> >>> >>> On Oct 3, 2021, at 5:38 AM, Anthony Clayden <anthony.d.clay...@gmail.com> >>> wrote: >>> >>> > pattern SmartConstr :: Ord a => () => ... >>> >>> Seems to mean: >>> >>> * Required constraint is Ord a -- fine, for building >>> >>> >>> Yes. >>> >>> * Provided constraint is Ord a -- why? for matching/consuming >>> >>> >>> No. Your signature specified that there are no provided constraints: that's >>> your (). >>> >>> >>> I'm using `SmartConstr` with some logic inside it to validate/build a >>> well-behaved data structure. But this is an ordinary H98 datatype, not a >>> GADT. >>> >>> >>> I believe there is no way to have provided constraints in Haskell98. You >>> would need either GADTs or higher-rank types. >>> >>> >>> This feels a lot like one of the things that's wrong with 'stupid theta' >>> datatype contexts. >>> >>> >>> You're onto something here. Required constraints are very much like the >>> stupid theta datatype contexts. But, unlike the stupid thetas, required >>> constraints are sometimes useful: they might be needed in order to, say, >>> call a function in a view pattern. >>> >>> For example: >>> >>> checkLT5AndReturn :: (Ord a, Num a) => a -> (Bool, a) >>> checkLT5AndReturn x = (x < 5, x) >>> >>> pattern LessThan5 :: (Ord a, Num a) => a -> a >>> pattern LessThan5 x <- ( checkLT5AndReturn -> (True, x) ) >>> >>> >>> My view pattern requires (Ord a, Num a), and so I must declare these as >>> required constraints in the pattern synonym type. Because vanilla data >>> constructors never do computation, any required constraints for data >>> constructors are always useless. >>> >>> >>> For definiteness, the use case is a underlying non-GADT constructor for a >>> BST >>> >>> > Node :: Tree a -> a -> Tree a -> Tree a >>> > >>> > pattern SmartNode :: Ord a => () => Tree a -> a -> Tree a -> Tree a >>> >>> with the usual semantics that the left Tree holds elements less than this >>> node. Note it's the same `a` with the same `Ord a` 'all the way down' the >>> Tree. >>> >>> >>> Does SmartNode need Ord a to match? Or just to produce a node? It seems >>> that Ord a is used only for production, not for matching. This suggests >>> that you want a separate smartNode function (not a pattern synonym) and to >>> have no constraints on the pattern synonym, which can be unidirectional >>> (that is, work only as a pattern, not as an expression). >>> >>> It has been mooted to allow pattern synonyms to have two types: one when >>> used as a pattern and a different one when used as an expression. That >>> might work for you here: you want SmartNode to have no constraints as a >>> pattern, but an Ord a constraint as an expression. At the time, the design >>> with two types was considered too complicated and abandoned. >>> >>> Does this help? >>> >>> Richard >>> _______________________________________________ >>> Glasgow-haskell-users mailing list >>> Glasgow-haskell-users@haskell.org >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users >> >> > _______________________________________________ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
