Kind Demotion (as opposed to Kind Promotion)

Question

The DataKinds extension promotes "values" (i.e. constructors) into types. For example True and False become distinct types of kind Bool.

What I'd like to do is the opposite, i.e. demote types into values. A function with this signature would be fine:

demote :: Proxy (a :: t) -> t

I can actually do this, for example for Bool:

class DemoteBool (a :: Bool) where
  demoteBool :: Proxy (a :: Bool) -> Bool

instance DemoteBool True where
  demoteBool _ = True

instance DemoteBool False where
  demoteBool _ = False

However, I'd have to write up instances for any type I want to demote back to it's value. Is there a nicer way of doing this that doesn't involve so much boilerplate?

Answer 1

That is one of the uses of singletons, in particular fromSing:

ghci> :m +Data.Singletons.Prelude
ghci> :set -XDataKinds
ghci> fromSing (sing :: Sing 'True)
True

It still involves a lot of boilerplate, but the package has a lot of it already defined and I believe it provides Template Haskell to let you generate your own more easily (and with less code).