小编Xia*_*ang的帖子

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

根据 Haskell 的库文档，Applicative 类的每个实例都必须满足四个规则：

• 身份： pure id <*> v = v
• 作品： pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
• 同态： pure f <*> pure x = pure (f x)
• 互换： u <*> pure y = pure ($ y) <*> u

然后它说作为这些规则的结果，底层的 Functor 实例将满足fmap f x = pure f <*> x。但是由于该方法fmap甚至没有出现在上述等式中，那么这个性质究竟是如何从它们得出的呢？