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?

Overburden

The reason you have to do it manually is partiality. Given a type-level b :: Bool you don't know for certain that it's either True or False. It could be a stuck type. A singleton proves that its type isn't stuck. Dependent Haskell will help a bit for this particular case, because True and 'True will be the same thing, but there are still unavoidable problems with partiality. – Downstairs

@BenjaminHodgson does the existing TypeInType help at all here, or is that unrelated? – Empyrean

It would be fun if strict fields when lifted could not contain stuck types, much like a strict field cannot contain bottom. I just want to be able to scope over a :: !Bool and use it in the code :) – Empyrean

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).

Meddlesome

ps : kind demotion is a particular example of a "comprehension". promotion and demotion are adjoints to each other in a very specific 2-category. many powerful operations could be written that way. – Hanse