On Thu, Sep 14, 2006 at 07:51:59PM +0200, Bertram Felgenhauer wrote:
It's a result of thinking about lazy evaluation, and especially lazy patterns (and let bindings) for some time. A wiki article that helped me a lot to understand these is
http://www.haskell.org/hawiki/TyingTheKnot
I'd like to point out the trustList function there which uses the idea of encoding the structure of a term and its actual values in different arguments, i.e. a blueprint.
One view of your device is as separating the shape (blueprint) from the contents, e.g. one can split a finite map type data Map k a = Node !Int k a (Map k a) (Map k a) | Leaf into a pair of types data MapShape k = SNode !Int k (MapShape k) (MapShape k) | SLeaf data MapData a = DNode a (MapData a) (MapData a) | DLeaf (We don't even need DLeaf, as it's never examined.) We need functions fill :: a -> MapShape k -> MapData a update :: Ord k => k -> (a -> a) -> MapShape k -> MapData a -> MapData a insert :: Ord k => k -> MapShape k -> (MapShape k, MapData a -> (a, MapData a)) In a dependently typed language we could parameterize MapData with shapes to give more precise types: fill :: a -> forall s :: MapShape k. MapData s a update :: Ord k => k -> (a -> a) -> forall s :: MapShape k. MapData s a -> MapData s a insert :: Ord k => k -> forall s :: MapShape k. (exists s' :: MapShape k, MapData s' a -> (a, MapData s a)) hinting that the function returned by insert reverses the effect of the insertion. It's not possible to code this with GADTs, because existentials are incompatible with irrefutable patterns, at least in GHC. Anyway, splitSeq then becomes splitSeq :: Ord a => [(a,b)] -> [(a,[b])] splitSeq = fst . splitSeq' SLeaf splitSeq' :: Ord a => MapShape a -> [(a,b)] -> ([(a,[b])], MapData [b]) splitSeq' bp [] = ([], fill [] bp) splitSeq' bp ((a,b):xs) | member a bp = let (l, m) = splitSeq' bp xs in (l, update a (b:) bp m) | otherwise = let (bp', extract) = insert a bp (l, m') = splitSeq' bp' xs (bs, m) = extract m' in ((a, b:bs) : l, m) Again, no knot-tying is required. To prove that (even for partial and infinite lists ps) splitSeq ps = [(a, seconds a ps) | a <- nub ps] where seconds :: Eq a => a -> [(a,b)] -> [b] seconds a ps = [b | (a', b) <- ps, a' == a] we need another function get :: Ord k => k -> MapShape k -> MapData a -> a and the properties member k s => get k s (fill v s) = v member k s => get k s (update k f s m) = f (get k s m) member k s /\ member x s /\ x /= k => get x s (update k f s m) = get x s m not (member k s) /\ insert k s = (s', extract) => member x s' = member x s || x == k not (member k s) /\ insert k s = (s', extract) => fst (extract m) = get k s' m not (member k s) /\ insert k s = (s', extract) /\ member x s => get x s (snd (extract m)) = get x s' m Then we can establish, by induction on the input list, (1) fst (splitSeq' s ps) = [(a, seconds a ps) | a <- nub ps, not (member a s)] (2) member x s => get x s (snd (splitSeq' s ps)) = seconds x ps This is enough to sustain the induction and obtain the desired property, but it's a bit inelegant not to have an exact characterization of the second component. It seems essential to observe the map data only though get.