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