静态执行这两个对象是从相同的（Int）“种子”创建的。 [英] Statically enforcing that two objects were created from the same (Int) "seed"

问题描述

在我工作的库中，我有一个类似于以下的API：

  data Collection a = Collection Seed {-etc ...-} 
 type Seed = Int 
 
 newCollection :: Seed  - > IO（Collection a）
 newCollection = undefined 
 
 insert :: a  - >集合a  - > IO（） -  ...和其他可变集合函数
 insert = undefined 
 
 mergeCollections :: Collection a  - >集合a  - > IO（Collection a）
 mergeCollections（Collection s0 {-etc ...-}）（Collection s1 {-etc ...-}）
 | s0 / = s1 =错误这是无效的，我们如何才能使其静态无法访问？ 
 |否则= undefined 
  

我希望能够强制用户不能调用<$ c $使用不同的种子值创建的集合上的c> mergeCollections 。

我想用类型级自然标记 Collection >我认为这意味着种子在编译时必须静态知道，但我的用户可能从环境变量或用户输入中获得它，所以我认为这不会起作用。

我也希望我可以做类似的事情：

  newtype Seed u = Seed Int 
 newSeed :: Int  - > Seed u 
 newCollection :: Seed u  - > IO（Collection u a）
 mergeCollections :: Collection u a  - >集合你 -   - > IO（Collection ua）
  

在某些情况下， Seed 以某种方式标记了一个唯一的类型，这样类型系统可以跟踪 merge 的两个参数是从同一个调用<$ c返回的种子中创建的$ C> newSeed 。在这个（手动波动）方案中清楚 a 和 b 在这里会以某种方式不统一： let a = newSeed 1; b = newSeed 1; 。

是这样的吗？

以下是我可以想象用户创建 Seed s和 Collection 秒。用户希望像其他任何 IO 可变集合一样自由使用其他操作（插入，合并等）：

1. 我们只需要一个种子来所有 集合程序，但用户必须能够以某种方式指定种子在运行时应如何根据环境来确定。




2. 一个或多个静态键从环境变量（或命令行参数）：
   
   

     main = do 
    s1 < -  getEnvSEED1
    s2 < -  getEnvSEED2
     -  ...很多集合可以从这些种子动态创建
     - 稍后动态合并
     




解决方案

可能不是一种方便的方式。为了处理仅在运行时已知的种子，可以使用存在类型;但是然后你不能静态检查这两个存在包装的集合是否匹配。简单得多的解决方案就是这样：



  merge :: Collection a  - >集合a  - > IO（Maybe（Collection a））
  

另一方面，如果强制执行所有操作从某种意义上说，你可以做一些类似于 ST monad的事情：将所有的操作组合在一起，然后提供一个运行的操作，所有这些操作只有在操作不会通过要求它们对幻象变量完全多态来泄漏集合时才有效，因此返回类型不会提及幻像变量。 （Tikhon Jelvis也在他的评论中暗示了这一点）。下面是它的外观：



  { - ＃LANGUAGE Rank2Types＃ - } 
 { - ＃LANGUAGE GeneralizedNewtypeDivingiving＃ - } 
模块集合（Collection，COp，newCollection，merge，inspect，runCOp）其中
 
导入Control.Monad.Reader 
 
 type Seed = Int 
 data Collection sa = Collection Seed 
 newtype COp sa = COp（Seed  - > a）派生（Functor，Applicative，Monad，MonadReader Seed）
 
 newCollection :: COp s（Collection sa）
 newCollection = Collection< $>询问
 
 merge :: Collection s a  - >集合s  -   - > COp s（Collection s a）
合并l r = return（不管l r）其中
 whatever = const 
 
  - 只是一个例子;用
替换你想要的任何函数 - 使用Collection 
 inspect :: Collection s a  - > COp s Int 
检查（收集种子）=返回种子
 
 runCOp ::（所有s。COp s a） - >种子 - > a 
 runCOp（COp f）= f 
  

特别注意 COp 和集合构造函数不会导出。因此，我们不必担心 Collection 会转义它的 COp ; runCOp newCollection 不是很好的类型（以及任何试图将集合泄漏到外部世界的操作都具有相同的属性）。因此，不可能将用一个种子构造的集合传递给在另一个种子的上下文中操作的 merge 。

In a library I'm working on, I have an API similar to the following:

data Collection a = Collection Seed {-etc...-}
type Seed = Int

newCollection :: Seed -> IO (Collection a)
newCollection = undefined

insert :: a -> Collection a -> IO () -- ...and other mutable set-like functions
insert = undefined

mergeCollections :: Collection a -> Collection a -> IO (Collection a)
mergeCollections (Collection s0 {-etc...-}) (Collection s1 {-etc...-}) 
  | s0 /= s1  = error "This is invalid; how can we make it statically unreachable?"
  | otherwise = undefined

I'd like to be able to enforce that the user cannot call mergeCollections on Collections created with different Seed values.

I thought of trying to tag Collection with a type-level natural: I think this would mean that the Seed would have to be statically known at compile time, but my users might be getting it from an environment variable or user input, so I don't think that would work.

I also hoped I might be able to do something like:

newtype Seed u = Seed Int
newSeed :: Int -> Seed u
newCollection :: Seed u -> IO (Collection u a)
mergeCollections :: Collection u a -> Collection u a -> IO (Collection u a)

Where somehow a Seed is tagged with a unique type in some way, such that the type system could track that both arguments to merge were created from the seed returned by the same invocation of newSeed. To be clear in this (hand-wavy) scheme a and b here would somehow not unify: let a = newSeed 1; b = newSeed 1;.

Is something like this possible?

Examples

Here are some examples of ways I can imagine users creating Seeds and Collections. Users would like to use the other operations (inserting, merging, etc) as freely as they could with any other IO mutable collection:

1. We only need one seed for all Collections (dynamically) created during the program, but the user must be able to specify in some way how the seed should be determined from the environment at runtime.

2. One or more static keys gathered from environment vars (or command line args):

   main = do
      s1 <- getEnv "SEED1"
      s2 <- getEnv "SEED2"
      -- ... many Collections may be created dynamically from these seeds
      -- and dynamically merged later
   

解决方案

Probably not in a convenient way. For handling seeds that are known only at runtime, you can use existential types; but then you cannot statically check that two of these existentially wrapped collections match up. The much simpler solution is simply this:

merge :: Collection a -> Collection a -> IO (Maybe (Collection a))

On the other hand, if it is okay to force all operations to be done "together", in a sense, then you can do something like what the ST monad does: group all the operations together, then supply an operation for "running" all the operations that only works if the operations don't leak collections by demanding they be perfectly polymorphic over a phantom variable, hence that the return type doesn't mention the phantom variable. (Tikhon Jelvis also suggests this in his comments.) Here's how that might look:

{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Collection (Collection, COp, newCollection, merge, inspect, runCOp) where

import Control.Monad.Reader

type Seed = Int
data Collection s a = Collection Seed
newtype COp s a = COp (Seed -> a) deriving (Functor, Applicative, Monad, MonadReader Seed)

newCollection :: COp s (Collection s a)
newCollection = Collection <$> ask

merge :: Collection s a -> Collection s a -> COp s (Collection s a)
merge l r = return (whatever l r) where
  whatever = const

-- just an example; substitute whatever functions you want to have for
-- consuming Collections
inspect :: Collection s a -> COp s Int
inspect (Collection seed) = return seed

runCOp :: (forall s. COp s a) -> Seed -> a
runCOp (COp f) = f

Note in particular that the COp and Collection constructors are not exported. Consequently we need never fear that a Collection will escape its COp; runCOp newCollection is not well-typed (and any other operation that tries to "leak" the collection to the outside world will have the same property). Therefore it will not be possible to pass a Collection constructed with one seed to a merge operating in the context of another seed.

这篇关于静态执行这两个对象是从相同的（Int）“种子”创建的。的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！