Reflect (undo) a DataKind promotion

Learn
1

Proxy is poly-kinded and so can be GADTs. Types can be promoted to kinds with the DataKinds extension. For certain types, it is possible to extract a value from a type proxy, e.g. the base module GHC.TypeLits provides ways to extract an integer or string when the corresponding type of kind Nat or Symbol is statically known. I feel this should be possible for any not too complicated monomorphic type. In some way, I am asking why the TypeRep of a promoted value can not be the value itself. The reflection package provides a type class Reifies for this with instances for a KnownNat and KnownSymbol.

Is there a uniform way for all kinds that were created using DataKinds? How to avoid the following boilerplate code?

data Ty = Foo | Bar | ... -- some monomorphic type

instance Reifies 'Foo Ty where
   reflect = const Foo
   -- ^ boilerplate, becomes unwieldy when Foo has arguments

Strangely, I can not mention a KnownSymbol constraint in an argument of a Ty constructor, or an “unpromotable context” arises.

Similarly to this situation I am trying to use DataKinds to define a type-safe term algebra. But in the end there shall be computations on the types of the terms (even if the type is statically known), whence I have to get my hands on the type as a value.

data Term :: Ty -> Type where
   FooT :: Term Foo
   -- etc.

typeOf :: Term ty -> Ty
typeOf = reflect
2

I have an experimental plugin that does this: GitHub - aaronallen8455/reflectacon: Plugin for working with promoted data constructors. I imagine a template haskell based solution should also be possible.

Edit: the singletons-th package provides a template haskell solution.

3 Likes
3

Nice!

but this won’t compile

newtype Wrapper = MkWrapper { unWrap :: Symbol } 
x = reflect @_ @(MkWrapper "hello")

Otherwise there’d have to be a value of type Symbol, which is not an inhabited type, instead of being able to convert it to String.

That was precisely what I had in mind: The terminals of my type hierarchy should be symbols. But I might as well leave the terminal type parameter open.

Now I understand that the Demote type family of singletons is doing what I described. The fact that one needs either externally-defined type families or type classes for reflection is a bit unfortunate, though. It would be nice if the reflectacon machinery was automatically in scope when using DataKinds. After all, the promotion part is.

1 Like