Haskell 等价于非类型的 C++ 模板

Question

我的一般理解是 Haskell 类型类与 C++ 模板在概念上有一些相似之处 - 即您可以定义函数或类型参数化的类型。但是，C++ 模板的一个有用特性是您也可以使用非类型模板参数。例如，维基百科有一个 great example 说明如何创建编译时阶乘。

理想情况下，我希望在 Haskell 中做同样的事情......而且我几乎可以使用 DataKinds 扩展名。以向量的经典示例为例，该向量在其类型中对其长度进行编码（取自here）。

data Nat = Ze | Su Nat

data Vec :: * -> Nat -> * where
  Nil  :: Vec a Ze
  Cons :: a -> Vec a n -> Vec a (Su n)

我希望能够将向量的类型级别“Nat”“降级”回值级别（可能使用ScopedTypeVariables），以便我可以使用它，因为可以使用 C++ 非类型模板参数作为常量值。 GHC.TypeLits 有点像 KnownNat 类中的一些骇客（它为每个具体文字伪造实例），但我显然不能自己在 Haskell 中编写。

我觉得我想要的东西是不可能的，但我想对为什么它可能不可能有一些直觉。

我觉得依赖类型潜伏在...

Answer 1

执行此操作的技术称为singleton types（该链接还链接到支持此功能的库）。

核心思想是创建一个参数化类型构造函数，以便类型的值和类型参数之间存在一一对应的关系。这是从上面链接中引用的第一篇论文中摘录的一个简化示例。

data SBool (a :: Bool) where
    STrue :: SBool 'True
    SFalse :: SBool 'False

现在只有一个SBool 'True 类型的值，即STrue。我们还通过 GADT 魔术知道，当我们在 SBool a 上进行模式匹配并得到 STrue 然后是 a ~ 'True。现在，回到值，我们使用基于类型选择值的正常机制：类型类。

class FromSBool (a :: 'Bool) where
    fromSBool :: SBool a -> Bool

instance FromSBool 'True where
    fromSBool STrue = True

instance FromSBool 'False where
    fromSBool SFalse = False

这是一个非常简单的例子，但是图书馆参考了更详细的论文，或者你可以直接使用图书馆。你说得对，类型级别的自然有点神奇。一个相关的库是 reflection 包，它可以让您将一个值推入一个类型并稍后取回。

如果你对其中的一些理论感兴趣，你可能也对论文Hasochism感兴趣。