Does such a "universal" Haskell type exist?

Question

I am looking for a Haskell type A with the following property (using exotic GHC extensions is fine with me...): For all traversable t, the following two types are isomorphic:

forall a. C a => t a -> a

and

t A -> A.

In my specific case, C is the following class:

class Floating a => C a where
    fromDouble :: Double -> a

In other words, I somehow would like to pull the universal quantification over all types a in class C into the type A, so that a function t A -> A gives me back a function for all a. So I guess I'm looking for a "universal" instance of class C in a certain sense...

I have considered all sorts of fancy definitions for A, along the lines of

newtype A = A (forall b. C b => b)

or

data A = forall b. C b => A b

or

newtype A = A (forall t b. (Traversable t, C b) => t b -> b),

or

data A = FromDouble Double | Plus A A | Tanh A | ...

or even

data A = A (forall t. Traversable t => t A -> A),

and they can all easily be made instances of class C, but they don't have the property I need (or at least I don't see how to get that property from any of my above definitions).

On odd days I am convinced type A simply doesn't exist, on even days I'm convinced of the opposite...

...so any help would be highly appreciated!

---

To give some motivation for my question: I am heavily leaning on Edward Kmett's ad library for my neural networks library, and in my first attempt, I was using his Numeric.AD.Rank1.Kahn type for automatic differentiation and backpropagation. This led to a nice API, but was less efficient than his reverse mode, which unfortunately uses a quantification as in my question for encoding differentiable functions.

I was hoping that I could have the best of both worlds - one specific (abstract) type plus reverse mode efficiency.

Answer 1

Let's assume such a "universal" type A exists.

Const () is traversable, hence we get an isomorphism between

forall a. C a => Const () a -> a
-- and
Const () A -> A

i.e. between (since Const () a is isomorphic to (), and () -> b is isomorphic to b)

forall a. C a => a
-- and
A

So, if any A exists, it must be isomorphic to forall a. C a => a.

Note that this was your first attempt at a solution -- if that does not satisfy the requirements, then nothing will.

---

Now, in your specific case

forall a. C a => a

roughly means, by definition of C (*) [Note: here I am wrongly "forgetting" the Floating a superclass, magin the whole argument much more fragile]

forall a. (Double -> a) -> a

which is isomorphic to Double:

iso :: Double -> forall a. (Double -> a) -> a
iso x f = f x
osi :: (forall a. (Double -> a) -> a) -> Double
osi f = f id

Proving that the above is really an isomorphism is non-trivial -- I think it requires some parametricity as in "Recursive types for free!". (Consequence of Yoneda? ... Comments welcome!)

So -- if there is a solution, for your C, it has to be A ~ Double, up to isomorphism.

(*) I'm stretching things a bit here. I don't know how to precisely handle Haskell's bounded quantification, so I resort to making the dictionary explicit, even if, I guess, it's not exactly the same.