If you haven't yet, it is probably a good idea to read section 6 of https://gergo.erdi.hu/papers/patsyns/2016-hs-patsyns-ext.pdf
On Wed, Oct 6, 2021 at 10:23 AM Gergő Érdi <ge...@erdi.hu> wrote: > > > 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
