I’ve recently been thinking about isomorphic presentations of datatypes, and how best to approach leveraging the different representations simultaneously. I wrote a small library llun intended as a drop-in replacement for Data.List.NonEmpty, and was able to use pattern synonyms to better understand the problem I was trying to attack.
Non-empty by construction
Non-empty lists are one of the most fundamental examples of the applications of type safety. A regular list has two modes of construction:
data List x where
Nil :: List x
(:) :: x -> List x -> List x
-- [1, 2, 3] is semantically equal to (1 : (2 : (3 : Nil)))
However, a NonEmpty list only has one constructor, so does not permit the empty case:
data NonEmpty x where
(:|) :: x -> List x -> NonEmpty x
This means that whenever we have a value of type NonEmpty, we have a projection function head :: (\(x :| _) -> x) :: NonEmpty x -> x. The same cannot be said for List x since we cannot know in general how to deconstruct Nil; instead we resort to listToMaybe :: List x -> Maybe x to handle this empty case.
The definition of NonEmpty above references List, but it doesn’t have to. There is a mathematically isomorphic definition with two constructors:
data NonEmpty' x where
End :: x -> NonEmpty' x
And :: x -> NonEmpty' x -> NonEmpty' x
-- (End x) ~ (x : [])
-- (And x xs) ~ (x : xs)
It’s like if we just stuck an x onto the constructors for List! And in fact there’s another isomorphic definition
data NonEmpty'' x where
N :: x -> Maybe (NonEmpty'' x) -> NonEmpty'' x
-- (x `N` Nothing) ~ (End x)
-- (x `N` Just xs) ~ (And x xs)
Just because they’re mathematically isomorphic doesn’t mean they’re semantically the same; different perspectives can yield useful insights about a problem. To avoid a bunch of different data types that can’t easily be converted, we’re going to use the following pattern synonyms in the rest of this post:
infixr 5 :|, :&, :&?
data NonEmpty x = x :| [x]
nonEmpty :: [x] -> Maybe (NonEmpty x)
nonEmpty = \case
[] -> Nothing
x : xz -> Just (x :| xz)
pattern End :: x -> NonEmpty x
pattern End x = x :| []
pattern (:&) :: x -> NonEmpty x -> NonEmpty x
pattern x :& xs <- (x :| ~(nonEmpty -> Just xs))
where
x :& ~(y :| xz) = x :| (y : xz)
{-# COMPLETE End, (:&) #-}
pattern (:&?) :: x -> Maybe (NonEmpty x) -> NonEmpty x
pattern x :&? mxs <- (x :| ~(nonEmpty -> mxs))
where
x :&? mxs = maybe (End x) (x :&) mxs
{-# COMPLETE (:&?) #-}
The {-# COMPLETE #-} pragmas in the above snippet assert to GHC that the listed patterns cover all the cases, and that it doesn’t need to emit warnings for non-exhaustive pattern matches if all of them show up. This is essentially the same as providing a different “constructor set” for the data type, without the added conversion cost. They can even be used in expressions because they are bidirectional: implicitly in End using = but made explicit in both (:&) and (:&?) with <- and where. For more information on pattern synonyms, see the GHC user’s guide.
We can also write some helper functions in the style of these patterns to make our life easier while keeping our eDSL consistent:
(&:) :: NonEmpty x -> x -> NonEmpty x
(x :| xs) &: y = x :| (xs <> [y])
(<&) :: NonEmpty x -> [x] -> NonEmpty x
(x :| xs) <& ys = x :| (xs <> ys)
(&>) :: [x] -> NonEmpty x -> NonEmpty x
xs &> ys = case xs of
[] -> ys
(x : xs) -> x : (xs &> ys)
To recap, we have three sets of complete pattern matches on NonEmpty x:
match1 = \case
(x :| xz) -> _ -- x :: x, xz :: [x]
match2 = \case
End x -> _ -- x :: x
(x :& xs) -> _ -- x :: x, xs :: NonEmpty x
match3 = \case
(x :&? mxs) -> _ -- x :: x, mxs :: Maybe (NonEmpty x)
List permutations
Let’s take a trip back to empty-list-land for this section, and savour the syntactic sugar. The permutations of a list are all the possible orderings of that list.
> sort (permutations [1..4])
[ [1,2,3,4]
, [1,2,4,3]
, [1,3,2,4]
, [1,3,4,2]
, [1,4,2,3]
, [1,4,3,2]
, [2,1,3,4]
, [2,1,4,3]
, [2,3,1,4]
, [2,3,4,1]
, [2,4,1,3]
, [2,4,3,1]
, [3,1,2,4]
, [3,1,4,2]
, [3,2,1,4]
, [3,2,4,1]
, [3,4,1,2]
, [3,4,2,1]
, [4,1,2,3]
, [4,1,3,2]
, [4,2,1,3]
, [4,2,3,1]
, [4,3,1,2]
, [4,3,2,1]
]
The current implementation in Data.List is the maximally lazy one. That means that it produces every permutation it can before moving on to the next element in the source list.
permutations [1 .. n] ==
map (take n) $ take (factorial n) (permutations [1 ..])
The StackOverflow link above explains some of the logic behind the existing implementation, shown below for y’all who didn’t click the link. We could hijack this implementation with fromList . map fromList since we would be certain that the empty case never happens, but where’s the fun in that?
permutations :: [a] -> [[a]]
permutations xs0 = xs0 : perms xs0 []
where
perms :: forall a. [a] -> [a] -> [[a]]
perms [] _ = []
perms (t:ts) is = foldr interleave (perms ts (t:is)) (permutations is)
where
interleave :: [a] -> [[a]] -> [[a]]
interleave xs r = let (_,zs) = interleave' id xs r in zs
interleave' :: ([a] -> b) -> [a] -> [b] -> ([a], [b])
interleave' _ [] r = (ts, r)
interleave' f (y:ys) r = let (us,zs) = interleave' (f . (y:)) ys r
in (y:us, f (t:y:us) : zs)
Yeah. That’s no fun. Let’s figure out how to write the nonempty version from scratch.
We’re going to need some way of keeping track of how many elements we’ve seen already, and how many are left. We need to be able to see ahead and behind at the same time. So let’s work diagonally. (1)
diagonally :: NonEmpty x -> (NonEmpty x -> NonEmpty x -> y) -> Maybe (NonEmpty y)
diagonally xs withFutureAndPast =
let futures' = tails xs
pasts' = inits xs
-- Note that these are different from the empty versions:
-- they do not include the empty tail or init. To make sure
-- that we're taking these into account, we'll just
-- call everything `Maybe` and tack `Nothing`s on either end.
futures = (Just <$> futures') &: Nothing
pasts = Nothing :& (Just <$> pasts')
in catMaybes $ -- Newbie level up: why not `sequence`?
zipWith
(liftM2 @Maybe withFutureAndPast)
futures
pasts
Okay, but what does this look like?
> let diagonals = flip diagonally (,)
> toList . fmap (toList *** toList) $ diagonals (1 :| [2, 3, 4])
[([2,3,4], [1]), ([3,4], [1,2]), ([4], [1,2,3])]
Each step diagonally gives us access to both sides of the list. Why does this help us? Well, because now at each step we can ensure that the past has been fully permuted before we look at the future. Now all we have to do is figure out how to do the recursive step.
permutations :: NonEmpty x -> NonEmpty (NonEmpty x)
permutations xs =
let subperms = diagonally xs \(next :| futures) pasts -> do
pastPerms <- permutations pasts
-- Now that we have the past permutations, we need to stick `next`
-- in there, in every place it can go, to find out all the permutations
-- that we'll have made at our next diagonal.
in undefined
Crap. Okay. Let’s figure out how to insert a value in front of every existing element of a list.
insertions :: x -> NonEmpty x -> NonEmpty (NonEmpty x)
insertions x l@(y :&? ys) =
(x :& l) -- stick it on the front
:&? -- if there's more,
(fmap (y :&) . insertions x <$> ys) -- recurse one element inwards
> fmap toList $ insertions 'A' ('x' :| "xxxx")
"Axxxxx" :| ["xAxxxx","xxAxxx","xxxAxx","xxxxAx"]
Now we can try again:
permutations :: NonEmpty x -> NonEmpty (NonEmpty x)
permutations xs =
-- subperms :: Maybe (NonEmpty (NonEmpty (NonEmpty x)))
let subperms = diagonally xs \(next :| futures) pasts -> do
-- pastPerms :: NonEmpty (NonEmpty x)
pastPerms <- permutations pasts
-- presentPerms :: NonEmpty (NonEmpty (NonEmpty x))
let presentPerms =
insertions next pastPerms
-- tack on the unpermuted future bits to each present perm
<&> (<& futures)
pure presentPerms
in xs :&? fmap @Maybe (join @NonEmpty) subperms
We finally join to squash all of the presentPerms into a single NonEmpty, because those are all of the permutations for a single step. We just had to insert next into every spot to generate them all. And now, in one line:
permutations :: NonEmpty x -> NonEmpty (NonEmpty x)
permutations xs =
(xs :&?) . fmap join $ diagonally xs \(t :| ts) -> fmap (<& ts) . insertions t <=< permutations
But is this maximally lazy? Let’s test it.
take :: Int -> NonEmpty x -> Maybe (NonEmpty x)
take n (x :| xs)
| n <= 0 = Nothing
| otherwise = Just (x :| Data.List.take (n - 1) xs)
Permitting ourselves to convert to plain lists for demonstration purposes, we do see that this is the case:
> let three = 1 :| [2, 3]
> let foops = three &: undefined
>
> (toList . fmap toList) (permutations three)
[[1,2,3],[2,1,3],[3,1,2],[1,3,2],[3,2,1],[2,3,1]]
> fmap (maybe [] toList . take 3) . maybe [] toList $ take 6 (permutations foops)
[[1,2,3],[2,1,3],[3,1,2],[1,3,2],[3,2,1],[2,3,1]]
And the general property can also be witnessed:
permsLazy :: Int -> Bool
permsLazy n =
let list = 0 :| [1 .. abs n - 1]
nn = List.product [1 .. n]
in (toList . fmap toList) (permutations list)
== ( fmap (maybe [] toList . take n) . maybe [] toList $
take nn (permutations (0 :| [1 ..]))
)
> map permsLazy [1..]
[True,True,True,True,True,^CInterrupted.
(1) This is actually where I’ve swept some stuff under the rug: this whole thing only works because Data.List.inits is implemented tail-recursively with snoc-lists. Otherwise we’d be forcing the list and we’d hit _|_ on infinite inputs. I just used the fromList . map fromList trick for this nonempty inits. I guess I’m not a true magician!