Dupable wars : implementation

[tbagrel1]

No description provided.

[aspiwack]

What I would like to see, as well, is a function in Data.Array.Mutable.Linear which defines an array from a Replicator. To test the Replicator API.

[aspiwack]

You don't have access to the Applicative class at this point†, but you should have a pure and a (<*>) function nonetheless. For both types.

We will probably need other functions, like a function Replicator %1 -> RepStream.

† Sometimes I feel as though this library should all be one big Internal file where everything is mutually recursive, and then we use the file hierarchy purely for exports.

[aspiwack]

Random thought: should we use unboxed pairs (and unit) in the projections? Maybe it'll be better?

[tbagrel1]

If we use unboxed tuple for the dups projector, then it becomes harder to write dupR in terms of dup2 (or we should also change the dup2 signature to use unboxed tuples).
I don't know how to write an unboxed unit, but if we return some in the consumes projector, then writing consume (from Consumable) for ReplicationStream is also less trivial.
I also tried to use unboxed tuples in the Applicative instance for ReplicationStream (for <*>), but AFAIK, it's not possible because the projections cannot receive an unboxed tuple as a function parameter.

Also, without 9.2, I don't see how we can actually write this:

dupsf sf' & \case
  (# sf1, sf2 #)

We need the func_call & lambda_case syntax here for linearity, but because the result of the function call is now passed as an argument to &, then unboxed tuples are not allowed in that position.

[treeowl]

Unboxed unit is (##).

[aspiwack]

Well, let's wait 9.2 before we decide to revisit this issue, then. It's not worth agonising over.

[aspiwack]

I pushed a little something to restore the backward functional
dependency.

As I see it, there are two solutions:

1. Remove the n argument from the Elim type class arguments
   altogether. It is effectively redundant, after all. This removes
   all functional dependencies.
2. We need to tell the compiler how to compute n from f and
   b. One way to convince oneself that GHC cannot know that n is
   effectively determined by f is to consider what would happen if
   we added an instance Elim 42 a b b? We need to make this
   impossible!

While (1) is definitely the simpler solution, I went for (2) in my
commit, because I do like the idea of having the option of saying
elim @7 when the function type is under-determined. Rather than
having to state the entire function type.

What this implied is making a type family Arity b f which computes
the arity of f (assuming its headed by b). And force n ~ Arity b f as a super-class constraint. This way, no instance 42. This
suffices to convince GHC.

What I don't know if why I had to add Arity b (a %1 -> b) = 1, this
should follow from the definition. But when I remove it, Haskell is
very unhappy.

[tbagrel1]

Should I redefine Arity when writing V.Elim, or should we share it someway?

Also, I was wondering yesterday, could we add a 2 <= n extra constraint on the last Elim n a b f instance instead of creating overlapping ones? What would be the cost of such a measure?

[aspiwack]

Should I redefine Arity when writing V.Elim, or should we share it someway?

I guess it's better to use the same.

Either way, it gives some pretty unappealing types, so we will have to give pretty solid documentation to elim.

Also, I was wondering yesterday, could we add a 2 <= n extra constraint on the last Elim n a b f instance instead of creating overlapping ones? What would be the cost of such a measure?

Unfortunately it wouldn't work. GHC only looks at the instance's head (the part to the right of the =>) to determine if instances are overlapping. You could add this constraint, but it would never apply.

[tbagrel1]

Do you see where we could but the Arity thing so? In Data.Unrestricted.Linear.Internal.Arity?

Unfortunately it wouldn't work. GHC only looks at the instance's head (the part to the right of the =>) to determine if instances are overlapping. You could add this constraint, but it would never apply.

I would have used something like Elim (n + 1) a b f) => Elim (n + 2) a b (a %1 -> f) then, if only we could.

[aspiwack]

Do you see where we could but the Arity thing so? In Data.Unrestricted.Linear.Internal.Arity?

I guess. There is no good place where to put it anyway. The relation with Unrestricted is kind of dubious, though. Maybe Data.Linear.Internal.Arity instead?

[facundominguez]

I came to have some fun explaining the code. I shared some suggestions for documentation that I think could be helpful.

[aspiwack]

I should add: this is another PR that got bigger than we planned. We should be more careful for the next ones.

[tbagrel1]

Why are we deriving Prelude (non-linear) versions of Eq, Ord, and especially Functor for V?

[aspiwack]

Why are we deriving Prelude (non-linear) versions of Eq, Ord, and especially Functor for V?

I don't remember for sure. But if I had to guess, it's because we wanted V n a to behave as much as possible as (a, …, a). We'd need a multiplicity polymorphic elim for this to work completely, though. We may have to wait until we are fully committed to 9.2 for this to work fine though. It may be worth a try (in a separate PR).

elim :: forall p n a b. (a %p -> … %p -> b) %1 -> V n a %p -> b

[aspiwack]

I've got some comments on the documentation. You can address them then merge.