logo标签列表

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

haskelltypesdata-kindstype-kinds
4
GHC的DataKinds扩展允许定义由某些数据参数化的类型。是否有可能在函数定义的右侧使用这些参数？例如，在Agda中，我可以直接从向量的类型中提取其长度，而无需对其构造函数进行计算。
length : Vec A n -> Nat
length {n = n} _ = n

在Haskell中有可能以某种方式实现这个吗？

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

method <- findMethod "toString" :: IO (JMethod (JObject "java.math.BigDecimal") (IO JString))
3个回答
5
在Haskell中，类型被擦除，在运行时不存在。`DataKinds`允许你在类型中使用数据构造函数，但它们仍然会被擦除。在类型为`forall n. Vec A n -> Nat`的函数中，不可能返回`n`，因为它将被擦除。
为了使`n`不被擦除，你需要一个依赖于运行时值`n`的类型`Vec A n`，这就是依赖类型的含义所在。
依赖类型并不是Haskell的本地特性（尚未）。然而，可以使用singletons来模拟它们。`length`的类型将变为`forall n. SingI n => Vec A n -> Nat`，其中`SingI`约束提供了对`n`的运行时反射。
3
在Haskell中，类型在运行时并不存在。它们仅用于对源代码中的表达式进行分类，而不是运行时的值。
你当然可以使用data JObject (className :: Symbol) = ...，并使用它来强制确保只有某个特定Java类的对象才能使用某个函数，而不能给定一个不同类名的JObject。你甚至可以确保在多态上下文中，即使你不知道实际的类名是什么，也不会给定不匹配类的JObject来组合两个相同类的Java对象。但所有这些都是关于你的代码的讨论。在运行时，当实际的JObject存在于内存中时，它根本不包含className。没有任何东西可以提取出来。

然而，有可能制作出一些具有将className作为值而不是类型访问的效果的东西。你需要的是一个可以调用的函数，该函数以className Symbol为参数，将生成一个运行时的String值。在Haskell中，为了使一个函数对类型参数的每个可能值具有不同的行为，通常使用类型类。你只需要一个带有给出String值的方法的类，然后为每个实现该方法并返回相应String的可能Symbol创建一个实例。简单！

幸运的是，GHC实际上有一个内置类，其中包含了每个Symbol的魔术实例，所以没有人需要手动编写所有这些实例。它被称为KnownSymbol。方法symbolSing @s实际上给你的是一个SSymbol s而不是直接给你String，但你可以通过调用fromSymbol来获取它。

除了神奇地拥有无限数量的离散实例之外，KnownSymbol类是一个完全普通的类。这意味着如果你只有一个类型参数化为未知Symbol的情况下，你不能自动获得一个KnownSymbol实例；你必须确保在函数中使用正确的约束条件，从选择Symbol的地方流经KnownSymbol实例，到你想要知道它是什么的地方。

SSymbol 类型是一种称为“单例”（不要与面向对象语言中的“单例模式”混淆）的技术示例。它意味着一个参数化类型，其值与类型参数的选择一一对应。例如，SSymbol s 是每个 Symbol s 选择的一个独立类型；每个类型只有一个值（因此称为“单例”），因此知道我们拥有的值可以揭示其对应的 Symbol，即使在运行时 Symbol 实际上并不存在。使用这些单例类型作为链接可以提供比直接链接类型和值的类更多的选项，尽管在简单情况下并不一定需要。如果您感兴趣，singletons 库 是一个更通用地定义和处理单例类型的框架（与由于需要编译器支持的“魔法实例”而提供的非常少数的单例类型不同）。
1
这实际上是可行的。演示:
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE GADTs #-}
    
  import GHC.Types
  import GHC.TypeLits
  import Data.Proxy

  data JavaObj :: Symbol -> * where
     JavaObj :: JavaObj a

  getJavaObjClassName :: KnownSymbol a => JavaObj a -> String
  getJavaObjClassName (_ :: JavaObj a) = symbolVal (Proxy :: Proxy a)

  mbd = JavaObj :: JavaObj "java.math.BigDecimal"

  main = do
    putStrLn (getJavaObjClassName mbd)

解释。

  1. 字符串字面量在类型上下文中被提升为GHC.Types.Symbol，所以我们需要将其作为我们的数据种类。
  2. KnownSymbol a => 刚好不允许在运行时抹去a。它携带一个字典，可以用来恢复字符串（通过Proxy）。

（这可能不是最惯用的方法，我不是疯狂且精通 Haskell 扩展的专家）。

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，
原文链接