Restricting functor arguments

[mikesperber]

We're currently implementing a Category that will execute on the GPU via Accelerate.

A recurring issue is that in Accelerate, we can have arrays of numeric types (and tuples of them), but not nested arrays.

This goes counter to ConCat.Category's OkFunctor class that assumes that functors nest arbitarily.

We can work around this for OkFunctor by making Ok imply type inspection, but no such luck with Additive1. The best I could come up with is making Typeable a prerequisite for Additive, like this:

https://github.com/active-group/concat/commit/c8006679ad34882c7517aabf111a4d3b05af2141

I tried making Typeable a prerquisite for additive1 instead, but this requires far more invasive and widespread changes, so I gave up eventually.

[conal]

How does type inspection help you with Accelerate's restriction on arrays?

[mikesperber]

We need an Additive instance for (our wrapper around) Accelerate's vector type like so:

instance (KnownNat n, Additive a) => Additive (Vector n a) where ...

... so that we can create an Additive1 instance like so:

instance KnownNat n => Additive1 (Vector n) where
  additive1 :: forall a. Sat Additive a |- Sat Additive (Vector n a)
  additive1 = Entail (Sub Dict)

In particular, we can't put more constraints in the context of the Additive instance because of Additive1.

Now, Accelerate restricts the things I can put in vectors via an Elt constraint - so I can't just put zero in them from Additive a. But Typeable lets me specialize to Double:

instance (KnownNat n, Additive a) => Additive (Vector n a) where
  zero
    | Just HRefl <- typeRep @a `eqTypeRep` typeRep @Double
      = Vector (Acc.use (Acc.fromList (Acc.Z Acc.:. fromInteger (natVal (Proxy :: Proxy n))) (repeat 0)))
    | otherwise = undefined

[conal]

Thanks for the motivation. It seems a shame to bypass type safety and introduce partiality. Maybe there's a better way.

[mikesperber]

The problem is that Additive1 and OkFunctor just do not hold.

Category.hs already has a sketch for switching categories upon fmapC, but that seems like a bridge too far for now.

Maybe instead of having an OkFunctor class constraint, just put Ok constraints on fmapC and descendants? (Haven't really thought this through all the way to the end.)

[conal]

Maybe instead of having an OkFunctor class constraint, just put Ok constraints on fmapC and descendants? (Haven't really thought this through all the way to the end.)

I don't know whether such an alternative could work out.

Explicit constraint entailment (including OkFunctor) may well be unnecessary now that GHC has quantified constraints. Even if we did eliminate entailment, however, I suspect that the basic problem with Accelerate incompatibility with Functor would persist.

[conal]

I guess one idea is to design an alternative to Functor with an associated constraint on element types (or maybe Accelerate already has one?)

[mikesperber]

Yes, Accelerate has one. (Acc.Elt) But making this something separate from FunctorCat would be super-awkward, as most of the functionality up to gradients would have to be re-written, with lots of duplicated code.

I contend the underlying problem is that FunctorCat stays within the same category. So adding one more workaround maybe isn't so bad?

[conal]

I contend the underlying problem is that FunctorCat stays within the same category. So adding one more workaround maybe isn't so bad?

Let's at least explore doing the right thing here. How would generalizing FunctorCat help?

[mikesperber]

Roughly, there'd be two "GPU categories", one for scalar computations, and the other one for arrays. FunctorCat would take you from one to the other.

[mikesperber]

The problem implementing that is that it would require a major overhaul of the plugin, which has a fairly deep-rooted assumption that there's only one category involved in a function application.

[mikesperber]

@conal I'm also hazy on how quantified constraints would help solve this problem. They allow encoding the implication differently, but it would still be an implication, no?

PS: Quantified constraints AFAICS aren't where we need them to be, see my attempt here:

https://github.com/mikesperber/concat/tree/quantified-constraints

[conal]

The problem implementing that is that it would require a major overhaul of the plugin, which has a fairly deep-rooted assumption that there's only one category involved in a function application.

Okay. Then let's look for a different principled solution rather than beginning (or continuing) a chain of unprincipled workarounds, each just a little worse than the preceding.

[mikesperber]

The problem implementing that is that it would require a major overhaul of the plugin, which has a fairly deep-rooted assumption that there's only one category involved in a function application.

Okay. Then let's look for a different principled solution rather than beginning (or continuing) a chain of unprincipled workarounds, each just a little worse than the preceding.

Just to be clear: I certainly didn't mean to suggest putting the Typeable hack in the mainline.

Do you have an idea in which direction you'd like to go?

[conal]

Just to be clear: I certainly didn't mean to suggest putting the Typeable hack in the mainline.

Oh! I may have misunderstood. Weren't you suggesting making Typeable a prerequisite for Additive?

[mikesperber]

Oh! I may have misunderstood. Weren't you suggesting making Typeable a prerequisite for Additive?

No, that's what we had to do to move forward with minimal changes. But you're right, I wasn't clear about what I wanted to do - sorry about that. I can see two rough directions:

• an OkFunctor f a associated constraint in FunctorCat
• an associated constraint analogous to Ok in Additive

I haven't worked either through, but will be happy to do it if you think a particular direction would be acceptable.