不允许赋值

Question

我正在尝试使用类型级别的权限系统，并且我正在尝试禁止分配并非来自同一“来源”的值，即：

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

我已经尝试过 N 级（或暗示性？）类型：

type Value = forall a. Value a ...

但上述两种情况是一致的。如果我约束a：

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

两种情况都没有。有没有办法实现这样的目标？在 Haskell 中可以吗？

（注意：Value 构造函数不会公开，即无法创建独立的Value。）

Answer 1

正如 user2407038 提到的，您可以使用幻像类型来做您想做的事情。

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

但是，有一个解决方法：

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

但是，如果您隐藏 Value 构造函数（通过不导出它），您可以阻止用户编写 getBValue。但这意味着绝对没有办法从Value 中提取实际值。您仍然可以为 Functor、Applicative 和 Monad 实例化 Value，以便您可以直接使用这些包装值。但是您必须将Value 更改为更通用的形式。这是一个例子：

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