Haskell 中的路径依赖类型答案

【问题标题】：Path dependent types in HaskellHaskell 中的路径依赖类型
【发布时间】：2016-10-29 11:01:17
【问题描述】：

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

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

type Table a = ...

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

type Column col = ...

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

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 操作生成的）并且在这种情况下编译可能会很慢。
使用类似于 ST monad 的 forall 构造来包装操作，但在我的情况下，我希望额外的标记类型能够真正逃避构造。

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

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

我目前的解决方案

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

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

表格仍按其内容标记：

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 可以实现的那样简单，但类型错误消息是可以理解的，这对我来说至关重要。

【问题讨论】：

您在列出的选项中似乎有相当不错的选择。唯一想到的是reflection，您可以通过一些聪明才智为您工作。
是的，我正在查看reflection 包。我的问题是 reify 的签名本质上是对正在创建的类型关闭的，即它不会转义。我对 Haskell 类型系统不够熟悉，无法理解是否可以从值中创建类型（这在 Haskell 中听起来像是异端邪说，并且只允许通过 Scala 中的特殊编译器构造）。
在 Haskell 中没有像 Scala 的路径依赖类型那样可用的东西。 “非fast”反射变体包含一种机制，您可以通过该机制对值进行类型表示，但它很混乱，而且您的错误消息会很可怕。创建具有“内涵标识”的类型（即不等于任何其他类型）的唯一方法是通过reify 或runST 之类的范围量词。我会开始寻找混合方法，例如使用您的选项#2，但创建一个简化的幻像类型，它不会捕获所有内容，并结合选择性手动标记或其他东西。
当然，如果您使用模板 haskell，您的选择范围会扩大。例如。您可以为每个表声明生成一个新的顶级类型，然后使用它来标记列。实际上，我认为您可以通过这种方式获得路径相关类型的最小近似值。
add a phantom type on the Table type itself, and pass this extra type to the columns 为什么表格需要有幻像类型？如果用原始表的幻像类型标记的列可能就足够了。

标签： haskell

【解决方案1】：

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

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

在一个 ST 动作中你可以有一个 STRef：

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

但是你得到的 STRef 带有s 类型参数，所以不允许它从runST 中转义。

【讨论】：