亲切降级(与善意促销相对)

Question

所述DataKinds扩展促进"值"(即构造函数)分为不同的类型.例如,True并False成为不同类型的种类Bool.

我想做的是相反的,即将类型降级为值.具有此签名的函数可以正常:

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

但是,我必须为我想要降级到它的价值的任何类型编写实例.有没有更好的方法来做这个不涉及太多的样板？

Answer 1

这是其中一个用途singletons,特别是fromSing:

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

它仍然涉及很多样板,但是包已经定义了很多,我相信它提供了模板Haskell,让你更容易生成自己的(并且代码更少).