Kind降级(与Kind促销相对)

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，让您可以更轻松地生成自己的文件(并且代码更少)。