Haskell中的路径依赖类型

我试图在 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扩展,以便在表类型本身上添加幻像类型,并将此额外类型传递给列.我不喜欢它,因为这种类型的构造会非常复杂(表是通过复杂的DAG操作生成的),并且在这种情况下编译速度很慢.
>使用类似于ST monad的forall构造来包装操作,但在我的情况下,我想要额外的标记类型实际上是逃避构造.

我很高兴有一个非常有限的有效范围,用于构建相同的列(即从表和(id表)的列不能混合),我主要关心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实现的那样简单,但类型错误消息是可以理解的,这对我来说至关重要.

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

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