haskell - 静态强制两个对象是从同一个 (Int) "seed"创建的

Question

在我正在研究的库中，我有一个类似于以下内容的 API:

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

我希望能够强制用户不能调用 mergeCollections在 Collection s 创建了不同的 Seed值(value)观。

我想尝试标记 Collection具有类型级别的自然:我认为这意味着 Seed必须在编译时静态知道，但我的用户可能是从环境变量或用户输入中获取它的，所以我认为这行不通。

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

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)

哪里有一个 Seed以某种方式被标记为唯一类型，以便类型系统可以跟踪 merge 的两个参数由 newSeed 的相同调用返回的种子创建.在这个(手波)方案中要清楚 a和 b这里会以某种方式不统一: let a = newSeed 1; b = newSeed 1; .

这样的事情可能吗？

例子

以下是我可以想象的用户创建 Seed 的一些示例。 s 和 Collection s。用户希望尽可能自由地使用其他操作(插入、合并等) IO可变集合:

我们只需要一粒种子Collection s(动态)在程序期间创建，但用户必须能够以某种方式指定如何在运行时从环境中确定种子。

从环境变量(或命令行参数)收集的一个或多个静态键:

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

Answer 1

可能不是以一种方便的方式。要处理仅在运行时已知的种子，您可以使用存在类型；但是你不能静态地检查这些存在包装的集合中的两个是否匹配。更简单的解决方案就是这样:

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

另一方面，如果可以强制所有操作“一起”完成，从某种意义上说，那么您可以执行类似于 ST 的操作。 monad 确实:将所有操作组合在一起，然后提供一个操作来“运行”所有操作提到幻象变量。 (Tikhon Jelvis 在他的评论中也提出了这一点。)这可能是这样的:

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

特别注意 COp和 Collection构造函数不会被导出。因此，我们不必担心 Collection将逃脱其 COp ; runCOp newCollection类型不正确(并且任何其他试图将集合“泄漏”到外部世界的操作都将具有相同的属性)。因此无法通过 Collection用一粒种子构建到 merge在另一个种子的上下文中运行。