从评估级别访问GADT contstraint

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中无效.有可能这样做吗？

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"将被释放,我们将拥有更少的繁琐工具供我们使用.目前,单身人士工作,但有时他们很麻烦.不过,目前我们还是要使用它们.