[Haskell-cafe] Re: irrefutable patterns for existential types /
GADTs
apfelmus at quantentunnel.de
apfelmus at quantentunnel.de
Sat Sep 30 07:43:04 EDT 2006
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
More information about the Haskell-Cafe
mailing list