[Haskell-cafe] Re: irrefutable patterns for existential types / GADTs

[apfelmus at quantentunnel.de]

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