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 让您更轻松地生成自己的模板(并且代码更少)。