How can I use a fixed-minimum-length list in a total and elegant way?

Question

I'm currently dealing with a function that goes like this:

foo = (\(a:b:c:d:e:f:_) -> foobar a b c d e f) . (++ repeat def)

In other words, given a list, it uses the first six elements for something, and if the list is less than six elements long, it uses def as a stand-in for the missing ones. This is total, but the pieces of it aren't (just like map fromJust . filter isJust), so I don't like it. I tried to rewrite this so that it doesn't need to use any partiality, and got this:

foo [] = foobar def def def def def def
foo [a] = foobar a def def def def def
foo [a,b] = foobar a b def def def def
foo [a,b,c] = foobar a b c def def def
foo [a,b,c,d] = foobar a b c d def def
foo [a,b,c,d,e] = foobar a b c d e def
foo (a:b:c:d:e:f:_) = foobar a b c d e f

I technically did what I want, but now this is a gigantic mess. How can I do this in a more elegant and less repetitive way?

Answer 1

Just for fun (and not recommended, this is for funsies), here's another way:

import Data.Default

data Cons f a = a :- f a
infixr 5 :-

data Nil a = Nil -- or use Proxy

class TakeDef f where takeDef :: Default a => [a] -> f a
instance TakeDef Nil where takeDef _ = Nil
instance TakeDef f => TakeDef (Cons f) where
    takeDef (x:xs) = x :- takeDef xs
    takeDef xs = def :- takeDef xs

foo xs = case takeDef xs of
    a:-b:-c:-d:-e:-f:-Nil -> foobar a b c d e f

The type that you use in the pattern match amounts to passing a type-level natural to takeDef saying how many elements to look at.

Answer 2

This is at least shorter:

foo (a:b:c:d:e:f:_) = foobar a b c d e f
foo xs = foo (xs ++ repeat def)

You can easily see that the patterns are exhaustive, but now you have to think a bit to see that it always terminates. So I don't know if you can consider it an improvement.

Otherwise we can do it with the state monad, although it's a bit heavyweight:

foo = evalState (foobar <$> pop <*> pop <*> pop <*> pop <*> pop <*> pop)
  where
    pop = do xs <- get
             case xs of [] -> pure def
                        y:ys -> put ys >> pure y

I could also imagine using an infinite stream type like

data S a = S a (S a)

because then you could construct foo out of repeat :: a -> S a, prepend :: [a] -> S a -> S a, and take6 :: S a -> (a,a,a,a,a,a), all of which could be total. Probably not worth it if you don't already have such a type handy.