不允许赋值

Question

我正在试验类型级别的权限系统，我试图禁止分配并非源自同一 "source" 的值，即：

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 构造函数不会是 public，即无法创建独立的 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

不允许赋值

Disallow assignment of values

haskell

purescript

unification

impredicativetypes

rank-n-types