Continuing the conversation beyond Pattern Synonyms for Non-Empty Lists.
by Lyle Kopnicky, Senior Software Developer at TripShot
A few months ago, we posted about Pattern Synonyms for Non-Empty Lists. These patterns, NE1 through NE4, make it convenient to construct and pattern-match on fixed-size NonEmpty lists. However, it still bugged us that when creating a list, we had to specify the number of elements. If we needed to add an element, we’d have to update the number. Why count when the computer can do it? Our solution was to create the variadic nel function, which can take an arbitrary number of arguments (at least one), and build a NonEmpty list from them.
For example, you can write nel ‘x’ ‘y’ ‘z’ :: NonEmpty Char and the result will be ‘x’ :| “yz”. Note that <| prepends an element to a NonEmpty and :| builds a NonEmpty from an element and a regular list. If the code is written in a module, the type is usually clear from the context and does not require an annotation.
First Version, Inspired by printf
As an existing example of a variadic function, we looked at Text.Printf.printf. It has the type signature printf :: (PrintfType r) => String -> r. It relies on type inference from the context to get the type of r, which can be of the form a -> b -> c -> String. The type class PrintfType has a recursive instance for a -> r, and a base case for String.
Inspired by this approach, we wrote the following code:
1{-# LANGUAGE MultiParamTypeClasses #-} 2 3{-# LANGUAGE FunctionalDependencies #-} 4 5{-# LANGUAGE FlexibleInstances #-} 6 7import Data.List.NonEmpty as NE 8 9class NELBuilder b a | b -> a where 10 11 buildNEL :: NonEmpty a -> b 12 13instance NELBuilder (NonEmpty a) a where 14 15 buildNEL xs = NE.reverse xs 16 17instance NELBuilder b a => NELBuilder (a -> b) a where 18 19 buildNEL xs x = buildNEL (x <| xs) 20 21nel :: NELBuilder b a => a -> b 22 23nel x = buildNEL (x :| [])
We are inferring the number of arguments from the context, so for nel ‘x’ ‘y’ :: NonEmpty Char, nel will have type Char -> Char -> NonEmpty Char. Thus in nel, a will match Char and b will match Char -> NonEmpty Char. It will call buildNEL with the singleton ‘x’ :| []. The type of buildNEL will match the recursive instance of NELBuilder for NELBuilder (a -> b) a where a is Char and b is NonEmpty Char. The buildNEL function will prepend ‘y’ to its first argument, yielding ‘y’ :| [‘x’]. Then it will recursively call buildNEL at the base case instance for (NonEmpty a) a where a is Char. That will reverse the supplied NonEmpty, producing the desired x :| [‘y’]. Here’s a table that shows how it unfolds:
Avoiding List Reversal
Although this worked, it felt slightly awkward that it had to reverse the list at the end (though it’s not really a performance issue with the typically tiny lists it’d be used to generate). So, instead of building up a non-empty list, we changed it to build up a difference list, that is, a function from non-empty lists to non-empty lists:
1{-# LANGUAGE FunctionalDependencies #-} 2{-# LANGUAGE FlexibleInstances #-} 3{-# LANGUAGE FlexibleContexts #-} 4import Data.List.NonEmpty as NE 5class NELBuilder b a | b -> a where 6 buildNEL :: (NonEmpty a -> NonEmpty a) -> b 7instance NELBuilder (a -> NonEmpty a) a where 8 buildNEL d x = d (x :| []) 9instance NELBuilder (a -> b) a => NELBuilder (a -> a -> b) a where 10 buildNEL d x = buildNEL (\xs -> d (x <| xs)) 11nel :: NELBuilder b a => b 12nel = buildNEL id
Although the difference list approach avoided reversing the list, type inference was not ideal when list elements were numeric literals. If one wrote nel 1 2 3 :: NonEmpty Int, GHC couldn’t figure out that the elements must be Ints:
1λ=> nel 1 2 3 :: NonEmpty Int 2<interactive>:5:1: error: 3 • No instance for (NELBuilder (Integer -> NonEmpty Int) Integer) 4 arising from a use of ‘nel’ 5 (maybe you haven't applied a function to enough arguments?) 6 • In the expression: nel 1 2 3 :: NonEmpty Int 7 In an equation for ‘it’: it = nel 1 2 3 :: NonEmpty Int
This happens because in the nel function, the type a doesn’t appear on the right-hand side, so it can’t be propagated from context. The types of the numeric literals get defaulted to Integer, but this doesn’t match the recursive NELBuilder (a -> a -> b) a instance as desired, because a must be both Integer and Int.
The problem seemed to lie in the weak relationship between b and a: If b were parameterized on a, we reasoned, then we could unify all the elements to the same type from the context.
Dependent Types to the Rescue
We found the clue in Donnacha Oisín Kidney’s post about liftAN. Instead of b, we use a dependent type family NELBuildFunc parameterized on both the count of arguments (using a type-level natural number) and the argument type. This allows for clean type inference of those two parameters:
1{-# LANGUAGE FlexibleInstances #-} 2{-# LANGUAGE FlexibleContexts #-} 3{-# LANGUAGE DataKinds #-} 4{-# LANGUAGE TypeFamilyDependencies #-} 5{-# LANGUAGE UndecidableInstances #-} 6{-# LANGUAGE AllowAmbiguousTypes #-} 7{-# LANGUAGE MultiParamTypeClasses #-} 8import Data.List.NonEmpty 9import GHC.TypeLits 10data N = Z | S N 11type family NELBuildFunc (n :: N) a = r | r -> n a where 12 NELBuildFunc Z a = NonEmpty a 13 NELBuildFunc (S n) a = a -> NELBuildFunc n a 14class NELBuilder n a where 15 buildNEL :: (NonEmpty a -> NonEmpty a) -> NELBuildFunc n a 16type NELNoArgsMessage = 17 'Text "Missing args to 'nel': Non-empty list cannot be empty" 18instance TypeError NELNoArgsMessage => NELBuilder Z a where 19 buildNEL = undefined 20instance NELBuilder (S Z) a where 21 buildNEL d x = d (x :| []) 22instance NELBuilder (S n) a => NELBuilder (S (S n)) a where 23 buildNEL d x = buildNEL (\xs -> d (x <| xs)) 24nel :: NELBuilder n a => NELBuildFunc n a 25nel = buildNEL id
We didn’t use GHC’s built-in Nat kind, because it’s not inductive, so we can’t pattern match on a successor. Instead, like Kidney, we created our own very simple Peano numerals and promoted them to the type level.
It’s also key that we made the type family injective(reversible): see the r | r -> n a annotation above. This is what allows GHC to infer the types of n and a from r.
As a bonus, we added a TypeError instance to report a helpful error if no arguments were supplied to n:
1λ=> nel :: NonEmpty Int 2<interactive>:3:1: error: 3 • Missing args to 'nel': Non-empty list cannot be empty 4 • In the expression: nel :: NonEmpty Int 5 In an equation for ‘it’: it = nel :: NonEmpty Int
Let the Computer Do the Counting
We’ve replaced many of our uses of NE1..NE4 with nel, but they’re still useful for pattern matching, and nel occasionally needs an extra type annotation introduced to work. Using nel, we can now let the computer count the number of arguments needed to build our non-empty lists.
