Make reify polykinded

[treeowl]

Currently, we have

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

I believe we probably want something more like

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

I have no particular opinion on the order of the type variables. Is there some fundamental reason this won't work? Is there some fundamental reason it's not desirable?

[mitchellwrosen]

What's the use case for this?

[WorldSEnder]

I'm not sure if this is what @treeowl originally had in mind. I have a small proof of concept library here, where reify is modified so that different kinds reflect different types of values.

reify :: Reifiable a => a -> (forall (s :: ReifyKind a). ReifyConstraint a s => Proxy s -> r) -> r

The interesting point is that some kinds, e.g. Nat, give you power by allowing to compare for equality, and the constraint Reifies s a is too weak to represent that. The mantra would be approximately "Different types of values are reflected by different kinds of variables".

It allows one to write stuff like

program :: forall s t. (ReifyComparable s t, Reifies s Integer, Reifies t Integer)
        => Proxy s -> Modulus s -> Proxy t -> Modulus t -> Integer
program tokenn valuen tokenm valuem =
  case testSameReification tokenn tokenm of
    Just Refl -> unMod (valuen + valuem)
    Nothing -> -1

and uniformly handles the currently four different reify, reifyTypeable, reifyNat and reifySymbol from this library (the above program is only callable with values from reifyTypeable and reifyNat and equality you get from reifyTypeable tests for equality of the StablePtr in the background, not the value`)

Again, it's only a proof of concept and I'm not sure how good of a real-world use case this actually is.

[treeowl]

I didn't have any particular application in mind. It just seemed a bit weird to restrict the kind. The downside of generalization, theoretically, is that if future Haskell has forall (x :: ()). x :~: '() then things will go wrong.

[zoranbosnjak]

It's my first attempt to use this library, so it is likely that I am doing something wrong. But from the original problem description it also looks like I hit exactly this problem in a real usecase.

I am trying to describe a 'schemas' with types (something like the servant does for the web API). The problem I am trying to solve with this library is to be able to select schema at runtime (for example a user preference) and still use type safe functions. Here is a simplified example (reflection-test.hs):

{-# LANGUAGE DataKinds #-}                                                                                 
                                                                                                           
import Data.Proxy                                                                                          
import Data.Reflection                                                                                     
import GHC.TypeLits                                                                                        
                                                                                                           
-- | Schema shape                                                                                          
data TL = TL Nat Nat -- type level schema                                                                  
data VL = VL Int Integer -- value leval schema                                                             
                                                                                                           
-- | Convert schema from type level to value level                                                         
instance (KnownNat m, KnownNat n) => Reifies ('TL m n) VL where                                            
    reflect _proxy = VL (fromIntegral $ natVal (Proxy @m)) (natVal (Proxy @n))                             
                                                                                                           
-- | Concrete schema examples, defined as types                                                            
type T1 = 'TL 1 0                                                                                          
type T2 = 'TL 2 3                                                                                          
type T3 = 'TL 3 0                                                                                          
-- ... more schemas are possible                                                                           
                                                                                                           
-- | Data type for actual data                                                                             
data Item (t :: TL) = Item [Integer] deriving Show                                                         
                                                                                                           
-- | Example type safe function to create item of requested type.                                          
mkItem :: forall t. Reifies t VL => Item t                                                                 
mkItem =                                                                                                   
    let (VL a b) = reflect (Proxy @t)                                                                      
    in Item (replicate a b)                                                                                
                                                                                                           
main :: IO ()                                                                                              
main = do                                                                                                  
    print (Item [0] :: Item T1) -- manually create item                                                    
    print (mkItem @T1) -- item created by concrete type                                                    
                                                                                                           
    -- Create item in a type safe way (using mkItem), but                                                  
    -- depending on some run-time value 'sch'.                                                             
    let sch :: VL                                                                                          
        sch = reflect @T1 Proxy                                                                            
                                                                                                           
    reify sch (\(p :: Proxy t) -> print (mkItem @t))

The error is:

reflection-test.hs:40:50: error:
    * Expected kind `TL', but `t' has kind `*'
    * In the type `t'
      In the first argument of `print', namely `(mkItem @t)'
      In the expression: print (mkItem @t)
   |
40 |     reify sch (\(p :: Proxy t) -> print (mkItem @t))

Is this the same problem?
Is there any way to work around it?
Is there any better way to select a schema at run-time?

I appreciate any suggestion.

[RyanGlScott]

I just came across this issue myself, and I am also inclined to agree that it makes more sense for reify to be poly-kinded. Aside from the reasons above, it's quite weird for reflect to be poly-kinded (as it is currently) but not reify.

Historically, I think the reason this wasn't the case is because you would have to define Magic like so:

newtype Magic a r k = Magic (forall (s :: k). Reifies s a => Proxy s -> r)

And this simply wasn't possible prior to the introduction of TypeInType in GHC 8.0. This isn't a problem in GHC 8.0+, however. If we wanted to pursue making reify poly-kinded (and I think it makes good sense to do this), then I would propose that we simply make reflection require GHC 8.0 or later to build.

Another hiccup is that it's not clear to me how to make the API in the slow subdirectory work with a poly-kinded reify. I don't think this is a deal-breaker, however, since the API in the slow subdirectory is already quite different from what is offered in the fast subdirectory.

[zoranbosnjak]

@RyanGlScott is there any quick fix possible to the library, such that I could run the example above and maybe some more experiments? It is OK if it's on a separate branch/fork, until all the details are sorted out.

[RyanGlScott]

I've pushed a branch to T34, if you'd like to try it out.

[zoranbosnjak]

@RyanGlScott , thanks.
With T43 branch, the example above works as expected.