Тип безопасного размера одинакового кортежа.

Question

Как написать лучшую запись типа сигнатуры в Haskell, которая наилучшим образом инкапсулирует идею о том, что функции нужно передать кортеж любой длины со всеми элементами X и список кортежей (одной длины) со всеми элементами Y?

Я не возражаю, если переданный тип является «реальным» кортежем некоторого альтернативного типа данных, если я могу обеспечить во время компиляции, что и кортеж, и список кортежей имеют одинаковую длину.

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

Answer 1

Как предлагает zoran119, векторы с индексом длины - это классический способ сделать это.

{-# 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 

Теперь вы можете легко написать

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