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

Question

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.

Without `DataKind`? Aren't you already using the extension given the type of `Universe` and `Worker`? — gallais, Aug 20 '15 at 16:58
It's pretty hard for me to see, from your code, what your ultimate goal is. That is, I can't tell which parts are important to you and which are pieces of the solution you don't like. — dfeuer, Aug 20 '15 at 17:06
@gallais, yes I'm already using DataKinds extension, I was just asking whether there isn't a better solution. — Martin Kolinek, Aug 20 '15 at 18:26
@dfeuer, my ultimate goal is to get a compile time error when I try to call doSomething with a worker and a universe if the worker and universe are unrelated. I achieve this by adding a version to the Universe and the workers which is incremented everytime something has happened. The type of the function doSomething checks whether the universe and the worker have the same version. This solution is ok, I'm just wondering if there isn't a simpler one as I have a feeling that the Haskell type system can check it without the version. — Martin Kolinek, Aug 20 '15 at 18:36
Ok, I think I see what you mean. I'd say that [something similar to the ST monad](http://stackoverflow.com/questions/12468622/how-does-the-st-monad-work) would be idiomatic. — gallais, Aug 20 '15 at 20:56
And here is a link to the paper describing it: http://www.researchgate.net/profile/Simon_Peyton_Jones/publication/2295326_Lazy_Functional_State_Threads/links/0046351edd5bb96287000000.pdf — gallais, Aug 20 '15 at 21:23

score 5 · Accepted Answer · answered Aug 20 '15 at 20:47

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

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

1 Answers1