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?
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]