Haskell: Specifying equal-length constraints of lists in the type system

Question

In Haskell, I often have a function like f, which accepts a list and returns a list of equal length:

f :: [a] -> [a]  -- length f(xs) == length xs

Similarly, I might have a function like g, which accepts two lists that should be of equal length:

g :: [a] -> [a] -> ...

If f and g are typed as above, then run-time errors may result if their length-related constraints are not satisfied. I would therefore like to encode these constraints in the type system. How might I do this?

Please note that I'm looking for a practical framework that may be used in everyday situations, adding as little intuitive overhead to the code as possible. I am particularly interested to know how you would deal with f and g yourself; that is, would you attempt to add the length-related constraints to their types, as asked here, or would you leave them with the types as given above for simplicity of code?

Answer 1

The following code is adapted from Gabriel Gonzalez's blog in combination with some information supplied in the comments:

{-# LANGUAGE GADTs, DataKinds #-}

data Nat = Z | S Nat

-- A List of length 'n' holding values of type 'a'
data List n a where
    Nil  :: List Z a
    Cons :: a -> List m a -> List (S m) a

-- Just for visualization (a better instance would work with read)
instance Show a => Show (List n a) where
    show Nil = "Nil"
    show (Cons x xs) = show x ++ "-" ++ show xs

g :: (a -> b -> c) -> List n a -> List n b -> List n c
g f (Cons x xs) (Cons y ys) = Cons (f x y) $ g f xs ys
g f Nil Nil = Nil

l1 = Cons 1 ( Cons 2 ( Nil ) ) :: List (S (S Z)) Int
l2 = Cons 3 ( Cons 4 ( Nil ) ) :: List (S (S Z)) Int
l3 = Cons 5 (Nil) :: List (S Z) Int

main :: IO ()
main = print $ g (+) l1 l2
       -- This causes GHC to throw an error:
       -- print $ g (+) l1 l3

This alternative list definition (using GADTs and DataKinds) encodes the length of a list in its type. If you then define your function g :: List n a -> List n a -> ... the type system will complain if the lists are not of the same length.

In case this would (understandably) be too much extra complication for you, I'm not sure using the type system would be the way to go. The easiest is to define g using a monad/applicative (e.g. Maybe or Either), let g add elements to your list depending on both inputs, and sequence the result. I.e.

g :: (a -> b -> c) -> [a] -> [b] -> Maybe [c]
g f l1 l2 = sequence $ g' f l1 l2
  where g' f (x:xs) (y:ys) = (Just $ f x y) : g' f xs ys
        g' f [] [] = []
        g' f _ _ = [Nothing]

main :: IO ()
main = do print $ g (+) [1,2] [2,3,4] -- Nothing
          print $ g (+) [1,2,3] [2,3,4] -- Just [3,5,7]

Answer 2

The lack you observe is because the information of length is not a part of the type of the list; because the type checker is meant to reason about types, you can't specify invariants in your functions unless the invariants are in the type of the arguments themselves, or on typeclass constraints or type family-based equalities. (There are some haskell pre-processors, though, like Liquid Haskell, that allow you to annotate functions with invariants like this that will be checked on compilation.)

there are many haskell libraries that offer list-like data structures with length encoded in the type. Some notable ones are linear (with V) and fixed-vector.

The interface for V goes something like this:

f :: V n a -> V n a -> V n a
g :: V n a -> V n a -> [a]
-- or --
g :: V n a -> V n a -> V ?? a -- if ?? can be determined at compile-time

Note the particular pattern of our first type signature for g: We take two types where we care about the lengths, and return a type that doesn't care about the length, losing information.

In the second case, if we do care about the length of the result, the length has to be known at compile-time for this to make sense.

Note that V from linear actually doesn't wrap a list, but a Vector from the vectors library. It also requires lens (the linear library, that is), which is admittedly a huge dependency to pull in if all you want is length-encoded vectors. I think the vector type from fixed-vectors does use something more equivalent to a normal haskell list...but I'm not totally sure. In any case, it has a Foldable instance, so you can convert it to a list.

Do remember of course that if you plan to encode lengths in your functions like this...Haskell/GHC has to be able to see that your implementation typechecks! For most of these libraries, Haskell will be able to typecheck things like this (if you stick with things like zipping and fmapping, binding, ap-ping). For most useful cases this is true...however, sometimes your implementation just can't be "proven" by the compiler, so you'll have to "prove" it to yourself in your head, and use some sort of unsafe coercion.