Sorry to barge into the discussion with neither much knowledge of the
theory nor the implementation. I tried to look at both, but my
understanding is severely lacking. However I do feel a tiny bit
emboldened because my own findings turned out to at least have the same
shadow as the contents of this more thorough overview.
The one part of the existing story I personally found the most promising
was to explore the category hierarchy around Arrows, in other words the
Gibbard/Trinkle perspective. Therefore I want to elaborate my own naive
findings a tiny bit. Bear in mind that much of this is gleaned from
experimental implementations or interpreted, but I do not have proofs,
or even theory.
Almost all parts necessary for an Arrow seem to already be contained in
a symmetrical braided category. Fascinatingly, even the braiding might
be superfluous in some cases, leaving only the need for a monoidal
category. But to get from a braided category to a full Arrow, there
seems to be a need for "constructors" like (arr $ \x -> (x,x)) and
"destructors" like (arr fst). There seem to be several options for
those, and a choice would have to be made. Notably: is introduction done
by duplicating existing values, or by introducing new "unit" values (for
a suitable definition of "unit")? That choice doesn't seem impactful,
but my gut feeling is that that's just because I cannot see the
potential points of impact.
What makes this story worse is that the currently known hierarchies
around ArrowChoice and ArrowLoop seem to be coarser still – although the
work around profunctors might help. That said, my understanding is so
bad that I can not even see any benefits or drawbacks of the structure
of ArrowLoop's "loop" versus a more "standard" fix-point structure.
I do, however, think there is something to be gained. The good old
Rosetta Stone paper still makes me think that what is now Arrow notation
might be turned into a much more potent tool – exactly because we might
be able to lift those restrictions. One particular idea I have in mind:
If the notation can support purely braided categories, it might be used
to describe reversible computation, which in turn is used in describing
quantum computation.
The frustrating part for me is that I would like to contribute to this
effort. But again, my understanding of each and every component is
fleeting at best.
MarLinn
On 2016-12-21 06:15, Edward Kmett wrote:
Arrows haven't seen much love for a while. In part this is because
many of the original applications for arrows have been shown to be
perfectly suited to being handled by Applicatives. e.g. the
Swiestra/Duponcheel parser that sort of kickstarted everything.
There are several options for improved arrow desugaring.
Megacz's work on GArrows at first feels like it should be applicable
here, as it lets you change out the choice of pseudo-product while
preserving the general arrow feel. Unfortunately, the GArrow class
isn't sufficient for most arrow desguaring, due to the fact that the
arrow desugaring inherently involves breaking apart patterns for
almost any non-trivial use and nothing really requires the GArrow
'product' to actually even be product like.
Cale Gibbard and Ryan Trinkle on the other hand like to use a more
CCC-like basis for arrows. This stays in the spirit to the GArrow
class, but you still have the problems around pattern matching. I
don't think they actually wrote anything to deal with the actual arrow
notation and just programmed in the alternate style to get better
introspection on the operations involved. I think the key insight
there is that much of the notation can be made to work with weaker
categorical structures than full arrows, but the existing class
hierarchy around arrows is very coarse.
As a minor data point both of these sorts of encodings of arrow
problems start to drag in language extensions that make the notation
harder to standardize. Currently they work with bog standard Haskell
98/2010.
If you're looking for an interesting theoretical direction to extend
Arrow notation:
An arrow is a strong monad in the category of profunctors [1].
Using the profunctors library [2] (Strong p, Category p) is equivalent
in power to Arrow p.
Exploiting that, a profunctor-based desugaring could get away with
much weaker constraints than Arrow depending on how much of proc
notation you use.
Alternately a separate class hierarchy that only required covariance
in the second argument is an option, but my vague recollection from
the last time that I looked into this is that while such a desguaring
only uses covariance in the second argument of the profunctor, you can
prove that contravariance in the first argument follows from the pile
of laws. This subject came up the last time someone thought to extend
the Arrow desguaring. You can probably find a thread on the mailing
list from Ross Paterson a few years ago.
This version has the benefit of fitting pretty close to the existing
arrow desugaring and not needing new language extensions.
On the other hand, refactoring the Arrow class in this (or any other)
way is somewhat of an invasive exercise. The profunctors package
offers moral equivalents to most of the Arrow subclasses, but no
effort has been made to match the existing Arrow hierarchy.
Given that little new code seems to be being written with Arrows in
mind, while some older code makes heavy use of it (hxt, etc.),
refactoring the arrow hierarchy is kind of a hard sell. It is by no
means impossible, just something that would require a fair bit of
community wrangling and a lot of work showing clear advantages to a
new status quo at a time when its very hard to get anybody to care
about arrow notation at all.
-Edward
[1] http://www-kb.is.s.u-tokyo.ac.jp/~asada/papers/arrStrMnd.pdf
<http://www-kb.is.s.u-tokyo.ac.jp/%7Easada/papers/arrStrMnd.pdf>
[2]
http://hackage.haskell.org/package/profunctors-5.2/docs/Data-Profunctor-Strong.html
On Fri, Dec 2, 2016 at 10:57 AM, Jan Bracker via ghc-devs
<ghc-devs@haskell.org <mailto:ghc-devs@haskell.org>> wrote:
Simon, Richard,
thank you for your answer! I don't have time to look into the GHC
sources right now, but I will set aside some time after the
holidays and take a close look at what the exact restrictions on
proc-notation are and document them.
Since you suggested a rewrite of GHC's handling of proc-syntax,
are there any opinions on integrating generalized arrows (Joseph
2014) in the process? I think they would greatly improve arrows! I
don't know if I have the time to attempt this, but if I find the
time I would give it a try. Why wasn't this integrated while it
was still actively developed?
Best,
Jan
[Joseph 2014]
https://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-130.pdf
<https://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-130.pdf>
2016-11-29 12:41 GMT+00:00 Simon Peyton Jones
<simo...@microsoft.com <mailto:simo...@microsoft.com>>:
Jan,
Type checking and desugaring for arrow syntax has received
Absolutely No Love for several years. I do not understand how
it works very well, and I would not be at all surprised if it
is broken in corner cases.
It really needs someone to look at it carefully, document it
better, and perhaps refactor it – esp by using a different
data type rather than piggy-backing on HsExpr.
In the light of that understanding, I think rebindable syntax
will be easier.
I don’t know if you are up for that, but it’s a rather
un-tended part of GHC.
Thanks
Simon
*From:*ghc-devs [mailto:ghc-devs-boun...@haskell.org
<mailto:ghc-devs-boun...@haskell.org>] *On Behalf Of *Richard
Eisenberg
*Sent:* 28 November 2016 22:30
*To:* Jan Bracker <jan.brac...@googlemail.com
<mailto:jan.brac...@googlemail.com>>
*Cc:* ghc-devs@haskell.org <mailto:ghc-devs@haskell.org>
*Subject:* Help needed: Restrictions of proc-notation with
RebindableSyntax
Jan’s question is a good one, but I don’t know enough about
procs to be able to answer. I do know that the answer can be
found by looking for uses of `tcSyntaxOp` in the TcArrows
module.... but I just can’t translate it all to source
Haskell, having roughly 0 understanding of this end of the
language.
Can anyone else help Jan here?
Richard
On Nov 23, 2016, at 4:34 AM, Jan Bracker via ghc-devs
<ghc-devs@haskell.org <mailto:ghc-devs@haskell.org>> wrote:
Hello,
I want to use the proc-notation together with
RebindableSyntax. So far what I am trying to do is working
fine, but I would like to know what the exact restrictions
on the supplied functions are. I am introducing additional
indices and constraints on the operations. The
documentation [1] says the details are in flux and that I
should ask directly.
Best,
Jan
[1]
https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#rebindable-syntax-and-the-implicit-prelude-import
<https://na01.safelinks.protection.outlook.com/?url=https:%2F%2Fdownloads.haskell.org%2F%7Eghc%2Flatest%2Fdocs%2Fhtml%2Fusers_guide%2Fglasgow_exts.html%23rebindable-syntax-and-the-implicit-prelude-import&data=02%7C01%7Csimonpj%40microsoft.com%7C80e472cedf78463bd18408d417de1af5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636159690104764444&sdata=ygqePSmgcPKnPmKDBfZplkyjG9BIDBO1L1MWHNpqw88%3D&reserved=0>
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org <mailto:ghc-devs@haskell.org>
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
<http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs>
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org <mailto:ghc-devs@haskell.org>
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
<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
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs