haskell - 从评估级别访问 GADT 约束

Question

我试图利用运行时的一些 GADT 参数，假设我已经使用DataKinds扩展来允许将数据提升为类型。即拥有

data Num = Zero | Succ Num
data Something (len :: Num) where
  Some :: Something len

我想有功能

toNum :: Something len -> Num

任何人Some :: Something n都会返回n：

toNum (s :: Something n) = n

这在 Haskell 中是无效的。有可能这样做吗？

标签： haskelldependent-typegadt

Answer 1

在 Haskell 中这是不可能的，因为类型在运行时被擦除。也就是说，当程序运行时，内存中没有关于let类型中索引值的信息。

为了克服这个问题，我们需要强制 Haskell 在运行时将该值保存在内存中。这通常使用单例辅助类型来完成：

data Num = Zero | Succ Num

data SNum (n :: Num) where
   SZero :: SNum 'Zero
   SSucc :: SNum n -> SNum ('Succ n)

data Something (len :: Num) where
  Some :: SNum len -> Something len

使用它，您可以轻松编写

sToNum :: SNum n -> Num
sToNum SZero = Zero
sToNum (SSucc n) = Succ (sToNum n)

接着

toNum :: Something len -> Num
toNum (Some n) = sToNum n

如果您查找“haskell singletons”，您应该会找到几个示例。甚至还有一个singletons库可以部分自动化。

如果/何时发布“依赖 Haskell”，我们将拥有更少繁琐的工具可供我们使用。目前，单身人士可以工作，但有时会很麻烦。不过，就目前而言，我们必须使用它们。