在没有 DataKinds 的情况下，如何使值依赖于其他值？答案

【问题标题】：How do I make values depend on other values without DataKinds?在没有 DataKinds 的情况下，如何使值依赖于其他值？
【发布时间】：2015-08-20 14:58:34
【问题描述】：

我有一个 Universe 类型和一个 worker 类型。工人可以改变宇宙。我想要实现的是确保宇宙只能由来自该宇宙的工人修改（不是未来或过去）。

我能做到的最好的是：

{-# LANGUAGE DataKinds       #-}
{-# LANGUAGE KindSignatures  #-}

module Module(initialUniverse, doSomething, doStep) where

data Nat = Z | S Nat

data Universe (t :: Nat) = Universe {
  _allWorkers :: [Worker t]
}

data Worker (t :: Nat) = Worker

initialUniverse :: Universe Z
initialUniverse = Universe [Worker]

doSomething :: Worker t -> Universe t -> Universe (S t)
doSomething = undefined

doStep :: Universe t -> Universe (S (S t))
doStep u = let w = head $ _allWorkers u
               u2 = doSomething w u
               w2 = head $ _allWorkers u2
               u3 = doSomething w2 u2
           in u3

如果我将 w2 = head $ _allWorkers u2 更改为 w2 = head $ _allWorkers u 我会收到我想要的编译错误。

我不太喜欢的是现在我有一个附加到每个宇宙的版本，我必须手动增加它。这可以以不需要显式版本控制的另一种方式完成吗？比如让doSomething 函数返回一个Universe otherType，其中类型检查器会知道otherType 与t 不同。

感谢您的宝贵时间。

【问题讨论】：

没有DataKind？你不是已经在使用Universe 和Worker 类型的扩展了吗？
我很难从你的代码中看出你的最终目标是什么。也就是说，我不知道哪些部分对您很重要，哪些部分是您不喜欢的解决方案。
@dfeuer，如果工人和宇宙不相关，我的最终目标是当我尝试用工人和宇宙调用 doSomething 时出现编译时错误。我通过向 Universe 和工作人员添加一个版本来实现这一点，每次发生事情时都会增加一个版本。函数 doSomething 的类型检查 Universe 和 worker 是否具有相同的版本。这个解决方案还可以，我只是想知道有没有更简单的，因为我感觉 Haskell 类型系统可以在没有版本的情况下检查它。
好的，我想我明白你的意思了。我会说something similar to the ST monad 会是惯用的。
这里是描述它的论文的链接：researchgate.net/profile/Simon_Peyton_Jones/publication/…

标签： haskell data-kinds

【解决方案1】：

一种方法是使用存在类型：

data Un = forall s. Un (Universe s)

doSomething :: Worker s -> Universe s -> Un

initialUniverse :: Un


doStep :: Un -> Un
doStep (Un u) = let w = head $ _allWorkers u
               u2 = doSomething w u
               w2 = head $ _allWorkers u2
               u3 = doSomething w2 u2
            in Un u3

【讨论】：