I have already discussed this particular issue at some length in #20470 <https://gitlab.haskell.org/ghc/ghc/-/issues/20470>, and I propose a possible desugaring, using higher-rank lambdas to encode existential quantification, in a comment <https://gitlab.haskell.org/ghc/ghc/-/issues/20470#note_381045>. This is fine, since we only need to desugar to Core, not source Haskell.
Alexis On Tue, Oct 5, 2021 at 11:50 AM Oleg Grenrus <oleg.gren...@iki.fi> wrote: > A simple desugaring example may illustrate: > > {-# LANGUAGE Arrows, GADTs #-} > > import Control.Arrow > > data X a where > X :: Bool -> Int -> X (Bool, Int) > > ex1 :: Arrow a => a (X x) (Int, Bool) > ex1 = proc (X b i) -> returnA -< (i, b) > > ex1expl :: Arrow a => a (X x) (Int, Bool) > ex1expl = > arr f >>> -- pattern match > arr g >>> -- expression > returnA > where > f :: X a -> (Bool, Int) > f (X b i) = (b, i) > > g :: (Bool, Int) -> (Int, Bool) > g (b, i) = (i, b) > > If we want to desugar Alexis' example > > data T where > T :: a -> T > > panic :: (Arrow arrow) => arrow T T > panic = proc (T x) -> do returnA -< T x > > which has the same shape, what would the type of `f` be? > > f :: T -> a -- doesn't work > > If we had sigmas, i.e. dependent pairs and type level lambdas, we could > have > > f :: T -> Sigma Type (\a -> a) -- a pair like (Bool, Int) but fancier > > i.e. the explicit desugaring could look like > > panicExplicit :: (Arrow arrow) => arrow T T > panicExplicit = > arr f >>> > arr g >>> > returnA > where > f :: T -> Sigma Type (\a -> a) > f (T @a x) = (@a, x) > > g :: Sigma Type (\a -> a) > g (@a, x) = T @a x > > My gut feeling says that the original arrow desugaring would just work, > but instead of tuples for context, we'd need to use telescopes. > Not that earth-shattering of a generalization. > > The evidence could be explicitly bound already today, > but I guess it's not, and simply thrown away: > > {-# LANGUAGE Arrows, GADTs, ConstraintKinds #-} > > import Control.Arrow > > data Showable a where > Showable :: Show a => a -> Showable a > > data Dict c where > Dict :: c => Dict c > > ex2explicit :: Arrow a => a (Showable x) (Showable x) > ex2explicit = > arr f >>> -- pattern match > arr g >>> -- expression > returnA > where > f :: Showable x -> (x, Dict (Show x)) > f (Showable x) = (x, Dict) > > g :: (x, Dict (Show x)) -> Showable x > g (x, Dict) = Showable x > > The > > ex2 :: Arrow a => a (Showable x) (Showable x) > ex2 = proc (Showable x) -> returnA -< Showable x > > works today, surprisingly. Looks like GHC does something as above, > if I read the -ddump-ds output correctly: > > ex2 > :: forall (a :: * -> * -> *) x. > Arrow a => > a (Showable x) (Showable x) > [LclIdX] > ex2 > = \ (@ (a_a2ja :: * -> * -> *)) > (@ x_a2jb) > ($dArrow_a2jd :: Arrow a_a2ja) -> > break<1>() > let { > arr' :: forall b c. (b -> c) -> a_a2ja b c > [LclId] > arr' = arr @ a_a2ja $dArrow_a2jm } in > let { > (>>>>) :: forall a b c. a_a2ja a b -> a_a2ja b c -> a_a2ja a c > [LclId] > (>>>>) = GHC.Desugar.>>> @ a_a2ja $dArrow_a2jn } in > (>>>>) > @ (Showable x_a2jb) > @ ((Show x_a2jb, x_a2jb), ()) > @ (Showable x_a2jb) > (arr' > @ (Showable x_a2jb) > @ ((Show x_a2jb, x_a2jb), ()) -- this is interesting > (\ (ds_d2kY :: Showable x_a2jb) -> > case ds_d2kY of { Showable $dShow_a2je x_a2hL -> > (($dShow_a2je, x_a2hL), ghc-prim-0.5.3:GHC.Tuple.()) > })) > ((>>>>) > @ ((Show x_a2jb, x_a2jb), ()) > @ (Showable x_a2jb) > @ (Showable x_a2jb) > (arr' > @ ((Show x_a2jb, x_a2jb), ()) > @ (Showable x_a2jb) > (\ (ds_d2kX :: ((Show x_a2jb, x_a2jb), ())) -> > case ds_d2kX of { (ds_d2kW, _ [Occ=Dead]) -> > case ds_d2kW of { ($dShow_a2jl, x_a2hL) -> > break<0>() Main.Showable @ x_a2jb $dShow_a2jl x_a2hL > } > })) > (returnA @ a_a2ja @ (Showable x_a2jb) $dArrow_a2jd)) > > - Oleg > > On 5.10.2021 19.12, Richard Eisenberg wrote: > > I think the real difference is whether new type variables are brought into > scope. It seems that GHC can't deal with a proc-pattern-match that > introduces type variables, but it *can* deal with introduced constraints. I > have no idea *why* this is the case, but it seems a plausible (if > accidental) resting place for the implementation. > > Richard > > On Oct 3, 2021, at 12:19 PM, Alexis King <lexi.lam...@gmail.com> wrote: > > Hi, > > I’ve been working on bringing my reimplementation of arrow notation back > up to date, and I’ve run into some confusion about the extent to which > arrow notation is “supposed” to support matching on GADT constructors. Note > [Arrows and patterns] in GHC.Tc.Gen.Pat suggests they aren’t supposed to > be supported at all, which is what I would essentially expect. But issues > #17423 <https://gitlab.haskell.org/ghc/ghc/-/issues/17423> and #18950 > <https://gitlab.haskell.org/ghc/ghc/-/issues/18950> provide examples of > using GADT constructors in arrow notation, and there seems to be some > expectation that in fact they *ought* to be supported, and some > recently-added test cases verify that’s the case. > > But this is quite odd, because it means the arrows test suite now includes > test cases that verify both that this is supported *and* that it isn’t… > and all of them pass! Here’s my understanding of the status quo: > > - > > Matching on constructors that bind bona fide existential variables is > not allowed, and this is verified by the arrowfail004 test case, which > involves the following program: > > data T = forall a. T a > > panic :: (Arrow arrow) => arrow T T > panic = proc (T x) -> do returnA -< T x > > This program is rejected with the following error message: > > arrowfail004.hs:12:15: > Proc patterns cannot use existential or GADT data constructors > In the pattern: T x > > - > > Despite the previous point, matching on constructors that bind > evidence is allowed. This is enshrined in test cases T15175, T17423, > and T18950, which match on constructors like these: > > data DecoType a where > DecoBool :: Maybe (String, String) -> Maybe (Int, Int) -> DecoType Bool > data Point a where > Point :: RealFloat a => a -> Point a > > > This seems rather contradictory to me. I don’t think there’s much of a > meaningful distinction between these types of matches, as they create > precisely the same set of challenges from the Core point of view… right? > And even if I’m wrong, the error message in arrowfail004 seems rather > misleading, since I would definitely call DecoBool and Point above “GADT > data constructors”. > > So what’s the intended story here? Is matching on GADT constructors in > arrow notation supposed to be allowed or not? (I suspect this is really > just yet another case of “nobody really knows what’s ‘supposed’ to happen > with arrow notation,” but I figured I might as well ask out of hopefulness > that someone has some idea.) > > Thanks, > Alexis > _______________________________________________ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > > > _______________________________________________ > ghc-devs mailing > listghc-devs@haskell.orghttp://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > _______________________________________________ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs