不允许转让

我与一个类型级权限的系统试验，我试图以禁止不从相同的“源”来源值的分配，即：不允许转让

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（或impredicative？）类型：

type Value = forall a. Value a ...

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

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

这两种情况都没有。有没有办法实现这样的事情？ Haskell有可能吗？

（注：Value构造不会公开，即有没有方法来创建一个独立的Value。）

来源

2017-06-18 Philip Kamenarsky

不会那么破*参照透明度*？ –

将一个幻像类型参数添加到'Value'并在'A'内用两种不同的类型实例化它;例如使用'TypeLits'：'data A = A（Value 1）（Value 2）'。这实际上只不过是有两个（或'k' for'k：Nat'）不同的，同构的'Value'类型。（另外：你说的第一件事你称之为'existensial'类型，而不是'impredicative'或'rank-N'，它们都是完全不同的东西）。 – user2407038

由于user2407038 mentionned，你可以使用幻象类型做你想做什么。

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

但是你可以防止用户编写getBValue如果隐藏Value构造函数（通过不出口的话）。但这意味着绝对没有办法从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

来源

2017-06-18 15:10:24 baxbaxwalanuksiwe

您可能不想使用非ASCII Unicode符号或将UnicodeSyntax添加到语言扩展中（个人而言，我建议使用前者，因为它可能在编程问题的答案的上下文中更清晰一些）。 –

对不起，UnicodeSyntax默认在我的GHCi中，我编辑我的代码使用ASCII字符，谢谢。 – baxbaxwalanuksiwe

回答

相关问题