Fix Haskell's arrow notation

[tomjaguarpaw]

[lexi-lambda]

The trouble with making commands less second class is that they fundamentally involve a complex notion of lexical closure. Given a command f -< e, e may refer to “arrow-local” variables. This command may be passed to a control operator like handle, but it does not close over its free variables, as they must be threaded through the operator explicitly. This is where the environment-passing of proc’s desugaring comes in.

For a command to stand on its own, it needs to include information about which variables are free in its body within its type. This is complicated, as it requires a kind of extra dimension of information than types normally contain.

For a way to encode this, one could imagine an entirely new kind of type, an Id. These are not ordinary Types, nor are they Symbols—you could think of them kind of like hygienically-scoped identifiers. In that sense, they would be related to Template Haskell’s 'Name and ''Name quotations (though unfortunately that syntax is already stolen at the type level for data kinds). An Id would behave kind of like a skolem, but instead of being scoped by a forall, they are implicitly scoped by the placement of the term-level binder.

Using this new Id kind, a command could be given the type

Command :: IdBag -> [Type] -> Type -> Type

where the IdBag contains the command’s free variables, the [Type] is the argument stack, and the Type is the return type. However, implementing this Id kind would obviously be a pretty radical change to the type system for arrows, which would be a pretty tough sell!

[tomjaguarpaw]

I think your Command type describes the command type from Definition 3 (page 5) of http://www.staff.city.ac.uk/~ross/papers/notation.html (although the arrow type itself seems to be missing from your version).

[lexi-lambda]

Yes, they are related, though I think the command type given by Definition 3 lacks the information about the free variables, which is the biggest obstacle to a command standing on its own. Take a look at Type and Translation Rules for Arrow Notation in GHC, and note how the context of arrow-local variables (named Δ) is interwoven with both typechecking and desugaring rules.

My ArrowEnv type family given in my proposal, and the corresponding Σ form in my typechecking judgements, is closer to my Command type described here. However, there is still a key difference: in the current typechecking rules and my proposal, the environment threading only appears explicitly in the typechecking rule for (| e c ... |); in other rules the environment threading is implicit. This is precisely because the notation is so aggressively first order: the (| e c ... |) rule is the only place where some second-order behavior sneaks in, and even there, it’s highly constrained.

If you want commands to be real values, it becomes possible to move them out of their current context into some other context entirely, and the assumptions made by the current rules for proc no longer apply. Therefore, you have to move a lot more information into the type system to ensure that the eventual use site where the command ends up still includes the necessary context, and captures the necessary information to wire up the command’s inputs to the corresponding values in its context during desugaring.

[tomjaguarpaw]

Isn't your IdBag the thing on the LHS of Paterson's ~>?

[lexi-lambda]

Oh, I suppose you are right. But Paterson’s ~> is really just using an extra argument on the argument stack to thread the environment through a control operator using a compiler-defined representation; it is guaranteed to work because the thing on the LHS (the b in b ~> θ) is universally quantified. Paterson punts on the idea of the sort of “relocatable” command I describe above. Things only work because the skolem in the type assigned to control operators ensures the environment is threaded to the operator’s arguments, so the first-order nature of the rest of the system can be maintained.

[tomjaguarpaw]

I would love an arrow syntax that allowed the types to look like the curried function types that we're used to in Haskell. For example, instead of

keyed :: Rule m (e, k, a) b -> Rule m (e, Map k a) (Map k b)

to have something like (following Paterson's notation)

keyed :: (k ⇀ a ⇀ Rule m \ b) -> (Map k a ⇀ Rule m \ Map k b)

This looks a lot like the monadic version would

keyed :: (k -> a -> Rule m b) -> (Map k a -> Rule m (Map k b))

But even if we could get ⇀ to mean something sensible we still need to handle the environment, as you mentioned above.

keyed :: (k ⇀ a ⇀ e ⇀ Rule m \ b) -> (Map k a ⇀ e ⇀ Rule m \ Map k b)

This looks less pleasant, but it's still workable.

[tomjaguarpaw]

I think we probably have to put the environment into the terminal type constructor. Can we have something like

data Command arr env =
    A arr env Type
  | (⇀) Type (Command arr)

[lexi-lambda]

The issue I was alluding to above is that it isn’t clear what env ought to be instantiated with. What do you put there? It can’t be a tuple, since that just describes the types of things, but you can’t connect the types to particular variables in scope without more information. It can’t be a mapping from variable names to types, as variables can be shadowed. So you need something more—and that brings in all the complexity of the hypothetical Id kind.

[tomjaguarpaw]

Oh, I assumed that keeping it polymorphic would always be fine.

[lexi-lambda]

If you can take the command out of its context and pass it around, where does the quantifier go?

[tomjaguarpaw]

Hmm, it feels like keeping it polymorphic a la ST should be sufficient, but I may not be imagining the same sorts of things that you are.

[lexi-lambda]

To be a little less cryptic, let me put it another way. When GHC checks a control operator against a polymorphic type, that’s okay, because a control operator isn’t a command, but a command maker. All that polymorphic type is saying is that the command maker needs to work on commands with any environment, and it needs to treat them all equivalently. That’s fine.

But GHC never assigns a polymorphic type to the environment of an actual command itself. That would be a big problem! If a command is given the type ∀ env. Command env args a, that implies it has to work with any environment… which would mean the term would have to be closed. No good. Dually, if a command is given the type ∃ env. Command env args a, that would mean the caller has to be able to provide any environment, which is also no good.

So after GHC checks a control operator against the polymorphic type, it actually immediately instantiates it to a concrete type before continuing with typechecking. It only uses the polymorphism to ensure the control operator can’t observe the concrete type, since it’s an implementation detail.

Put yet another way, the polymorphism in a control operator is simply a way of ensuring two environments are exactly the same (specifically, the input environment to the resulting command and the input environment to its arguments). It pins a relationship between two commands. If you want a command to be able to stand on its own, there’s no relationship you can take advantage of, there’s just an environment, so you can’t get away with the polymorphism trick.

[tomjaguarpaw]

This is an "embedded" version of the typing rules that I'm imagining. I've used GADTs rather than TypeFamilies as I prefer to keep things explicit. That implies a certain amount of syntactic noise though. It wouldn't leak through to the user though.

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE TypeOperators  #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds      #-}

import GHC.Types
import Control.Arrow
import Control.Category

data CG type_ = A type_ | (:->) type_ (CG type_)

infixr :->
infixr :->.

type (:->.) (a :: k) (b :: k) = a :-> A b

data Command arr env c where
  I :: arr env b -> Command arr env (A b)
  K :: Command arr (env, a) b
    -> Command arr env (a :-> b)

data CO f c where
  J :: f b -> CO f (A b)
  L :: (f b -> CO f c) -> CO f (b :-> c)

type ControlOperator arr env = CO (Command arr env)

originalKeyed :: (Eq k, Applicative m)
              => Rule m (e, k, a) b
              -> Rule m (e, Map k a) (Map k b)
originalKeyed = undefined

keyed :: (Eq k, Applicative m)
      => ControlOperator (Rule m) env
         ((k :-> a :->. b) :->. (Map k a :->. Map k b))
-- It's the type that's important.  The implementation is too messy to
-- care about looking it.
keyed = L (\x ->
  let K (K (I x')) = x
      mungeArguments = (arr (\(x, y, z) -> ((x, y), z)) >>>)
  in  J (K (I (originalKeyed (mungeArguments x')))))

-- Irrelevant cruft:

data Map k v
-- Only doing this proxy business to avoid turning on KindSignatures
data Rule m a b = Rule (Proxy (m a))
data Proxy a = Proxy

instance Category (Rule m)
instance Arrow (Rule m)

[EDIT: Improved names] [EDIT2: Generalised to a jaw-dropping degree]

[tomjaguarpaw]

Naively, I expect the env to a similar role to the polymorphic return type in the holey monoid and various Cont tricks*. I expect it to either end up looking like a -> b -> c -> ... -> env or (a, (b, (c, ... env))) depending on which way it happens to work out in practice!

• NB: Not as I said before the same role as the fully polymorphic s in ST.