Hi,Thanks for the pointers. So I’ve got
data M (n :: Nat) a = M [a] deriving Show
t2 :: M 2 Int
t2 = M [1,2]
t3 :: M 3 Int
t3 = M [1,2,3]
fx :: Num a => M n a -> M n a -> M n a
fx (M xs) (M ys) = M (zipWith (+) xs ys)
and having
g = fx t2 t3
won’t compile. Which is what I want.
However…
t2 :: M 2 Int
t2 = M [1,2]
is ‘hardwired’ to 2 and clearly I could make t2 return a list of any length.
So what I then tried to look at was a general function that would take a list of Int and create the M type using the length of the supplied list.
In other words if I supply a list, xs, of length n then I wan’t M n xs
Like this
createIntM xs = (M xs) :: M (length xs) Int
which compile and has type
λ-> :t createIntM
createIntM :: [Int] -> M (length xs) Int
and all Ms created using createIntM have the same type irrespective of the length of the supplied list.
What’s the type jiggery I need or is this not the right way to go?
Thanks
Mike