Here is a formulation of what exactly I require from irrefutable pattern matches for GADTs. The problem arouse from the "Optimization problem" thread. In short, here is a GADT-using, type safe version of Bertram's solution (without balancing)
-- a binary search tree with witness about its shape data Map s k a where Leaf :: Map () k a Node :: k -> a -> Map s k a -> Map t k a -> Map (s,t) k a
empty :: Map () k a empty = Leaf
member :: Ord k => k -> Map s k a -> Bool member _ Leaf = False member k (Node k' _ l r) = case compare k k' of LT -> member k l EQ -> True GT -> member k r
-- a wrapper for an existential type data Undoer s k a where Undoer :: (Map t k a) -> (Map t k a -> (a,Map s k a)) -> Undoer s k a
-- insert key element blueprint map (blueprint, result, map) insert :: Ord k => k -> a -> Map s k a -> Undoer s k a insert k a Leaf = Undoer (Node k a Leaf Leaf) (\(Node k a Leaf Leaf) -> (a,Leaf)) insert k a (Node k' b (l :: Map l k a) (r :: Map r k a) :: Map s k a) = case compare k k' of LT -> case insert k a l of Undoer (m :: Map t k a) f -> Undoer (Node k' b m r :: Map (t,r) k a) (\(Node k' b' m' r' :: Map (t,r) k a) -> let (a,l') = f m' in (a,Node k' b' l' r' :: Map s k a)) EQ -> error "inserting existing element" GT -> case insert k a r of Undoer (m :: Map t k a) f -> Undoer (Node k' b l m :: Map (l,t) k a) (\(Node k' b' l' m' :: Map (l,t) k a) -> let (a,r') = f m' in (a,Node k' b' l' r' :: Map s k a))
update :: Ord k => k -> (a -> a) -> Map s k a -> Map s k a -- the culprit, to be defined later
splitSeq :: Ord a => [(a,b)] -> [(a,[b])] splitSeq = fst . splitSeq' empty
splitSeq' :: Ord a => Map s a [b] -> [(a,b)] -> ([(a,[b])], Map s a [b]) splitSeq' bp [] = ([], bp) splitSeq' bp ((a,b):xs) = case member a bp of True -> let (l, m) = splitSeq' bp xs in (l, update a (b:) m) _ -> case insert a [] bp of Undoer bp' f -> let (rs,m) = splitSeq' bp' xs (bs,m') = f m in ((a, b:bs) : rs, m')
To make this work in a lazy manner (it becomes an online algorithm then and works for infinite lists), I'd like to have
update :: Ord k => k -> (a -> a) -> Map s k a -> Map s k a update k f ~(Node k' a l r) = case compare k k' of LT -> Node k' a (update k f l) r EQ -> Node k' (f a) l r GT -> Node k' a l (update k f r)
reasoning that the Node constructor should be output before one inspects the incoming ~Node. I thought that "(l, m) = splitSeq' bp xs" witnesses that bp and m have the same Shape s, but this is the point where the not-normalizing argument throws in: the type of splitSeq' claims to be a proof that bp and m have the same s but who knows whether it really terminates? So, I'm opting for a different update which is more along the lines of Bertram's original:
update :: Ord k => k -> (a -> a) -> Map s k a -> Map t k a -> Map s k a update k f (Node k' _ l' r') ~(Node _ a l r) = case compare k k' of LT -> Node k' a (update k f l' l) r EQ -> Node k' (f a) l r GT -> Node k' a l (update k f r)
The blueprint gives immediate witness that splitSeq' preserves shape, so this update should be fine. To summarize, the main problem is to get a lazy/online algorithm (the problem here falls into the "more haste, less speed" category) while staying more type safe. @Conor: how does this issue look like in Epigram? Regards, apfelmus