17

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?

Alec
  • 31,829
  • 7
  • 67
  • 114
Clinton
  • 22,361
  • 15
  • 67
  • 163
  • 2
    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](https://typesandkinds.wordpress.com/2015/09/09/what-are-type-families/). 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. – Benjamin Hodgson Nov 22 '16 at 13:54
  • @BenjaminHodgson does the existing `TypeInType` help at all here, or is that unrelated? – porges Jul 05 '17 at 05:28
  • 1
    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 :) – porges Jul 05 '17 at 06:17

1 Answers1

13

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

David Young
  • 10,713
  • 2
  • 33
  • 47
  • 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. – nicolas Jan 29 '22 at 13:58