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

[apfelmus at quantentunnel.de]

> Thanks for asking!
> [...]
> Online algorithms do look like a good place to try to get some leverage
> from this, but we haven't really been in a position to experiment so
> far. I'm sure that will change. 

Well, I asked because laziness with memoization gives a definite edge in
terms of algorithmic time complexity over strictness (proved for online
algorithms in "more haste, less speed") and I wonder how this goes
together with totality and dependent types. A forthcoming ultimate
programming language should retain this edge, shouldn't it? ;-)


> It isn't necessary to perform
> constructor discrimination when it's statically known that exactly one
> constructor is possible, so those patterns can always be made
> irrefutable, with matching replaced by projection.

Thanks for pinpointing the culprit, because translated to GADTs, it
means that

    "whenever we know from the type index that only one constructor is
possible, it can be made irrefutable."

So this is the kind of irrefutable pattern one could safely add. In
particular, this can be weakened to

    "whenever we know the type index, i.e. there is no type refinement
depending on the value, an irrefutable pattern is safe."

But once no type refinement happens, the irrefutable pattern can already
be obtained via let bindings in existing Haskell! Below is a lazy
version of Bertram solution to the "Optimization problem" following
Ross' suggestions with existentials and GADTs:

> {-# OPTIONS_GHC -fglasgow-exts #-}
> 
> 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

(Map s k a) is a tree which makes its structure explicit in the type
index s.

>
> unNode :: Map (s,t) k a -> (k,a,Map s k a, Map t k a)
> unNode (Node k a l r) = (k,a,l,r)

unNode knows the type index and is to be used for a lazy pattern match
  let (k,a,l,r) = unNode ..

> 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
> 
> data Undoer s k a where
>     Undoer :: (Map t k a) -> (Map t k a -> (a,Map s k a)) -> Undoer s k a

Undoer is just (exists t. ...) wrapped into a digestible type.

>     -- 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)
>     (\map -> let (_,a,_,_) = unNode map in (a,Leaf))

Note how the type system proves that the function (\map -> ..) always
has to expect (map) == Node ...
Then, unNode binds k',b',... /lazily/.
Same goes for the rest of insert:

> 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)
>                     (\map -> let
>                             (k',b',m',r') = unNode map
>                             (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)
>                     (\map -> let
>                             (k',b',l',m') = unNode map
>                             (a,r') = f m'
>                         in (a,Node k' b' l' r' :: Map s k a))
> 
>     -- update k fun blueprint map
> update :: Ord k => k -> (a -> a) -> Map s k a -> Map s k a -> Map s k a
> update k f (Node k' _ l' r') map = 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' r)
>     where
>     (_,a,l,r) = unNode map

Again a lazy pattern match on (map). Note that the type system enforces
that blueprint and actual (map) have the same shape s. The type
refinement for GADTs happens in the strict pattern match on the
blueprint and this allows us to lazily match the (map).

> 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:) bp 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 summarize, the problem can be solved without irrefutable patterns for
GADTs: the code above works for infinite lists. Yet, they are handy and
can be introduced safely in the case where the type indices are known in
advance and no type refinement happens.

Regards,
apfelmus