Support for linear arrows

[jeltsch]

The linear types extension should make it possible to work with a linear variant of arrows.

First, it should be possible to change the Arrow class such that it covers both the linear and the non-linear case. The crucial feature for this is multiplicity constraint polymorphism. Using the interface proposed in #10, the proposed new version of Arrow could be defined as follows:

class Category a => Arrow a where

    type ArrowMultiplicityConstraint a :: MultiplicityConstraint

    arr :: Function (ArrowMultiplicityConstraint a) b c -> a b c

    first :: a b d -> a (b, c) (d, e)

Second, it should be possible to use arrow notation also for linear arrows. This is important, since arrow notation is often crucial when working with arrows. The syntactic restrictions for linear arrows should probably be analogous to the ones for linear functions.

An open question is how to deal with promotion. Functions of types a -+ b can be promoted to functions of types a -> b, as I understand. Something similar could be useful for arrows in cases where an arrow type has both a linear and a non-linear variant. However, it is not clear to me at the moment, how such arrow promotion could be realized.

[aspiwack]

I will try to finish a robust monomorphic implementation before I make a polymorphic one. When the multiplicity-polymorphic implementation is out, you can define your own multiplicity-parametric Arrow type class to play with (and use -XRebindableSyntax to use it with the proper notation).

We've had some success using -XRebindableSyntax with variants of the Monad type class (e.g. here).

[aspiwack]

I'm not sure what your question about promotion is?

[jeltsch]

I’m not sure what your question about promotion is?

Say there are two variants of a certain arrow: a linear one, named -->., and a non-linear one, named -->. I would like values of a type a -->. b be automatically values of type a --> b, like values of type a ->. b (where ->. means ⊸) are automatically values of type a -> b through promotion.

[aspiwack]

I see.

Well, I don't see a reason why this could be done automatically as GHC does not provide an implicit user-defined coercion mechanism. I believe that you'll end up with two arrow types who happen to be related, but not trivially so. And you will have to problem: Haskell will not be able to see that the two types are related, and if it could, you cannot specify this relation in your type class.

[jeltsch]

I think it should be possible to use multiplicity polymorphism for what I want to achieve: I define a single type Arrow :: Multiplicity -> * -> * -> * and define aliases as follows:

type (-->.) = Arrow Linear
type (-->)  = Arrow Arbitrary

Whenever I do not need the features of Arbitrary (ω), I do not use Linear (1) as the first argument of Arrow, but a variable.

This brings me to a question: Why do we need promotion at all? We could just use multiplicity polymorphism also for linear functions. For example, instead of id :: a ->. a, we could have id :: a ->[m] a. What is actually the difference between a ->. b and forall m . a ->[m] b? Is it not so that you can use both in exactly the same ways?

[aspiwack]

It may be possible to use polymorphism if set right. But it's not entirely obvious: there is no subtyping between linear arrows and variable-multiplicity arrows.

I think it is possible to set it up so that linear arrows are subtypes of variable-multiplicity arrows (so that you can indeed have the two interchangeable types for id as you suggest). Though it is not clear at this time that it is desirable as it may prevent us from playing with the set of multiplicities: the two types you suggest are clearly different as soon as there is a multiplicity which means "variable used exactly twice" for instance (not that this is a particularly interesting multiplicity, but just for the sake of illustration)).

But even if we have this subtyping relation, it would not be sufficient: constructors have type C :: A ->. B ->. C but they very much don't have the type C :: A ->[p] B ->[q] C: it would behave very differently during pattern-matching.

Additionally, we cannot not have some amount of subtyping, really, as for f :: A ->. B, we can always do

g :: A -> B
g x = f x

As it happens, subtyping is elaborated as such an η-expansion, Core doesn't know of it.

[jeltsch]

When you say “arrows”, are you really talking about arrows (values of instances of the Arrow class), or are you talking about functions?

It may be possible to use polymorphism if set right. But it's not entirely obvious: there is no subtyping between linear arrows and variable-multiplicity arrows.

It should always be possible to replace a variable by something more concrete. For example, e :: forall a . [a] implies e :: [Int]; so e :: forall m . a ->[m] b should also imply e :: a ->[1] b.

I think it is possible to set it up so that linear arrows are subtypes of variable-multiplicity arrows (so that you can indeed have the two interchangeable types for id as you suggest). Though it is not clear at this time that it is desirable as it may prevent us from playing with the set of multiplicities: the two types you suggest are clearly different as soon as there is a multiplicity which means "variable used exactly twice" for instance […].

I see. The other direction would not work; e :: a ->[1] b would not imply e :: forall m . a ->[m] b.

At the moment, the types a ->[1] b and forall m . a ->[m] b are only interchangeable, because all multiplicities (1 and ω) cover the linear case.

But even if we have this subtyping relation, it would not be sufficient: constructors have type C :: A ->. B ->. C but they very much don’t have the type C :: A ->[p] B ->[q] C: it would behave very differently during pattern-matching.

What would be wrong with C having type forall p . A ->[p] B ->[q] C? This would mean that p is existentially quantified. During pattern matching, you would learn that there is a multiplicity p, but you would not learn which one it is; so you would have to use the fields of types A and B only linearly to be on the safe side. Or am I missing something?

Additionally, we cannot not have some amount of subtyping, really, as for f :: A ->. B, we can always do

g :: A -> B
g x = f x

I do not understand this. We can turn a value of type A ->. B into a value of type A -> B, and we can turn a value of type forall m . A ->[m] B into a value of type A -> B (by replacing m with ω).

[aspiwack]

When you say “arrows”, are you really talking about arrows (values of instances of the Arrow class), or are you talking about functions?

I meant function types, sorry.

What would be wrong with C having type forall p . A ->[p] B ->[q] C? This would mean that p is existentially quantified. During pattern matching, you would learn that there is a multiplicity p, but you would not learn which one it is; so you would have to use the fields of types A and B only linearly to be on the safe side. Or am I missing something?

No, you're right, that was a careless argument on my end. Though of course, if we only add affine function, we see where some amount of subtyping comes in handy (since both linear and affine function can be used where unrestricted functions are expected, and linear functions can be used where affine functions are expected). But this is not a full-blown support for subtyping: basically the motto is subtyping for first-order things, and polymorphism for higher order things. (in fact, there is no subtyping at all in Core, the idea is that subtyping opportunities detected by the type-checker are elaborated into η-expansions.