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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe