<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>A simple desugaring example may illustrate:<br>
<br>
{-# LANGUAGE Arrows, GADTs #-}<br>
<br>
import Control.Arrow<br>
<br>
data X a where<br>
X :: Bool -> Int -> X (Bool, Int)<br>
<br>
ex1 :: Arrow a => a (X x) (Int, Bool)<br>
ex1 = proc (X b i) -> returnA -< (i, b)<br>
<br>
ex1expl :: Arrow a => a (X x) (Int, Bool)<br>
ex1expl =<br>
arr f >>> -- pattern match<br>
arr g >>> -- expression<br>
returnA <br>
where<br>
f :: X a -> (Bool, Int)<br>
f (X b i) = (b, i)<br>
<br>
g :: (Bool, Int) -> (Int, Bool)<br>
g (b, i) = (i, b)<br>
<br>
If we want to desugar Alexis' example<br>
<br>
data T where<br>
T :: a -> T<br>
<br>
panic :: (Arrow arrow) => arrow T T<br>
panic = proc (T x) -> do returnA -< T x<br>
<br>
which has the same shape, what would the type of `f` be?<br>
<br>
f :: T -> a -- doesn't work<br>
<br>
If we had sigmas, i.e. dependent pairs and type level lambdas, we
could have<br>
<br>
f :: T -> Sigma Type (\a -> a) -- a pair like (Bool,
Int) but fancier<br>
<br>
i.e. the explicit desugaring could look like<br>
<br>
panicExplicit :: (Arrow arrow) => arrow T T<br>
panicExplicit =<br>
arr f >>><br>
arr g >>><br>
returnA<br>
where<br>
f :: T -> Sigma Type (\a -> a)<br>
f (T @a x) = (@a, x)<br>
<br>
g :: Sigma Type (\a -> a)<br>
g (@a, x) = T @a x<br>
<br>
My gut feeling says that the original arrow desugaring would just
work,<br>
but instead of tuples for context, we'd need to use telescopes.<br>
Not that earth-shattering of a generalization.<br>
<br>
The evidence could be explicitly bound already today,<br>
but I guess it's not, and simply thrown away:<br>
<br>
{-# LANGUAGE Arrows, GADTs, ConstraintKinds #-}<br>
<br>
import Control.Arrow<br>
<br>
data Showable a where<br>
Showable :: Show a => a -> Showable a<br>
<br>
data Dict c where<br>
Dict :: c => Dict c<br>
<br>
ex2explicit :: Arrow a => a (Showable x) (Showable x)<br>
ex2explicit =<br>
arr f >>> -- pattern match<br>
arr g >>> -- expression<br>
returnA <br>
where<br>
f :: Showable x -> (x, Dict (Show x))<br>
f (Showable x) = (x, Dict)<br>
<br>
g :: (x, Dict (Show x)) -> Showable x<br>
g (x, Dict) = Showable x<br>
<br>
The<br>
<br>
ex2 :: Arrow a => a (Showable x) (Showable x)<br>
ex2 = proc (Showable x) -> returnA -< Showable x <br>
<br>
works today, surprisingly. Looks like GHC does something as above,<br>
if I read the -ddump-ds output correctly:<br>
<br>
ex2<br>
:: forall (a :: * -> * -> *) x.<br>
Arrow a =><br>
a (Showable x) (Showable x)<br>
[LclIdX]<br>
ex2<br>
= \ (@ (a_a2ja :: * -> * -> *))<br>
(@ x_a2jb)<br>
($dArrow_a2jd :: Arrow a_a2ja) -><br>
break<1>()<br>
let {<br>
arr' :: forall b c. (b -> c) -> a_a2ja b c<br>
[LclId]<br>
arr' = arr @ a_a2ja $dArrow_a2jm } in<br>
let {<br>
(>>>>) :: forall a b c. a_a2ja a b ->
a_a2ja b c -> a_a2ja a c<br>
[LclId]<br>
(>>>>) = GHC.Desugar.>>> @ a_a2ja
$dArrow_a2jn } in<br>
(>>>>)<br>
@ (Showable x_a2jb)<br>
@ ((Show x_a2jb, x_a2jb), ())<br>
@ (Showable x_a2jb)<br>
(arr'<br>
@ (Showable x_a2jb)<br>
@ ((Show x_a2jb, x_a2jb), ()) -- this is
interesting<br>
(\ (ds_d2kY :: Showable x_a2jb) -><br>
case ds_d2kY of { Showable $dShow_a2je x_a2hL
-><br>
(($dShow_a2je, x_a2hL),
ghc-prim-0.5.3:GHC.Tuple.())<br>
}))<br>
((>>>>)<br>
@ ((Show x_a2jb, x_a2jb), ())<br>
@ (Showable x_a2jb)<br>
@ (Showable x_a2jb)<br>
(arr'<br>
@ ((Show x_a2jb, x_a2jb), ())<br>
@ (Showable x_a2jb)<br>
(\ (ds_d2kX :: ((Show x_a2jb, x_a2jb), ()))
-><br>
case ds_d2kX of { (ds_d2kW, _ [Occ=Dead])
-><br>
case ds_d2kW of { ($dShow_a2jl, x_a2hL) -><br>
break<0>() Main.Showable @ x_a2jb
$dShow_a2jl x_a2hL<br>
}<br>
}))<br>
(returnA @ a_a2ja @ (Showable x_a2jb)
$dArrow_a2jd))<br>
<br>
- Oleg<br>
<br>
</p>
<div class="moz-cite-prefix">On 5.10.2021 19.12, Richard Eisenberg
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:010f017c513ab5a2-63ed4ac9-6a34-4499-820d-113f462ea5da-000000@us-east-2.amazonses.com">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
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.
<div class=""><br class="">
</div>
<div class="">Richard<br class="">
<div><br class="">
<blockquote type="cite" class="">
<div class="">On Oct 3, 2021, at 12:19 PM, Alexis King <<a
href="mailto:lexi.lambda@gmail.com" class=""
moz-do-not-send="true">lexi.lambda@gmail.com</a>>
wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<div dir="ltr" class="">
<p class="">Hi,</p>
<p class="">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. <code class="">Note [Arrows and
patterns]</code> in <code class="">GHC.Tc.Gen.Pat</code>
suggests they aren’t supposed to be supported at all,
which is what I would essentially expect. But issues <a
href="https://gitlab.haskell.org/ghc/ghc/-/issues/17423" class=""
moz-do-not-send="true">#17423</a> and <a
href="https://gitlab.haskell.org/ghc/ghc/-/issues/18950"
class="" moz-do-not-send="true">#18950</a> provide
examples of using GADT constructors in arrow notation,
and there seems to be some expectation that in fact
they <em class="">ought</em> to be supported, and
some recently-added test cases verify that’s the case.</p>
<p class="">But this is quite odd, because it means the
arrows test suite now includes test cases that verify
both that this is supported <em class="">and</em>
that it isn’t… and all of them pass! Here’s my
understanding of the status quo:</p>
<ul class="">
<li class="">
<p class="">Matching on constructors that bind bona
fide existential variables is not allowed, and
this is verified by the <code class="">arrowfail004</code>
test case, which involves the following program:</p>
<pre class=""><code class="">data T = forall a. T a
panic :: (Arrow arrow) => arrow T T
panic = proc (T x) -> do returnA -< T x</code></pre>
<p class="">This program is rejected with the
following error message:</p>
<pre class=""><code class="">arrowfail004.hs:12:15:
Proc patterns cannot use existential or GADT data constructors
In the pattern: T x</code></pre>
</li>
<li class="">
<p class="">Despite the previous point, matching on
constructors that bind evidence is allowed. This
is enshrined in test cases <code class="">T15175</code>,
<code class="">T17423</code>, and <code class="">T18950</code>,
which match on constructors like these:</p>
<pre class=""><code class="">data DecoType a where
DecoBool :: Maybe (String, String) -> Maybe (Int, Int) -> DecoType Bool
data Point a where
Point :: RealFloat a => a -> Point a</code></pre>
</li>
</ul>
<p class="">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 <code class="">arrowfail004</code> seems
rather misleading, since I would definitely call <code
class="">DecoBool</code> and <code class="">Point</code>
above “GADT data constructors”.</p>
<p class="">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.)</p>
<p class="">Thanks,<br class="">
Alexis</p>
</div>
_______________________________________________<br
class="">
ghc-devs mailing list<br class="">
<a href="mailto:ghc-devs@haskell.org" class=""
moz-do-not-send="true">ghc-devs@haskell.org</a><br
class="">
<a class="moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br
class="">
</div>
</blockquote>
</div>
<br class="">
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
ghc-devs mailing list
<a class="moz-txt-link-abbreviated" href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a>
<a class="moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a>
</pre>
</blockquote>
</body>
</html>