Haskell相当于C++模板而不是非类型

Haskell equivalent to C++ template over non-types

本文关键字：是非 类型 相当于 C++ Haskell      更新时间：2023-10-16

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

理想情况下，我想在哈斯克尔做同样的事情......我几乎可以使用DataKinds扩展。以一个向量的典型示例为例，该向量将其长度编码为其类型（取自此处）。

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++非类型模板参数作为常量值。全康。TypeLits 在 KnownNat 类中通过一些黑客来做到这一点（它为每个具体的文字伪造实例），但我显然不能自己在 Haskell 中编写这个。

我

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

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

执行此操作的技术称为单例类型（该链接还链接到库以支持此类型）。

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

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

这是一个非常简单的例子，但图书馆引用的论文涉及更多详细信息，或者你可以只使用库。 你是对的，类型级别的自然有点神奇。 相关的库是反射包，它允许您将值推入类型并在以后取回。

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

相关文章：