可变引用的非单子模型探索

### 可变引用的非单子模型探索 #### 1. 快速实现的正确性 InitValue的定义与快速实现中的相同，这是合理的。newRef函数会返回一个新的引用，并将新引用和给定的被引用值添加到堆中。新堆初始为空，用于创建新键的辅助值初始为1，其定义如下： ```haskell newHeap′ hs :: (∀t.∗Heap′ hs t →a) →a newHeap′ hs f = f (Heap′ hs 1 empty) ``` 关于快速实现的正确性，有如下定理：设P是使用纯实现的程序，P'是使用快速实现的类似程序。如果P'能通过Clean的唯一性类型系统进行类型检查，那么P和P'的可观察行为相同。快速实现中，新引用的创建、引用的读写操作都是常数时间操作。不过，该定理的准确表述和证明还有待进一步研究。 #### 2. 同质堆 之前的模型无法给出完全纯的实现，主要原因是堆不是同质的，即堆可以存储不同类型的值，因为值的类型由键的类型决定，而非堆本身。现在引入同质堆，其中存储值的类型由堆的类型决定。至于这是否会降低模型的抽象能力，还有待进一步研究，但第4节的应用表明，其表达能力并未显著降低。 同质堆的纯实现代码如下： ```haskell data Heaphom v t = Heaphom Integer (Map Integer v) newtype Refhom t = Refhom Integer instance HeapRef (Heaphom v t) (Refhom t) where type Value (Heaphom v t) (Refhom t) = v readRef (Refhom i) h@(Heaphom m) = case lookup i m of Just x → (x, h) writeRef (Refhom i) v (Heaphom s m) = Heaphom s (insert i v m) ``` 这里，被引用值由堆的类型决定，readRef和writeRef的定义与之前模型类似，但这次不需要使用unsafeCoerce。NewRef实例的定义与简单标记模型类似，也无需unsafeCoerce，newHeaphom的定义同样如此。 #### 3. 分离种子 之前的模型支持“堆种子”特性，现在来看只支持“分离种子”和“同质堆”的模型。分离种子意味着无需堆也能创建引用。 快速实现中，种子的定义与堆类似： ```haskell data Seedsep v t = Seedsep ``` 种子实际上不存储任何内容，新引用的实际值将存储在引用中。相关实例定义如下： ```haskell instance NewRef (Seedsep v t) (Refsep t) where type InitValue (Seedsep v t) (Refsep t) = v newRef v Seedsep = unsafePerformIO$ do r ← newIORef (unsafeCoerce v) return (Refsep r, Seedsep) instance Split (Seedsep v t) where split2 Seedsep = (Seedsep, Seedsep) ``` 由于没有堆种子，每次创建堆时都需要同时创建对应的种子： ```haskell newHeapsep :: (∀t.∗Heapsep v t →∗Seedsep v t →a) →a newHeapsep f = f Heapsep Seedsep ``` 纯实现中： ```haskell data Ref′ sep t = Ref′ sep Any Integer newtype Heap′ sep v t = Heap′ sep (Map Integer v) newtype Seed′ sep v t = Seed′ sep Integer instance HeapRef (Heap′ sep v t) (Ref′ sep t) where type Value (Heap′ sep v t) (Ref′ sep t) = v readRef (Ref′ sep d i) h@(Heap′ sep m) = case lookup i m of Nothing → (unsafeCoerce d, h) Just v → (v, h) writeRef (Ref′ sep d i) v (Heap′ sep m) = Heap′ sep (insert i v m) instance NewRef (Seed′ sep v t) (Ref′ sep t) where type InitValue (Seed′ sep v t) (Ref′ sep t) = v newRef v (Seed′ sep s) = (Ref′ sep (unsafeCoerce v) s, Seed′ sep (2 ∗ s)) instance Split (Seed′ sep v t) where split2 (Seed′ sep s) = (Seed′ sep (2 ∗ s), Seed′ sep (2 ∗ s + 1)) newHeap′ sep :: (∀t.∗Heap′ sep v t →∗Seed′ sep v t →a) →a newHeap′ sep f = f (Heap′ sep empty) (Seed′ sep 1) ``` 这里，纯引用需要包含创建时给定的值，由于同质引用类型构造函数未由被引用值类型参数化，导致实现的纯度有所降低。不过，可以通过为Ref′ sep添加被引用值类型作为参数来解决，后续会给出其他解决方案。 #### 4. 可删除引用 可删除引用是指可以从堆中删除的引用。从某种角度看，可删除引用就是被引用值类型为Maybe σ（σ为某种类型）的普通引用。 纯实现代码如下： ```haskell data Seeddel t = Seeddel Integer newtype Heapdel v t = Heapdel (Map Integer v) newtype Refdel t = Refdel Integer instance HeapRef (Heapdel v t) (Refdel t) where type Value (Heapdel v t) (Refdel t) = Maybe v readRef (Refdel i) h@(Heapdel m) = (lookup i m, h) writeRef (Refdel i) Nothing (Heapdel m) = Heapdel (delete i m) writeRef (Refdel i) (Just v) (Heapdel m) = Heapdel (insert i v m) instance NewRef (Seeddel t) (Refdel t) where type InitValue (Seeddel t) (Refdel t) = () newRef () (Seeddel s) = (Refdel s, Seeddel (2 ∗ s)) ``` 可删除引用的主要优点是，其种子无需由被引用类型参数化，因为可以为任何类型的新引用提供默认的Nothing值，这将简化“共享引用”特性的实现。 同时，还定义了一些专门用于可删除引用的函数： ```haskell deleteRef :: (HeapRef h r, Value h r∼Maybe v) ⇒ r → h → h deleteRef r h = writeRef r Nothing h insertRef :: (HeapRef h r, Value h r∼Maybe ```