haskell - 同类降级(与同类促销相反)

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

但是，我必须为我想降级为它的值的任何类型编写实例。有没有更好的方法来完成这些工作而不涉及太多样板工作？

最佳答案

那是 singletons 的用途之一，尤其是 fromSing :

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

它仍然涉及很多样板，但是该包中已经定义了很多样板，我相信它提供了模板Haskell，使您可以更轻松地(更少的代码)生成自己的模板。