使用“DataKinds”从 Haskell 类型中提取参数

Question

GHC 的DataKinds扩展允许定义由某些数据参数化的类型。是否有一些可能的方法可以在函数定义的 RHS 上使用这些参数？例如，在 Agda 中，我可以直接从向量的类型中提取向量的长度，而无需计算其构造函数：

length : Vec A n -> Nat
length {n = n} _ = n

Haskell 有没有可能做到这一点？

我对此感兴趣的原因是因为我认为这对我正在做的一个项目很有帮助，该项目是一个自定义 Haskell 库，用于以类型安全的方式调用 Java（尽可能安全）。我认为，与其使用单一类型来表示所有 Java 对象，不如使用一个由 Java 类名参数化为字符串的类型（例如JObject "java.math.BigDecimal"），这样 Java 中不同类的实例在 Haskell 中的表示形式也将具有不同的类型。如果我在这里问的是可能的，那么它将允许从方法的给定 Haskell 类型自动计算 JNI 类型签名字符串，以便我可以编写类似的内容

length : Vec A n -> Nat
length {n = n} _ = n

Answer 1

在 Haskell 中，类型被删除，它们在运行时不存在。DataKinds允许您在类型中使用数据构造函数，但它们仍然会被删除。在 类型的函数中forall n. Vec A n -> Nat，不可能返回，n因为它将被擦除。

为了n不被删除，您将拥有一个Vec A n依赖于运行时值的类型n，这就是依赖类型的含义。

依赖类型还不是 Haskell 的原生功能。但是，可以使用singleton来模拟它们。的类型length将为forall n. SingI n => Vec A n -> Nat，其中SingI约束提供 的运行时反射n。