Disallow assignment of values

Question

I'm experimenting with a type-level permission system, and I'm trying to disallow assignment of values which do not originate from the same "source", i.e:

data A = A { a :: Value, b :: Value }

modify :: A -> A
modify (A v) = A $ v { a = v.a } -- should work
modify (A v) = A $ v { a = v.b } -- should *NOT* work

I've experimented with rank N (or impredicative?) types:

type Value = forall a. Value a ...

but both cases above unify. If I constrain a:

type Value = forall a. Unique a => Value a ...

both cases don't. Is there a way to achieve something like that? Is it possible in Haskell?

(Note: the Value constructor would not be public, i.e. there's no way to create a standalone Value.)

Answer 1

As user2407038 mentionned, you could use phantom types to do what you want.

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

data ValueType = A | B

data Value :: ValueType -> * where
    Value :: Int → Value t

data V = V { a :: Value A, b :: Value B }

modify ∷ V -> V
modify v = v { a = a v }  -- no error
modify v = v { a = b v }  -- Couldn't match type ‘'B’ with ‘'A’

However, there is a workaround:

modify ∷ V -> V
modify v = v { a = Value $ getBValue (b v) }
    where getBValue (Value x) = x

But you can prevent the user from writing getBValue if you hide the Value constructor (by not exporting it). But that would mean that there is absolutely no way to extract the actual value out of a Value. You could still instantiate Value for the Functor, Applicative and Monad so that you can work with those wrapped values directly. But you would have to change Value to a more general form. Here is an example:

data Value :: ValueType -> * -> * where
    Value :: a -> Value t a

instance Functor (Value t) where
    fmap f (Value x) = Value (f x)

instance Applicative (Value t) where
    pure = Value
    Value f <*> Value x = Value (f x)

instance Monad (Value t) where
    Value x >>= f = f x