Returning reified type using Data.Reflection in Haskell

Question

This is a question of type Data.Reflection in Haskell. Reflection allows me to take an Int and convert it to a type.

The functions f and g below are our best attempts at something reasonable, if you have a better way, let it be!

For example, I could add mod 41 numbers by doing something like:

import Data.Reflection import Data.Proxy newtype Zq qi = Zq i deriving (Eq) instance (Reifies qi, Integral i) => Num (Zq qi) where (...) zqToIntegral :: (Reifies qi, Integral i) => Zq qi -> i (...) f :: forall i . (Integral i) => i -> (forall q . Reifies qi => Zq qi) -> i f modulus k = reify modulus (\ (_::Proxy t) -> zqToIntegral (k :: Zq ti) 

Then

 >>:t (f 41 (31+15)) (f 41 (31+15)) :: Integral i => i 

However, we would like to write a function such as:

 g :: forall i . (Integral i) => i -> (forall q . Reifies qi => Zq qi) -> Zq qi g modulus k = reifyIntegral modulus (\ (_::Proxy t) -> (k :: Zq ti) 

and would like to receive:

 >>:t (g 41 (31+15)) (g 41 (31+15)) :: <some type info> => Zq qi 

The difference is that we would like to be able to return a type that uses reified int. At least one problem with the above definition is that the type of rank-2 q is not visible in the return type.

Signature for reify in Data.Reflection

 reify :: a -> (forall s. Reifies sa => Proxy s -> r) -> r 

which, as far as we know, requires a type of rank-2, and we do not know (if it is really possible) how to pass this type to the return type of the function.

Answer 1

You can raise the value to type. But the type cannot escape the function that makes the upgrade. This is how level 2 classes work. Imagine if we could write g as you described. Then, given some user input value, we could get the Zq qs variables at runtime.

But what can we do with them?

If we have two Zq with the same q , we can add them. But we would not know that they were the same or not until the time of execution! And it's too late for type checking, since we need to decide whether we can add them or not at compile time. If you ignore the fact that q is in the phantom position, it is for the same reason that you cannot have a function that returns Int or Bool at compile time based on input (you can use Either , of course).

So, as noted in the comment, you can do several different things.

One thing you can do is simply return the module (i.e. the q level version) at run time along with your result. Then you can always use it later.

It looks like this:

 g :: forall i . (Integral i) => i -> (forall q . Reifies qi => Zq qi) -> (i,i) g modulus k = reify modulus (\ m@ (_::Proxy t) -> (zqToIntegral (k :: Zq ti), reflect m)) 

Another thing you can do is use existential functions:

 data ZqE i = forall q. ZqE (Zq qi) h :: forall i . (Integral i) => i -> (forall q . Reifies qi => Zq qi) -> ZqE i h modulus k = reify modulus (\ (_::Proxy t) -> ZqE (k :: Zq ti)) 

Now the only thing we can do with our ZqE is to unzip it and return something else, which also does not reveal q directly in the type.

Please note that we are not able to know that q in any two ZqE are equal, therefore we cannot perform operations that combine them directly, but must create them all under the same reify call, and this is not a mistake, but a function!