c++ - Haskell 等同于非类型上的 C++ 模板

Question

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

理想情况下，我想在 Haskell 中做同样的事情……而且我几乎可以使用 DataKinds 扩展。以 vector 的经典示例为例，该 vector 在其类型中对其长度进行编码(取自 here )。

data Nat = Ze | Su Nat

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

我希望能够将 vector 的类型级别“Nat”“降级”回值级别(可能使用 ScopedTypeVariables)，这样我就可以使用它了使用 C++ 非类型模板参数作为常量值。 GHC.TypeLits有点像 KnownNat 类中的一些 hackery(它为每个具体文字伪造实例)做这件事，但我显然不能用 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 .