Kind Demotion (в отличие от Kind Promotion)

Расширение DataKinds поддерживает "значения" (т.е. конструкторы) в типы. Например, True и False становятся разными типами вида Bool.

То, что я хотел бы сделать, это наоборот, т.е. типы demote в значения. Функция с этой сигнатурой будет в порядке:

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

Я действительно могу это сделать, например, для Bool:

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

instance DemoteBool True where
  demoteBool _ = True

instance DemoteBool False where
  demoteBool _ = False

Однако мне придется писать экземпляры для любого типа, я хочу понизить его ценность. Есть ли более хороший способ сделать это, что не связано с большим количеством шаблонов?

Ответы

Ответ 1

Это одно из видов использования singletons, в частности fromSing:

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

Он по-прежнему включает в себя множество шаблонов, но пакет имеет многого, что уже определено, и я считаю, что он предоставляет Template Haskell, чтобы вы могли создавать свои собственные более легко (и с меньшим количеством кода).