4

ユニバース タイプとワーカー タイプがあります。労働者は宇宙を変えることができます。私が達成したいのは、そのユニバースのワーカーのみがユニバースを変更できるようにすることです (将来または過去のワーカーではありません)。

私が達成できる最高のものはこれです：

{-# 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関数が a を返すようにするようなものは、とは異なります。Universe otherTypeotherTypet

御時間ありがとうございます。

4

1 に答える 1

5

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
于 2015-08-20T20:47:22.047 に答える