FWIW, when we tried to use the arrow notation commercially we ended up using a separate desugarer - the GHC version just seemed too broken. @pepeiborra did the work and wrote our replacement, so can comment as to what was broken.

The desugaring post 7.8 was accumulating bindings in a giant tuple and not releasing them after they went out of scope, causing space leaks. I simply repackaged the original algorithm by Ross Patterson into a quasiquoter. @lexi-lambda seems to be fixing it in a much better way here, which is awesome.

IIUC, the main goal of arrowp-qq is to desugar to smarter combinators so as to improve performance without needing to rely so heavily on rewrite rules. While certainly an admirable goal, and really something that GHC ought to do better, I think that point is orthogonal to this proposal, which is mostly about the static semantics. This proposal doesn’t affect how GHC prunes environments or what combinators it desugars to.

I think it might be beneficial to show some user code demonstrating why this desugaring is beneficial.

@ocharles I’ve pushed a change that includes two examples of real world code helped by this proposal, and it works through the proposed typechecking process for one of them in gory detail. Let me know if that helps.

I can't even get the example to type check using the type for handle that GHC supposedly currently accepts. Am I doing something wrong here? I get a couple of failed occurs checks relating to a ~ (a, ()).

{-# LANGUAGE Arrows #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

import Control.Arrow
import Control.Category

newtype ReaderA r arr a b = ReaderA { runReaderA :: arr (a, r) b }

lift :: Arrow arr => arr a b -> ReaderA r arr a b
lift a = ReaderA (arr fst >>> a)

class Arrow arr => ArrowError e arr | arr -> e where
  throw :: arr e a
  handle :: arr (a, ()) b -> arr (a, (e, ())) b -> arr (a, ()) b

instance Category arr => Category (ReaderA r arr) where

instance Arrow arr => Arrow (ReaderA r arr) where

instance ArrowError e arr => ArrowError e (ReaderA r arr) where
  throw = lift throw
  handle (ReaderA f) (ReaderA g) = ReaderA $ proc (a, r) ->
    (f -< (a, r)) `handle` \e -> g -< ((a, e), r)

Your implementation of handle isn’t quite right. This is the one that GHC currently accepts:

instance ArrowError e arr => ArrowError e (ReaderA r arr) where
  throw = lift throw
  handle (ReaderA f) (ReaderA g) = ReaderA $ proc ((a, ()), r) ->
    (f -< ((a, ()), r)) `handle` \e -> g -< ((a, (e, ())), r)

Those ()s in the type of handle really do need to be reflected at the term level, so the difference isn’t strictly in the type system. And indeed, the noisiness at the term level is part of the reason the current implementation is frustrating to work with!

Aha, thanks. I got the impression that only the type of the control operators needed to change after 7.8, but the usage of control operators needed to change too. I think it's very important to make that clear in the proposal. Something like

Whereas the type of handle used to be the nice-looking

handle :: ArrowError e arr => arr a b -> arr (a, e) b -> arr a b

to use it in proc notation after 7.8 it's type had to become the unpleasant-looking

handle :: ArrowError e arr => arr (a, ()) b -> arr (a, (e, ())) b -> arr (a, ()) b

and whereas expected usages of handle used to be nice-looking things like

    (f -< (a, r)) `handle` \e -> g -< ((a, e), r)

post 7.8 they had to become unpleasant-looking things like

    (f -< ((a, ()), r)) `handle` \e -> g -< ((a, (e, ())), r)

A good point—I’ll try to work that in more explicitly. It might be worth saying, however, that the issue isn’t quite as bad as that instance might make it appear. The changes at the term level only show up when implementing control operators, and that ArrowError instance counts, even if it’s only a lifting instance.

When using control operators (and obediently remaining entirely within the proc DSL), the code does not (usually) need to change. If you had some code that used handle, like

proc (foo, bar) -> (launchTheMissiles -< foo) `handle` \e -> recover -< (e, bar)

then it would not have had to change from GHC 7.6 to 7.8.

In practice, I find I end up writing a lot of control operators myself—many of which simply wrap existing control operators like handle—so I definitely don’t think user code is by any means immune from the effects of the change. It’s just important to be aware of where the abstraction boundaries lie.

I see. That makes it clearer why you left it out of the original proposal. It also makes me more confused about how this desugaring works at all. I haven't read it through in detail. Now I'm guessing there must be two cases: one where a desugaring of applied arguments to (...(..., ())) form happens and one where it doesn't because the arguments are already in that form!

I'm confused about the keyed example. As a function, keyed only has one argument. As a control operator it is given two. What's going on there?

Another way of reasoning about what I said in my previous comment is to consider the relationship between arrows, functions on arrows, and commands. Commands are the building block of proc notation, but they aren’t values in any sense; they’re purely a syntactic construct.

Atomic commands are created by “lifting” an arrow into a command—in effect, this is what -< and -<< do. However, note that -< and -<< don’t only lift an arrow into a command, they also apply it to an argument simultaneously. This leads to rather awkward constructions: consider, for example, the command \e -> f -< e. If the arrow being used here is (->), this command is equivalent to the ordinary lambda expression \e -> f e. That expression can be trivially eta-reduced to f, but there is no equivalent in the world of commands!

This hints at a missing feature of proc notation, an ability to lift an arrow into a command without applying it to any arguments. A natural syntax for such an operation would be (f -<), a sort of “command section.” (The reason plain f on its own won’t do is you need to know if f should be in the scope of arrow-local variables or not, so you need (f -<) or (f -<<) to disambiguate.)

In any case, the (| e c ... |) syntax is also a lifting operation, but a different kind: it lifts a function on arrows into a function on commands, rather than lifting an arrow into a command. Since commands are not actually values (and do not actually have Haskell types), it does this using a somewhat complicated “calling convention,” which is where all this tupling and untupling comes in.

When living completely in the DSL, as in the example I gave in my previous comment, the calling convention isn’t exposed because you are working exclusively with commands. Even though handle is really a function on arrows, not a function on commands, its implementor has already done all the work of making sure it cooperates with the right calling convention. Therefore, you can just think about commands.

When you want to implement a new function on commands, however, you fundamentally must think about the calling convention, since you are straddling the boundary between arrows and commands. This hints at a second missing feature of proc notation: a syntax for defining functions on commands directly, where the calling convention is hidden behind an abstraction boundary in the same way it already is for uses.

This “arrow/command” duality is an extraordinarily leaky abstraction, and it makes proc notation a little bit frustrating to work with in practice, even with the proposed change. Since commands are not values, just syntax, it means you cannot lift a command out of a subexpression and bind it to a local variable. To illustrate, if you have some monadic code, you can transform

\foo bar -> launchTheMissiles foo `catchError` \e -> recover e bar

into

\foo bar -> do
  let handler e = recover e bar
  launchTheMissiles foo `catchError` handler

or even

\foo bar -> launchTheMissiles foo `catchError` flip recover bar

There is no equivalent capability with commands. It would be wonderful to fix that problem, but that would be a much, much larger proposal, and it might amount to a new Arrows2 language extension rather than a modification to the existing one.

It also makes me more confused about how this desugaring works at all. I haven't read it through in detail. Now I'm guessing there must be two cases: one where a desugaring of applied arguments to (...(..., ())) form happens and one where it doesn't because the arguments are already in that form!

To be honest, I am confused about this, too! In the original (pre-7.8) implementation, and in my proposal, applying an arrow to an argument stack of length 1 simply Does The Right Thing due to the way the calling convention is defined. In the original implementation, the argument stack takes the shape ( ... ((s1, s2), s3), ... sn), so when there’s only one argument, it’s just s1. Likewise, in my proposal, ArrowStack '[s1] is simply s1.

In the current implementation, however, this property clearly does not hold. The argument stack has the shape (s1, (s2, (s3, ... (sn, ())))), and the base case of that is not s1 but (s1, ()). This implies that f -< e should actually expect f to have type arr (a, ()) b if e has type a, but obviously this does not actually happen in practice. There is an inconsistency here, and I consider it to be one of many flaws with the current implementation.

I'm confused about the keyed example. As a function, keyed only has one argument. As a control operator it is given two. What's going on there?

That is a mistake in the proposal; good catch. I previously used a different type for keyed, decided to simplify it slightly, but failed to update the example. I’ll push a fix.

consider, for example, the command \e -> f -< e

Do you mean proc -> f -< e? I can't get the former to be accepted as valid syntax.

Do you mean proc -> f -< e? I can't get the former to be accepted as valid syntax.

\e -> f -< e is not a valid expression (unlike proc e -> f -< e), but it is a valid command. It appears in uses of handle, for example:

proc x -> (f -< x) `handle` \e -> g -< e

That \e -> g -< e is not a lambda expression! It is a lambda command, which is quite different—note that the body of the lambda is itself a command. We would presumably like to be able to write proc x -> (f -< x) `handle` g, but that is rejected, since g is not a valid command. Hence the hypothetical (g -<) syntax, so we could write proc x -> (f -< x) `handle` (g -<)… but that is not (currently) part of this proposal, so it’s mostly just a tangent.

Oh I see. \ is used where Paterson uses kappa.

Yes, that’s right. Type and Translation Rules for Arrow Notation in GHC is a better reference for the pre-7.8 syntax as implemented in GHC than the original paper.

I think you and I (and any other interested parties) should find a place to have a discussion about addressing the points in your longer comment, for example, by trying to turn commands into real things by making ⇀ a real thing (perhaps a type family).

Sure, I agree that would be valuable! I also agree that this thread is probably not the place to have it. Do you have any suggestions for a venue? Perhaps a haskell-cafe thread? Or is too deep in the weeds for that?

Maybe we can just start an Arrows2 GitHub repo and do it on comments and PRs.

Works for me. Feel free to create one and link me to it, and we can continue the conversation there.

Anyone interested in discussing next-generation Arrow notation in general can join in at https://github.com/tomjaguarpaw/Arrows2 and we can leave this PR discussion for the particular proposal at hand.

It also makes me more confused about how this desugaring works at all. I haven't read it through in detail. Now I'm guessing there must be two cases: one where a desugaring of applied arguments to (...(..., ())) form happens and one where it doesn't because the arguments are already in that form!

To be honest, I am confused about this, too! In the original (pre-7.8) implementation, and in my proposal, applying an arrow to an argument stack of length 1 simply Does The Right Thing due to the way the calling convention is defined. In the original implementation, the argument stack takes the shape ( ... ((s1, s2), s3), ... sn), so when there’s only one argument, it’s just s1. Likewise, in my proposal, ArrowStack '[s1] is simply s1.

As it happens, I’ve figured out the answer to this conundrum: the current implementation just ignores the argument stack entirely in the typing rules for -< and -<<! This makes it impossible to partially apply arrows passed to control operators. So that’s another point against the current implementation.

Expanded on my previous comment's edit, you already address this a bit with:

If [ArrowStackTup '[a] /~ a], then users who restrict themselves to the simpler subset would conceptually be working with a rule like this:

[rule with implicit Unit]

Users would find this rule perplexing and frustrating, and rightly so. It’s a very stupid rule. So we either make ArrowStackTup '[a] ~ a, or we drop support for the stack in arrow application.

I totally agree with that if we must use one -<. But if we move the goal posts, a third solution is to keep -< traditional by requiring no stack and also not using Unit, and make a new --< (straw-man syntax) which does support arbitrary stacks with one injective type family that uses Unit:

G |-- e_1 :: alpha tau_1 tau_2
G, D |-- e_2 :: tau_1
----------------------------------------------
G, D |--_alpha e_1 -< e_2 :: Stk[[ '[] ]] --^ tau_2

G |-- e_1 :: alpha Stk[[ tau_1 ': sigma_2 ]] tau_2
G, D |-- e_2 :: Unit tau_1 -- Unit tau_1 ~ Stk[[ '[ tau_1 ] ]]
----------------------------------------------
G, D |--_alpha e_1 --< e_2 :: sigma_2 --^ tau_2

No breakage or implicit Unit wrapping! Of course, we have turned the problem of two awfully similar type families into two awfully similar operators, a rather Pyrrhic victory. But, we can generalize our second operator "for free", giving it more purpose:

G |-- e_1 :: alpha Stk[[ sigma_1 ++ sigma_2 ]] tau_2
G, D |-- e_2 :: Stk[[ sigma_1 ]]
----------------------------------------------
G, D |--_alpha e_1 --< e_2 :: sigma_2 --^ tau_2

Here, the stacks are concatenated, so one can do exp --< (), or exp --< (....) in addition to exp --< Unit x. The injectivity is crucial is crucial to be able to concatenate the type level lists without ambiguity.

As a final second bonus circling back to my previous comment, this also helps the eta-contraction problem @lexi-lambda was talking about above, with f --< () turning an arrow into command without effecting the arguments it takes:

G |-- e :: alpha Stk[[ sigma ]] tau_2
| - () :: Stk[[ '[] ]]
----------------------------------------------
G |--_alpha e --< () :: '[] ++ sigma --^ tau_2
----------------------------------------------
G |--_alpha e --< () :: sigma --^ tau_2

The only caveat is the parameter type of e has to be in the image of Stk[[ .. ]], i.e. it has to be a tuple (including Unit).

@lexi-lambda #303 (comment) is a very good explanation, and deserves not to be forgotten in a Github thread. It would absolutely be worth make it a blog post or an appendix to this proposal. Somewhere where it can be found in the future.

Alexis, I confess that I have been a laggard on this proposal. My apologies. Arrows make my head spin. But let me say that I am very sympathetic to your goals of a simpler and more uniform treatment of arrow. The entire arrow-notation part of GHC has received very little well-informed love, and I for one am delighted that you are minded to rectify this lack. Thank you!

I really appreciated your tutorial above. But I stumbled many times because there are no typing rules. Yet you have them, attached to your proposal (though I missed that at first). Moreover, as Arnaud says, your tutorial is too valuable to be left in a comment thread. Would you consider:

• Making a standalone wiki page (or whatever) with your tutorial, perhaps something you can continue to refine.
• Given a full BNF of the fragment of Haskell that you want, with new bits highlighted.
• And its typing rules, with old vs new highlighted
• Including the desugaring changes.
• And types of the key built-in or library functions (eg mapA), again highlighting changes. I think you plan to change the type of mapA, handle?

I think you have most or all this already, so I don't think I'm asking you to do new work. Please say if I am wrong about this. But, coming un-informed to this, I found it hard to be sure what changes are being proposed, in the context of the full system.

If it would help, I've managed to dig out the source Latex for the Type and translation rules for arrow notation in GHC (2004) document.

Regardless, before we are finished with landing all this, it would be great to have an updated version of that (very sketchy and incomplete) document, as a permanent guide to this part of GHC.

Returning to the payload,

• You say that GHC 7.8 changed the types of mapA and handle in ugly ways, but you don't say why that change was forced, or specifically how your approach avoids that.
• Leaving aside cmd abstractions, in your system the ordinary rules for -< and -<< use the Stk (in rules; ArrowStackTup in code) type family. Is that necessary, or does pairing suffice, as it did before? Or is it somehow indirectly forced by what you are doing for cmd abstractions? Or, guessing wildly, could you continue to used nested pairs for ordinary -< etc, by using a different (nested) definition for ArrowEnvTup?
• I'm quite baffled by the ArrowStackTup/ArrowStackEnv distinction, and the subtle stuff about how one is injective and one is not. I believe you, but it's hard for me to grok what are the "important type inference properties" that you are trying to uphold. Perhaps some examples would help?

Side note: I always stumble on the difference between -< and -<<. They seem to have an identical typing rule, but different desugarings. It's nothing to do with this proposal, but what's going on there?

In conclusion: I'm sure we should accept this proposal in some form. I'm just trying to be sure it can't be simpler.

In addition to the comments by Simon, during the Committee discussion the "wired-in-ness" of te type families was discussed, and we seem to lean towards not discussing that issue in the proposal, but leave it as an implementation detail.

@lexi-lambda I am going to put the proposal again as "in review", until you feel comfortable with submitting it again

Thanks for pinging me about this—I had actually forgotten that I had not yet responded to Simon’s comments!

I am unfortunately likely going to be pretty tied up for the next week or so, but I will get on top of this after that.

No rush, Alexis. Arrows are tricky, and a bit unfamiliar to many (incl me), so there is more "tutorial" to do. But I don't think that is wasted effort -- quite the reverse, as I say above I hope we can capture some of the core ideas in a more durable form.

I really appreciated your tutorial above. But I stumbled many times because there are no typing rules. Yet you have them, attached to your proposal (though I missed that at first). Moreover, as Arnaud says, your tutorial is too valuable to be left in a comment thread. Would you consider: [snip]

Yes! I intend to significantly rewrite the section of the User’s Guide to incorporate some of that information, and I’d be happy to create a wiki page with some of the less user-facing details. Some of that information is also included in Notes in the current implementation PR.

If it would help, I've managed to dig out the source Latex for the Type and translation rules for arrow notation in GHC (2004) document.

Regardless, before we are finished with landing all this, it would be great to have an updated version of that (very sketchy and incomplete) document, as a permanent guide to this part of GHC.

I agree! I think it would be helpful, and I am hoping to expand upon the current Ott model with some explanatory prose that adds some much-needed context to the rules themselves.

You say that GHC 7.8 changed the types of mapA and handle in ugly ways, but you don't say why that change was forced, or specifically how your approach avoids that.

Yes, that is a good point. I have added an entirely new section to the proposal that discusses the rationale for the GHC 7.8 change, just below the Motivation section. It is subtle, so feel free to ask for clarification, but I am hopeful that will help somewhat with your confusion.

Leaving aside cmd abstractions, in your system the ordinary rules for -< and -<< use the Stk (in rules; ArrowStackTup in code) type family. Is that necessary, or does pairing suffice, as it did before? Or is it somehow indirectly forced by what you are doing for cmd abstractions? Or, guessing wildly, could you continue to used nested pairs for ordinary -< etc, by using a different (nested) definition for ArrowEnvTup?

There are several questions here, and I am not sure I fully understand all of them. You ask “does pairing suffice?” but I am unsure what you have in mind by “pairing,” as ArrowStackTup is doing tupling!

Perhaps you mean “could it use nested pairs instead of flat tuples,” and the answer is “sure.” But that would just involve a different definition of ArrowStackTup that produces nested pairs instead of flat tuples, and I see no benefit to such a design.

I'm quite baffled by the ArrowStackTup/ArrowStackEnv distinction, and the subtle stuff about how one is injective and one is not. I believe you, but it's hard for me to grok what are the "important type inference properties" that you are trying to uphold. Perhaps some examples would help?

Yes, it is quite subtle. However, the proposal actually already does provide an example, though it may not be obvious to find. Take a look at the subsection entitled “A worked example using handle,” which relies on the injectivity of ArrowEnvTup in step 3.ii. The end of the section reflects on its necessity:

This example concretely illustrates why it is crucial that ArrowEnvTup is injective: in step 3, it allowed us to infer the expected stack for each argument to handle. Consider that if we didn’t learn that information that way, we’d be totally stuck in step 4, since ArrowStackTup is non-injective! We would gain no information from the types of f and g, so if s1 and s2 remained unsolved metavariables, resulting in a type error due to insoluble equalities.

Does that help?

Side note: I always stumble on the difference between -< and -<<. They seem to have an identical typing rule, but different desugarings. It's nothing to do with this proposal, but what's going on there?

The answer is that -<< requires ArrowApply while -< requires only Arrow. Here’s a Note from my implementation branch that goes into a little more detail, which perhaps you will find clarifying:

Note [The command environment]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Although lambda expressions have a direct counterpart in core, proc
expressions do not---they are desugared into ordinary applications of
the Arrow class methods. This process essentially involves rewriting
the program into point-free form. For example, the expression

    proc x -> do { y -< f -< x; g -< y }

is desugared into simply `f >>> g`; the intermediate x and y variables
disappear! But this presents a problem: what if x or y appeared in one
of the arrow expressions itself, rather than as an argument?

    proc x -> do { y <- f x -< x; g -< y }

As before, we’d desugar this into `f x >>> g`... but now x is unbound!
So we reject this program as ill-formed. More precisely, we disallow
references to “arrow-local” variables on the left side of a “-<”. (In
fact, we don’t even consider them in scope.)

Which variables are “arrow-local”? All variables bound by the proc
argument pattern or any commands. This is quite restrictive, but it’s
also what makes arrows useful relative to monads: the structure of an
arrow computation doesn’t depend on the arrow’s input. Exceptions to
this restriction implement the ArrowApply class, which provides the
app method:

    app :: ArrowApply p => p (p a b, a) b

Using app, it turns out we can express the above example after all:

    arr (\x -> (f x, x)) >>> app >>> g

We don’t try to figure this out automatically (since that would make
lexical scope dependent on typing!), but the programmer can request it
explicitly using the -<< command:

    proc x -> do { y <- f x -<< x; g -< y }

To summarize: we treat arrow-local variables as out of scope on the
left side of “-<”, but in scope on the left side of “-<<”.

After grasping at straws for a bit, I thought I might have found a solution to having just one one type family, invective via Unit, but without implicit Unit conversions, in #303 (comment) . But I think my comment got lost in the preceding discussion, and there were no explicit typing rules so it was hard to follow. I just edited in some crude ascii-art providing the rules along with more elaboration (I really do need to go learn this OTT!), so hopefully it is clearer now, and useful.

I agree that it's a Bad Thing to change the user experience for the
worse to make type inference easier. I don't think I ever understood
that's what happened in GHC 7.8. Yikes. So bravo for working on this.
I'm totally on board with going back to a better user API.

However, I am not yet convinced that the way to solve the type inference
question is through several new type functions, especially if they
are user-visible. (And I assume they are, or else they wouldn't appear
in this proposal.)

For example in the "command typing" type rule the judgement has form

    |- cmd :: sigma \funnyarrow tau

Now the \funnyarrow is not a real type constructor that can appear in types.
It's part of the syntax of the typing judgement. We could write

    |- cmd :: sigma_1, ..., sigma_n ; tau

Now we don't need to form tuples or anything. In the code of GHC today I see

type CmdType    = (CmdArgType, TcTauType)    -- cmd_type
type CmdArgType = TcTauType                  -- carg_type, a nested tuple

tc_cmd :: CmdEnv -> HsCmd GhcRn  -> CmdType -> TcM (HsCmd GhcTcId)

But we could instead have

type CmdType    = ([TcTauType], TcTauType)    -- cmd_type

where that list is the sigma_1 .. sigma_n above.

It may not be easy to work all this out in a written dialogue -- I need
too much education. Maybe we should have a call? I don't know much
about arrows, but I know quite a bit about type inference in GHC :-).

However, I am not yet convinced that the way to solve the type inference question is through several new type functions, especially if they are user-visible. (And I assume they are, or else they wouldn't appear in this proposal.)

The crux of the problem is that, when control operators come into play, GHC can’t immediately determine how many values are on the stack. This is why your proposed solution isn’t enough. You say

But we could instead have

type CmdType    = ([TcTauType], TcTauType)    -- cmd_type

but now we’ve lifted the list out of the language (i.e. Haskell’s type language) and into the metalanguage (i.e. the GHC typechecker). This is trouble, because we may need to run the constraint solver to figure out how many values are on the stack.

If you want a concrete example of a pathological scenario, consider code like this:

foo :: Int -> String
foo = proc x -> (| id (show -< x) |)

Here, the control operator used is id, which is enormously polymorphic. How do we figure out how many values are on the stack while typechecking f -< x? Just looking at the type of id alone tells us nothing, since it’s so polymorphic it would work with any number of values. For example, we could also write

foo :: Int -> String
foo = proc x -> (| id (\y -> show -< y) |) x

which does the same thing, but it passes x through id on the stack instead of via the environment. That’s legal, since we can instantiate id at either of these types:

• id :: (ArrowEnv Int -> String) -> ArrowEnv Int -> String
• id :: ((ArrowEnv (), Int) -> String) -> (ArrowEnv (), Int) -> String

If GHC’s CmdType were to include a metalanguage-level list of TcTauTypes, it would have to disambiguate between these two situations at constraint-generation time. That’s quite an unreasonable burden in general, since it may even require knowing the types of the argument commands!

This proposal hinges on pushing the list from the metalanguage into the language by using a type-level list. Then we can just emit some equalities for the constraint solver to deal with later:

[W] t1 ~ ArrowEnvTup e1 s1
[W] t1 ~ ArrowEnvTup e2 s2
[W] s1 ~ '[]
[W] t3 ~ ArrowEnv Int
[W] (t1 -> t4) ~ (t3 -> String)

The constraint solver can use its entire bag of tricks to find a solution to these constraints. Sometimes that means propagating information top-down, sometimes it means propagating it bottom-up. This is where the injectivity of ArrowEnvTup comes in, since it allows GHC to work backwards to pluck a solution out of these ambiguous-at-first-glance scenarios.

Any simpler solution must compromise on this in some way. Maybe we don’t want to accept things like id as arrow control operators. Fine—this is obviously not a real use case. But will whatever we come up with support the use cases people do have? Do we want to allow things like (| (f e) cmd |)? How do we intend to typecheck those?

The solution in this proposal is the simplest design I can come up with that is both clearly sufficiently-general and does not break type inference.

GHC can’t immediately determine how many values are on the stack.

Fair enough. But we should make a sharp distinction between

1. The declarative type system that says what is and is not well typed
2. The inference engine (in GHC: generating constraints and solving them later) that figures out what types everything has.

The inference engine has lots of to-and-fro information flow, true enough. But that typically does not show through in the specfication. To take an example, the declarative type system for ML often guesses monotypes out of thin air, such as

G, x:tau |- e : rho
-------------------
G |- (\x.e) : tau -> rho

Here tau comes from nowhere. That's the spec. The inference engine uses a unification variable, and does lots of unification, to figure out what tau should be. But no details about unification variables or unification show up in the specification.

The bit I'm not convinced about, then, is whether ArrowTup and friends need to be in the specification. Implementation/inference engine perhaps, but do they have to be part of the spec?

For example, maybe rule CMD_APPF could look something

G |- e1 :: alpha (t1, s1, ..., sn) t2
G,D |- e2 :: t2
-------------------------------
G|D |- e1 <-- e2 :: (s1, ..., sn) hookarrow t2

That is, after type inference is complete we need to know n, and s1..sn.

Then there's a separate question about how to implement type inference, which will involve constraints and, quite possibly, type families.

A call might help? @rae may have views here

Fair enough. But we should make a sharp distinction between

1. The declarative type system that says what is and is not well typed
2. The inference engine (in GHC: generating constraints and solving them later) that figures out what types everything has.

The inference engine has lots of to-and-fro information flow, true enough. But that typically does not show through in the specfication.

I want to make clear that I completely agree with this. My justification is the typing rules in this proposal are perfectly declarative because Sᴛᴋ and Eɴᴠ are metafunctions. They aren’t type families.

Now, having said that, arguably there are two ways I let implementation details leak into the rules beyond what I should have:

1. The declarative rules have no need to distinguish between Sᴛᴋ and Eɴᴠ, they just need a single metafunction to perform tupling.

2. The use of promoted list constructors in the declarative rules is unnecessary; the judgment could simply include a list of types.

So I think your point is a good one, and perhaps I should make those changes. But I think the more algorithmic rules have value, too, if only as an explanatory tool for the implementation.

The bit I'm not convinced about, then, is whether ArrowTup and friends need to be in the specification. Implementation/inference engine perhaps, but do they have to be part of the spec?

Here’s my point of view: Paterson’s old rules had the Sᴛᴋ and Eɴᴠ metafunctions, too, just with a different syntax. His syntax looked like this:

It has already been discussed upthread how this syntax is confusing. So I decided to make my metafunctions more explicit. On the other hand, perhaps the flat-tuple representation eliminates the potential for confusion? Maybe I am now in fact justified to use Paterson’s notation!

Then there's a separate question about how to implement type inference, which will involve constraints and, quite possibly, type families.

Indeed. Yet I think it would be a bad idea for this proposal to not mention any algorithmic details, as the reason arrow notation doesn’t already work this way today is primarily due to implementation obstacles, not the lack of a worked system of declarative rules. So I think focusing entirely on the declarative system would rather miss the point.

Then there's a separate question about how to implement type inference, which will involve constraints and, quite possibly, type families.

…actually, let me comment on this point a little bit more. There is something you are alluding to here, namely the idea that we could solve this problem without any type families. And you are, of course, quite right: we could introduce an entirely new type of constraint within GHC specifically to support arrow notation. Then we could keep these special “arrow notation constraints” entirely out of the user’s face, which would most definitely be an improved experience.

But I did not list that as an alternative in this proposal because I did not think such a thing had any hope of being accepted. I figured it would be far too much additional logic too deeply wired into the GHC typechecker to support a feature that is already somewhat maligned. The type families approach seemed like a compromise: a way to encode things into the type system without such a large maintenance burden. But if you disagree, and you think such an idea really ought to be considered, by all means, say so!

OK, this is good. I had totally conflated your meta-functions and the new type functions.

This is confusing territory, not easy to express clearly. Suggestions:

• Make a remorselessly clear separation in the proposal between

  • Specification (which mentions nothing about type families). This is the user-visible "proposed change specification".
  • Implementation implementation/inference. Yes, I agree it is good to discuss this, but in a section labelled "Type inference", and being clear that the section is there to indicate that there is a feasible implementation path.

• The specification part should have typing rules -- and you already have those. We should get @rae's help in writing them. For these lists of types I think you can be quite syntactic, using BNF. Rather than an informal \overline{\tau}, you could write

\overline{\tau} ::=  \epsilon    -- Empty sequence
                          |   \tau , \overline{\tau}

Now \overline{\tau} is a metavariable (just like \tau itself) which has two productions as above. You may want a way to turn such a list of types into a tuple, by including it in the sytnax of types, something liie

\tau ::= a     -- Type variable
         | \tau_1 \tau_1    -- Application
         | ( \overline{\tau} )    -- Tuple
        ...

where I'm using the round brackets to turn a list of types t1, t2, ... tn, into a tuple type (t1, t2, ..., tn).

I think this might be a quieter notation, and less misleading (in the way I was misled), that would do what you want.

It's important to be clear about the difference between a sequence of two types t1,t2 and a one-element sequence whose only element happens to be a pair thus (t1,t2). This is a potent source of confusion.

Something like this will really help not only the proposal, but our permanent description of what we have.

Returning to type inference, I'm not against using type families. But if we know they are an implementation artefact, that will help us when designing error messages etc -- and it means we can change the details at will because it's not part of the language spec.

@simonpj asked me to pipe up here, but I'm not really sure what to say to really move this conversation forward:

• I, too, stumbled in understanding the rules at first glance. But in retrospect, I think that's because I came in thinking I already knew what was going on, when I didn't. Reading the rules now, they seem clear enough to me.

• I realize I never profusely thanked @lexi-lambda for the tutorial above -- I read it when it was fresh and felt very educated. I apologize for not thanking her sooner.

• I agree with Simon about specification vs implementation. That is, the specification indeed need not mention type families, but I do think they are a very viable implementation path. Having these points separated out is good, but I actually don't think it's necessary here. There are tons of features in GHC lacking even an algorithmic write-up, and so insisting on having both an algorithmic presentation and a declarative one seems a stretch too far. I'd personally be happy with an admission that the type families are not part of the spec -- they can be simply be viewed as metafunctions used to write the rules, and we happen to implement these rules via type families.

• I do think the type families will show up in error messages -- just like error messages today mention unification variables (noticeable by their e.g. 0 suffix), among other details like occurs-check errors and skolem-escape. I'm fine with exposing these type families in error messages. Maybe I could be convinced that we shouldn't export them (so as to reserve flexibility for the future), but I'm fine with exporting them, too.

My bottom line is that I'm quite happy with this proposal and think we should try to move forward with it.

I do think the type families will show up in error messages -- just like error messages today mention unification variables (noticeable by their e.g. 0 suffix), among other details like occurs-check errors and skolem-escape. I'm fine with exposing these type families in error messages.

I agree. Also, my proposal (in #303 (comment)) for avoiding the Env-Stack distinction goes further in exposing the (now single) type family to the user so as not to loose expressive power w.r.t. the proposal as written.

@simonpj had a chat about this proposal to resolve our differences (he wants more clarification; I'm not feeling that as strongly). We agreed that a good way to move forward was simply to add a little bit of tweaking to the ott spec (rendered at https://github.com/lexi-lambda/ghc-proposals/blob/constraint-based-arrow-notation/proposals/0000-typechecking-rules.pdf). I think the changes would be quite modest. @lexi-lambda, would you want me to suggest some concrete changes, or just submit a PR against your repo?

Just to clarify more what I meant in (my comment above](https://github.com/ghc-proposals/ghc-proposals/pull/303#issuecomment-652636138]

• I'd love the typeset rules to be fairly complete. In particular, fully define the funny Stk and Env notation. I totally misunderstood them as standing for type families, but actually it's just doing something that is more commonly expressed using syntax (see my comment above) and/or over-bar notation.

  For example, consider the rule form in a box G | D |-a cmd :: sigma --> tau, where --> is the funny hook arrow. Here sigma is a type. But I don't think you need it to be. It'd be simpler for it to be a list of types, thus G | D |-a cmd :: \overline{\tau} --> \tau.

  Then you do indeed need a way to turn a sequence of types \overline{\tau} into a tuple type (tau_1, ... tau_n), so you need a notation for that, perhaps tuple(\overline{\tau}).

• Move everything about type families out of "Change specification" and into "One possible implementation plan". As I understand it, any implementation of the rules (which make no mention of type families) would be absolutely fine. The type families are not part of the spec. It's good to articulate an implementation path, but I really clear blue water between the spec and the impl.

• Once we have the specification/implementation split clear, we might want to talk more about the implementation choices -- but that needn't hold up the proposal.

To be clear, I'm fully in support of the goal, and I think you've done a fantastic job of explaining stuff. I'm sure we should accept this proposal. I'd just like to to be clear, to everyone, just what we are accepting.

@sgraf812 Let me preface this by saying that everything in the Ott model is currently exclusively about generating something that is (hopefully) useful to people once it is typeset. Some of the details you note—such as underspecifying the structure of contexts and having a somewhat naïve view of pattern typing—are really just because the model is intended to show all the details of arrow notation, not the rest of GHC’s modern flavor of Haskell. And in the context of Haskell 2010, pat : t => D really is a perfectly fine judgment for pattern typing because view patterns do not exist.

Regardless, your comments suggest that the current approach was not successful in distilling those details and effectively communicating them, so something does still need to change. It’s been ages since I actually looked at that Ott model at all, but I’ll find some time to go through it again and see if I can incorporate your suggestions.

The bit I'm not convinced about, then, is whether ArrowTup and friends need to be in the specification. Implementation/inference engine perhaps, but do they have to be part of the spec?

Having only had a cursory look over the comments after having read the typing rules, I wonder the same thing as Simon above. I see no material change to the typing rules at all! It's basically just two opaque uninterpreted functions slammed in-between, which seem to give a representation to a list of types in different ways. Ah yes, you acknowledge that:

I want to make clear that I completely agree with this. My justification is the typing rules in this proposal are perfectly declarative because Sᴛᴋ and Eɴᴠ are metafunctions. They aren’t type families.

So, to be clear: If I understand correctly, we could just stick to Patterson's rules and substitute the confusing overloaded use of (tau,taus), maybe to something like [tau taus] and we wouldn't need to touch the declarative spec at all, right?

Yes, I think this is currently the main problem with the proposal as-written, and I think Simon’s criticism (and by extension yours) is on the money. The proposal is currently insufficiently clear about a few things:

• From a behavioral point of view, this proposal is essentially nothing more than a bug fix. GHC used to implement Patterson’s arrow notation rules, and at some point it stopped doing so, which was a regression that unfortunately went unnoticed for a very long time. This proposal suggests we fix it.

• Because the proposal amounts to a bug fix, the proposed change to the declarative type system is… nothing at all.¹ This means the meat of this proposal is really about implementation, not specification.

• The suggestion about type families arises entirely from the fact that the only obstacle here is one of implementation, not specification, so the content of the proposal is a proposed implementation technique. Not surprising when spelled out like this, but not at all clear from the text of the proposal.

Why did I screw this up so badly in my first draft of the proposal? Because when I wrote it, it wasn’t actually clear to me that everyone would view the change in behavior as a regression rather than as a change in specification that I would have to argue against, so I presented it primarily through that point of view. However, the discussion revealed that (a) almost nobody knew this feature existed in the first place, and (b) even fewer realized any change had ever occurred.

So, with that added context, I think the main thing that needs revision here is the framing of the proposal. It would be better to just assert that the current behavior is broken and make explicit that the proposal is about an implementation technique to fix it. That should, I hope, clear up the confusion.

We could then say "well, but we want to represent these Stk [taus] like this and this Env [taus] like this", for obvious efficiency reasons. Then all that is left to do is either

1. Use wired-in type families to represent the constraints that we need during inference, leaning on a lot of existing infrastructure for coping with TyFams, or

2. Come up with new constraints that need special handling in the inference engine

I have no idea which of the two is more feasible. (2) might seem daunting, but maybe it wins when we start trying to give good error messages?

Yes, absolutely correct! And to be honest, I have thought about option 2 myself quite a few times since I originally wrote this proposal, especially after I attempted to implement everything in GHC. However, I did not list it as a possible alternative in the proposal for two reasons:

• I got the impression that arrow notation is a rather unpopular feature that several people find (or at least have found) more trouble than it’s worth to maintain. Therefore, adding entirely new types of constraints just for arrow notation seemed unlikely to go over very well, as it’s unclear whether the maintenance burden they would create would be worth it.

• Using wired-in type families is an existing technique already used in GHC, and it’s enough to straightforwardly implement everything in the proposal except error reporting. Given the previous point, taking advantage of all that existing infrastructure seemed like a big win—it would make the maintenance burden of the change much closer to “basically free”.

Unfortunately, when I went to write the implementation, I discovered that getting the sort of custom error reporting I wanted for wired-in type families is nearly impossible given the way they are currently handled in the constraint solver. So, having learned that, I think it would be valuable to revise the proposal in three ways:

1. As discussed above, reframe the proposal to be explicitly about finding an implementation technique to fix a bug in GHC’s implementation of arrow notation.

2. Present the proposed declarative rules without coupling them to any particular implementation technique. Discuss why they are challenging to implement in GHC as-written and why the regression occurred in the first place.

3. Discuss how wired-in type families are a possible implementation technique for the proposed declarative rules, and note the effects they would have on error reporting. Also discuss custom constraints as a potential alternative and how they would make improved error reporting easier.

After such a revision, the proposal would not really be in a state to be approved, because it leaves a significant question open: should we use type families or custom constraints? But hopefully the revised proposal would make it easier for people to understand the content of the proposal and the associated tradeoffs, so we could resurrect the conversation and pick which implementation technique is preferable before moving forward.

Does all that sound good to you? If it does, I may attempt to make those revisions myself at some point (though it’s been long enough that I admit I’m not certain exactly how much effort it’s worth it to me to personally invest in getting this proposal merged).

Does all that sound good to you?

It does to me.

If it does, I may attempt to make those revisions myself at some point (though it’s been long enough that I admit I’m not certain exactly how much effort it’s worth it to me to personally invest in getting this proposal merged).

I know the feeling.

But is your lack of motivation about the proposal or about the implementation? I sense that perhaps you are motivated to get this implemented, but less motivated to have a beautiful writeup of the various implementation choices? I ask because a GHC proposal doesn't need to say much about implementation. Indeed, since we now understand that this one is simply a bug-fix, you could argue that we should simply fix the bug. Since it is a long standing bug, a proposal to describe the change may be good practice, and helpful for some -- but is far less of a big deal than proposals that introduce new features.

That said, even if it's not a formal proposal, it is really helpful to discuss, and get consensus around, design choices before getting elbow deep in code. So it's not wasted work!

And in the context of Haskell 2010, pat : t => D really is a perfectly fine judgment for pattern typing because view patterns do not exist.

I'm still not convinced it is. Which type variables may appear in t? Any? In particular, I'd like to know at the use sites of pat : t => D, in Abs, Case and Do_Bind, which type variables are in scope for pat/t. Only those from G or also the local D ones? Probably the latter. Or maybe the former, given that tau_1 from Abs ends up in the arg tuple and that will eventually escape the scope of D?! I actually asked myself this question while working on rebasing https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3191. Maybe we want to choose differently in Abs (no locals) than in Do_Bind (locals allowed)?

It's underspecified in the original spec as well, so no worries. And I think we established that we are primarily interested in the bug fix nature of this proposal. That is not to say that it's not worthwhile to fix the lack of scoping in the spec... As part of this proposal or in a separate one, to decouple the orthogonal discussion threads.

Why did I screw this up so badly in my first draft of the proposal?

I don't think you have! It still make sense, but it just needs the change in framing that you suggest.

After such a revision, the proposal would not really be in a state to be approved, because it leaves a significant question open: should we use type families or custom constraints?

I'm not that familiar with what should and what shouldn't be part of the proposal, but the user-facing part here is primarily related to error messages. If we can make the impl so that users a) can't write ArrowStackTuple (w/e) in their code and give a guarantee that they should never see such constraints in an error message, I don't see why (3) should be part of the proposal. The discussion should be part of the MR, for sure, but it's not user-facing and hence doesn't need to be discussed as part of the proposal (IMO). What I gather should be part of the proposal, though, is which representation we pick for the arg tys. A flat tuple is a breaking change compared to nesting pairs like today (or like pre-7.8 IIUC).

But is your lack of motivation about the proposal or about the implementation? I sense that perhaps you are motivated to get this implemented, but less motivated to have a beautiful writeup of the various implementation choices?

I often feel this way, by the way... But writing a proposal often leads to a carefully-designed implementation, so it's not all in vain.

I still wonder if the right thing to do for arrows is to factor them out into a plugin or similar. They are little used, many issues have accumulated, and it would be a good demonstration of GHC being sufficient modular/extensible to support new syntax with interesting semantics.

This is a bunch of work up front, but gets a bunch of little-maintained code out of GHC, which I think is good because we have too many features. It also means @lexi-lambda is free to experiment with the implementation and semantics, without being bogged down by the requirements of this proposal process. Finally the others of us who would like to see something more like https://arxiv.org/pdf/1007.2885.pdf and https://github.com/conal/concat, and therefore have inherently conflicting goals, can use the same plugin foundation to explore in a different direction.

This seems like a great a win-in provided we can get over the initial factor-out hump: less junk collecting dust in GHC, more concurrent exploration of design space. Fundamentally, I think GHC needs to start shedding features for santiy's sake, and this seems like a good high-value place to begin.

But is your lack of motivation about the proposal or about the implementation? I sense that perhaps you are motivated to get this implemented, but less motivated to have a beautiful writeup of the various implementation choices?

I don’t think that’s really true… I’m not sure I’m much more excited to work on the implementation, either. :) But I would like to be able to call it done, since it would be a pity to have the work I’ve already done go to waste, and that requires doing more work, so I’d like to find the motivation to finish it regardless of how much it may or may not excite me.

I'm still not convinced it is. Which type variables may appear in t? Any?

Yes, fair enough… and in any case, I agree it would be useful clarification here.

I often feel this way, by the way... But writing a proposal often leads to a carefully-designed implementation, so it's not all in vain.

I agree, and I actually care quite a lot about getting the proposal into a good place. I would not be at all satisfied if the implementation were merged without feeling like the proposal and updates to the user’s guide were satisfactory, too. It’s just a matter of doing it!

I still wonder if the right thing to do for arrows is to factor them out into a plugin or similar. They are little used, many issues have accumulated, and it would be a good demonstration of GHC being sufficient modular/extensible to support new syntax with interesting semantics. […] It also means @lexi-lambda is free to experiment with the implementation and semantics, without being bogged down by the requirements of this proposal process.

This seems like a great a win-in provided we can get over the initial factor-out hump: less junk collecting dust in GHC, more concurrent exploration of design space. Fundamentally, I think GHC needs to start shedding features for santiy's sake, and this seems like a good high-value place to begin.

I don’t agree at all, but that’s probably neither here nor there at this point, anyway. Plugins are still too limited to support arrow notation satisfactorily, so as long as it’s in GHC (and I will certainly not be drafting any proposals to remove it), I figure it might as well work properly.