Type safe equal tuple sizes.

Question

How can I write best write a type signature in Haskell that best encapsulates the idea that a function must be passed a tuple of any length with all elements X, and a list of tuples (of the same length) with all elements Y?

I don't mind if the type passed is a "real" tuple some alternate data type, as long as I can enforce at compile time that both the tuple and the list of tuples have the same length.

Tuple N X -> [Tuple N Y] -> Z

Answer 1

As zoran119 suggests, length-indexed vectors are the classic way to do this.

{-# LANGUAGE GADTs, DataKinds #-}

data Nat = Z | S Nat

data Vec n a where
  Nil :: Vec 'Z a
  Cons :: a -> Vec n a -> Vec ('S n) a

Now you can easily write

f :: Vec n X -> [Vec n Y] -> Z