haskell - Haskell 中的路径依赖类型

Question

我正在尝试为 Haskell 中的某些数据库系统设计一个 API，并且我想以某种方式对该数据库的列进行建模，以使不同表的列之间的交互不会混淆。

更准确地说，假设您有一个类型来表示数据库中的表，并与某种类型相关联:

type Table a = ...

并且您可以提取表的列以及列的类型:

type Column col = ...

最后，还有各种提取器。例如，如果您的表包含 Frog 的描述，那么您可以使用一个函数提取包含 Frog 重量的列:

extractCol :: Table Frog -> Column Weight

这是问题:我想区分列的来源，以便用户无法在表之间进行操作。例如:

bullfrogTable = undefined :: Table Frog
toadTable = undefined :: Table Frog
bullfrogWeights = extractCol bullfrogTable
toadWeights = extractCol toadTable
-- Or some other columns from the toad table
toadWeights' = extractCol toadTable
-- This should compile
addWeights toadWeights' toadWeights
-- This should trigger a type error
addWeights bullfrogWeights toadWeights

我知道如何在 Scala 中实现这一点(使用路径相关类型，请参阅 [1])，并且我一直在考虑 Haskell 中的 3 个选项:

不使用类型，只在运行时进行检查(当前解决方案)

TypeInType 扩展在 Table 类型本身上添加一个幻像类型，并将这个额外的类型传递给列。我不喜欢它，因为这种类型的构造会非常复杂(表是通过复杂的 DAG 操作生成的)并且在这种情况下编译可能会很慢。

使用 forall 包装操作构造类似于 ST monad，但在我的情况下，我希望额外的标记类型实际上逃避构造。

我很高兴为相同列的构建(即来自 table 和 (id table) 的列不可混合)的构造提供非常有限的有效范围，并且我主要关心 API 的 DSL 感觉而不是安全性。

[1] What is meant by Scala's path-dependent types?

我目前的解决方案

这是我最终使用 RankNTypes 所做的。

我仍然希望让用户能够使用他们认为合适的列，而无需进行一些强类型检查，并且如果他们想要一些更强大的类型保证，则可以选择加入:这是为不了解 Haskell 方面强大功能的数据科学家提供的 DSL

表格仍按其内容标记:

type Table a = ...

和列现在标记了一些额外的引用类型，在它们包含的数据类型之上:

type Column ref col = ...

从表到列的投影要么加标签，要么不加标签。实际上，这隐藏在类似镜头的 DSL 后面。

extractCol :: Table Frog -> Column Frog Weight

data TaggedTable ref a = TaggedTable { _ttTable :: Table a }

extractColTagged :: Table ref Frog -> Column ref Weight

withTag :: Table a -> (forall ref. TaggedTable ref a -> b) -> b
withTag tb f = f (TaggedTable tb)

现在我可以编写如下代码:

let doubleToadWeights = withTag toadTable $ \ttoadTable ->
  let toadWeights = extractColTagged ttoadTable in
    addWeights toadWeights toadWeights

这不会按需要编译:

let doubleToadWeights =
  toadTable `withTag` \ttoads ->
     bullfrogTable `withTag` \tbullfrogs ->
       let toadWeights = extractColTagged ttoads
           bullfrogWeights = extractColTagged tbullfrogs
       in addWeights toadWeights bullfrogWeights -- Type error

从 DSL 的角度来看，我认为它不像使用 Scala 可以实现的那样简单，但是类型错误消息是可以理解的，这对我来说至关重要。

Answer 1

Haskell(据我所知)没有路径依赖类型，但您可以通过使用 rank 2 类型来获得一些方法。例如 ST monad 有一个虚拟类型参数 s用于防止 runST 调用之间的泄漏:

runST :: (forall s . ST s a) -> a

在 ST Action 中，您可以有一个 STRef:

newSTRef :: a -> ST s (STRef s a) 

但是你得到的 STRef 带有 s类型参数，因此不允许从 runST 中转义.