haskell - 亲切的降级（相对于亲切的晋升）

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

它仍然涉及很多样板，但是包已经定义了很多，我相信它提供了 Template Haskell 让您更轻松地生成自己的模板（并且代码更少）。