輸入安全的相等元組大小。

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