Is there such a "universal" type of Haskell?

Question

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

forall a. C a => ta -> 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 get universal quantification for all types a in class C to type A , so that the function t A → A returns a function for all a. Therefore, I assume that I am looking for a "universal" instance of class C in a certain sense ...

I looked at all kinds of fancy definitions for A line by line

 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) => tb -> b), 

or

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

or even

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

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

On odd days, I am convinced that type A simply does not exist, on even days I am convinced of the opposite ...

... so any help would be greatly appreciated!

---

To give some motivation for my question: I am strongly inclined towards the Edward Kmet advertising library for a neural network library , and on my first attempt I used my type Numeric.AD.Rank1.Kahn for automatic differentiation and backpropagation. This led to a good API, but was less efficient than its reverse mode, which unfortunately uses quantification, as in my question for encoding differentiable functions.

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

Answer 1

Suppose that such a “universal” type A exists.

Const () is passing, so 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 forall a. C a => a .

Please note that this was your first attempt at a solution - if it does not meet the requirements, then nothing will happen.

---

Now, in your particular case

 forall a. C a => a 

roughly, by definition, C (*) [Note: here I mistakenly “forget” the superclass of the class Floating a , magin the whole argument is much more fragile]

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

which is isomorphic to Double :

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

The proof that the above is really an isomorphism is nontrivial - I think that it requires some parametricity, as in "Recursive types for free!" . (The consequences of Yoneda? ... Comments are welcome!)

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

(*) I stretch things a bit. I don’t know how to accurately handle Haskell’s limited quantification, so I resort to making the dictionary explicit, even if, I think, it’s not exactly the same.