GHC indecisive whether matching on GADT constructors in arrow notation is allowed
Alexis King
lexi.lambda at gmail.com
Tue Oct 5 19:03:15 UTC 2021
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.grenrus at 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.lambda at 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
>
> _______________________________________________
> ghc-devs mailing listghc-devs at haskell.orghttp://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20211005/b6b691d4/attachment.html>
More information about the ghc-devs
mailing list