CODEWITHSUNDEEP
haskelldata-kinds
Martin Kolinek
Martin Kolinek

Reputation: 2010

How do I make values depend on other values without DataKinds?

I have a universe type, and a worker type. Workers can change the universe. What I would like to achieve is ensure that the universe can only be modified by workers from that universe (not one in the future, or in the past).

The best I could achieve is this:

{-# 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

If I change w2 = head $ _allWorkers u2 to w2 = head $ _allWorkers u I get a compilation error which is what I want.

What I don't like that much is that now I have a version attached to each universe, and I have to increment it manually. Can this be done in another way which would not require the explicit versioning? Something like making the doSomething function return a Universe otherType where the type checker would know otherType is different from t.

Thanks for your time.

Upvotes: 4

Views: 109

Answers (1)

dfeuer
dfeuer

Reputation: 48580

One way is to use existential types:

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

Upvotes: 5

Related Questions